new task list incoming

Stream: Infinity-Cosmos

[Emily Riehl]

I've been (slowly) working on extending the infinity-cosmos blueprint, as you can see from the newly enlarged dependency graph. Sometime in the next few days, I should be ready to post a new task list to map out the second phase of the infinity-cosmos project.

The main objectives will be to :

(i) develop a bit of infinity-cosmos theory (the easier results from section 1.5)
(ii) develop a bit more enriched category theory (about enriched completeness and enriched change of base)
(iii) prove that the homotopy category functor preserves products (when restricted to quasi-categories), a task from the original list now spread over a series of lemmas appearing in the new section 1.3
(iv) compare Cat-enriched categories and 2-categories.
(v) An optional side quest: to prove that 1-categories define an infinity-cosmos (see section 1.7).

The upshot will be the construction of the 2-category of infinity-categories contained in an infinity-cosmos. Then the formal category theory can begin.

Here is a question: where should I put the new tasks? Appended to an edited version of the original list? Later in the same thread? In a new thread? I have no idea where it is least likely to get lost.

[Pietro Monticone]

I think it’s better to adopt the new dashboard-based workflow we are using in #FLT and #Equational (see here and here).

If you’re interested, I have just sent you the instructions you should follow to enable it for InfinityCosmos too and then I’ll add the new workflow scripts.

I apologise for the current lack of documentation, but it will be available in a month or so within the LeanProject template (adding MAINTAINING.md and MANAGING.md to the usual CONTRIBUTING.md).

[Emily Riehl]

Thanks @Pietro Monticone it does sound like a good idea to move to the dashboard-based workflow. I'll see if I can figure out how to set it up (over the next week or so) and will be in touch if I need help.

[Pietro Monticone]

Added :check: (see here).

Tested :check: (see here).

[Dean Young]

Jiazhen and I don't work on this topic but his lemmas about cofibrations are going to be PR'd and the recent work on CW-complexes is important for the analytic approach that the group here has outlined.