synchronous meeting Monday November 24

Stream: Infinity-Cosmos

[Emily Riehl]

Save the date for a synchronous meeting of the infinity-cosmos team at 2025-11-24T11:00:00-5:00 - 2025-11-24T13:00:00-5:00 .

The aim will be to discuss plans to formalize the formal theory of quasi-categories described here: #Infinity-Cosmos > time for the formal category theory of quasicategories! @ 💬

[Emily Riehl]

Reminder that we will be holding a synchronous meeting on Zoom at 2025-11-24T11:00:00-5:00 - 2025-11-24T13:00:00-5:00 to discuss near term applications of bicategory theory to quasicategory theory. All are welcome (newcommers included).

[Mario Carneiro]

The universe issue is caused by an unnecessarily restrictive universe annotation upstream, fixed in #32063

[Mario Carneiro]

cleaned up and pushed the live coding session: cd00b63

[Emily Riehl]

How did you figure this out?

[Emily Riehl]

I promised a summary of the meeting that @Joël Riou, @Spencer Woolfson, @Jack McKoen, @Rida Hamadani, @Mario Carneiro, @Dagur Asgeirsson, @Julian Komaromy, @Judah Towery, Jonathan Weinberger and I had yesterday.

We discussed:

1. The new strict bicategory of quasicategories, now in Mathlib.
2. We constructed an analogous strict bicategory of infinity-categories in an infinity-cosmos. Later when we build the infinity-cosmos of quasicategories the strict bicategory of quasicategories will be a special case of this construction.
3. We discussed that the standard theory of adjunctions in a bicategory, much of which has already been formalized in Mathlib, specializes to define and develop adjunctions between quasicategories. So once we import the definition, Mathlib will have proofs of many interesting theorems about adjunctions between quasicategories!
4. We mentioned, but didn't really explain, that to develop the analogous formal theory of limits and colimits in a quasicategory, we need to know that the strict bicategory of such is cartesian closed. This will follow from the fact that quasicategories define a cartesian closed subcategory of simplicial sets.
5. We worked on the definition of a cartesian closed strict bicategory but haven't proven any theorems or developed API to work with this.

[Emily Riehl]

In the near term, I think it would be interesting to simultaneously:

1. Develop the theory of cartesian closed strict bicategories.
2. Develop the theory of limits in a cartesian closed strict bicategory (using Mathlib's existing notion of absolute lifting diagram.
3. Formalize the proof, assuming @Jack McKoen's result about functor quasicategories, that the strict bicategory of quasicategories is cartesian closed.

Unfortunately none of this is reflected by the current blueprint. So if there is any interest in working on any of these, let me know, and I'll get to work on writing up / finding references.

[Joël Riou]

About the prerequisites to 3., I recently found an article by Sean Moss, Another approach to the Kan-Quillen model structure, which gives a combinatorial approach to (strong) anodyne extensions, and I used it in my work on the Quillen model category structure on simplicial sets because I needed to know that anodyne extensions are preserved by the subdivision functor. The article by Moss also contains a lemma which allows to show that the inclusion (Λ[p, i] ⊗ Δ[q] ⊔ Δ[p] ⊗ ∂Δ[q]) ⟶ Δ[p] ⊗ Δ[q] is a (strong) anodyne extension (which is inner when Λ[p, i] is an inner horn), which I have also essentially formalized, and it contains as special cases both results about usual anodyne extensions which I had already formalized and a critical (more difficult) lemma that Jack had obtained. Several PRs to mathlib related to this have already been merged and the next are #28346, #28351 and #28462.

[Joël Riou]

The next significant result towards the study of (inner) fibrations is the result that I formalized (and which Jack uses) which is that any monomorphism of simplicial sets is a relative cell complex with basic cells consisting of boundary inclusions ∂Δ[q] ⟶ Δ[q]. This builds on previous formalization work about nondegenerate simplices. The first PR towards this result is #31996.

[Judah Towery]

I'm certainly interested in specifically what theory would be useful to work towards, I'd love to work on something. I did want to ask a perhaps basic question about how we've defined cartesian closed bicategories here. Am I correct in understanding that when we extend CartesianMonoidalCategory C, we get specifically just a monoidal structure on the underlying 1-category of the bicategory? If that is the case, then I wonder if that really is the same as the "usual" definition of a monoidal bicategory, which I understand briefly as "tricategory with one object." If we were to write out the algebraic data of this, we would require the monoidal structure to be a 2-functor that holds up to natural 2-isomorphisms with certain modification diagrams on 2-unitors etc., and I'm not sure if just a monoidal structure on the 1-category level can see or guarantee that. Is this idea of a monoidal bicategory not needed for this project?

[Emily Riehl]

@Judah Towery you're exactly right about monoidal bicategories, which are a much more complicated definition. In the cartesian monoidal structures on strict bicategories the definition simplifies: it's just a property of the strict bicategory (having finite cartesian products that have a universal property with respect to both 1-dimensional and 2-dimensional morphisms).

[Emily Riehl]

That said we should really prove a few properties of the definition to make sure that it's correct. For instance:

(i) The product should define a 2-functor, not just a functor.
(ii) We should have equivalences (in fact isomorphisms) of hom-categories into a finite product (essentially from the definition that our coyoneda functor preserves them).

In the case of cartesian closed strict bicategories we should have
(i) The exponential defines a 2-functor, not just a functor.
(ii) We should have equivalences (in fact isomorphisms) of hom-categories, extending currying to a 2-adjunction.

[Spencer Woolfson]

I would be happy to do the first two, and maybe the second two afterwards.