Jack McKoen: Toward functor quasi-categories in Lean

Stream: Lean Together 2025

[Johan Commelin]

Hi @Jack McKoen! Thanks for your talk. I'm currently half-way through watching it. On p24 you mention subcomplexes, and you show a formalization of Subpresheaf. But there is also a reasonably large API for subobjects in mathlib already. (All monomorphism modulo equiv.) Do you think it would be useful/possible to reuse that API?

[Adam Topaz]

I think Jack is using docs#CategoryTheory.Subpresheaf

[Emily Riehl]

I'd also be curious to hear about the relative merits of Subpresheaves and more general subobjects.

Relatedly, what is the rationale for the name: [Set](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Defs.html#Set) (F.obj U). I had assumed this was a typo in the slides and it should have said "Subset" until I looked up the definition just now...

[Yaël Dillies]

Do you mean docs#Set ?

[Emily Riehl]

My main comment for @Jack McKoen and the peanut gallery is that he is really underselling the importance of this project. We need this result and some extensions (a few relative forms of the theorem he has nearly proven involving an isofibration between quasi-categories) to construct the motivating examples of an ∞-cosmos: the ∞-cosmos of quasi-categories. Only then will the general synthetic theory of ∞-categories we are developing have concrete implications for Mathlib.

[Emily Riehl]

Yaël Dillies said:

Do you mean docs#Set ?

Yes, how should I be thinking of sets? I had been thinking that types in mathlib were either sets (or propositions), eg., 0-types or -1-types in the language of HoTT. So why are we using the name "set" for their subsets?

[Yaël Dillies]

This is how the type theory lingo goes as far as I'm aware. Set-theoretic sets becomes types, and subset of X become Set X.

[Joël Riou]

In this case, using the Subpresheaf API seems much more convenient for computations, as compared to Subobject (equivalences classes of monomorphisms). Imagine doing computations with "subsets" of a set X using only the notion of monomorphism in the category of sets, pullbacks, etc, when we can use the more convenient Set API.
I am currently working on usual "anodyne extensions", whereas Jack works on "inner anodyne extensions". The latter are probably slightly more difficult to handle as it seems he has to deal with subcomplexes of $\Delta^2 \times \Delta^n$ which may have more intricate combinatorics as compared to the subcomplexes of $\Delta^1 \times \Delta^n$ which I have to deal with.

[Adam Topaz]

Yaël Dillies said:

This is how the type theory lingo goes as far as I'm aware. Set-theoretic sets becomes types, and subset of X become Set X.

The fact that Agda likes to use Set to mean Type could be some source of confusion.

[Johan Commelin]

Emily Riehl said:

Relatedly, what is the rationale for the name: [Set](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Defs.html#Set) (F.obj U). I had assumed this was a typo in the slides and it should have said "Subset" until I looked up the definition just now...

I think one reason is that you can think of S : Set Nat as a set of natural numbers.
Of course "subset" is a good mental model. But since Nat is not itself a set, it breaks down somewhere...

[Adam Topaz]

I guess a natural name could be SetOf X so S : SetOf Nat is a set of nats.

[Adam Topaz]

But I don't think Set is ever going to change in Lean, and I think most Leansters are used to it by now.

[Adam Topaz]

In terms of HoTT, IIRC, contractible types are the (-2)-types, props are the (-1)-types and sets are the 0-types. So Lean's Prop should correspond to the type of HoTT's (-1)-types, Lean's Type should correspond to the type of HoTT's 0-types (and of course we don't have a built-in notion of an n-type for positive n). In Lean, Set X is defined as X -> Prop, i.e. we identify a subset of X with the predicate that defines it.

[Kevin Buzzard]

I goofed up the intro to this one, the video with fixed intro is here https://youtu.be/PHL4Ma3znmE?si=VCdzQ6cIzuqSHtMN

[Jack McKoen]

Late response but I largely agree with Joël on using the Subpresheaf API. Thanks for your comments @Johan Commelin and @Emily Riehl!