locally cartesian closed categories

Stream: maths

[Sina Hazratpour 𓃵]

The polynomial functor project includes a formalization of locally cartesian closed categories (lccc). In the next week, I am going to PR some code from the polynomial functors project to mathlib.

Where would be a good place in mathlib for lcccs? Closed.LocallyCartesian is one candidate. Another option would be to have a separate subdir LocallyCartesianClosed in CategoryTheory.

[Mario Carneiro]

BTW, can we agree that LCCC has 3 C's in it?

[Adam Topaz]

I think we should rather have a Cartesian subdirectory in CategoryTheory where stuff like this should go. But that would involve some reorganizing of existing files, so it’s probably worth adding LCCCs and only later doing the reorganization

[Robin Carlier]

@Sina Hazratpour Locally cartesian closed categories were mentioned in #28908, where @Joël Riou essentially proves that Type _ is locally cartesian closed.
Do you still plan to upstream this work?

[Sina Hazratpour]

yes, i plan to. They are currently in the mathlib PR queue, and there is a merge conflict that needs to be resolved. But I can do it this week.

[Sina Hazratpour]

I also have proved the locally cartesian closedness of Type in the Poly repo mentioned above. The strategy is as follows: I showed that in the category of types the slices $Types/X$ are the same as functor categories $X \to Type$ which is shown to be cartesian closed in mathlib

[Sina Hazratpour]

We then obtain the explicit right adjoints to the pullback functor from the definition of locally cartesian closed.

[Robin Carlier]

#21525 for reference.

Do you also plan on upstreaming cartesian closedness of Type? I believe @Joël Riou is a bit in a hurry to have that the base change functors preserve colimits for his applications.

[Sina Hazratpour]

i feel this proof is better than constructing the right adjoints explicitly, since it uses the bundle classifier pointed Types to Types and this kind of proofs scale better

[Sina Hazratpour]

i will upstream both lccc and the cartesian closedness of Type. I also have the preservation of colimits.

[Sina Hazratpour]

ok, let me see if i can finish this tonight.

[Joël Riou]

No, no, I am not at all in a hurry. This will be used in some of the last steps on the construction of the Quillen model category structure on simplicial sets, which shall need 35k extra lines of code.

[Robin Carlier]

Oh, then we have time! Then no hurry @Sina Hazratpour

[Robin Carlier]

(sorry to have assumed the hurry!)

[Sina Hazratpour]

no problem, i think i will do it tonight anyway, it's a good excuse to get this past the PR queue.

[Robin Carlier]

Feel free to assign it (and related PRs) on GitHub when they're ready!

[Sina Hazratpour]

@Robin Carlier @Joël Riou
Coming back to this, I have started to push LCCC work to mathlib. Since the write-access thing on mathlib has changed, and one needs to PR from a fork of mathlib, I am opening new PRs from my fork of mathlib than using the ones with merge conflict from back in February. It seems cleaner this way. I have so far pushed lccc-prelim (#30366), lccc-section (#30373) and lccc-basic (#30375), each depending on the previous one. lccc-basic defines locally cartesian closed categories. Then there will be lccc-types, lccc-presheaf, lccc-beck-chevalley. I will however only open PRs for the last three ones once the first three PRs get merged (though all six of them are on my fork of mathlib), since otherwise i would create a lot more extra work with merge, rebase, etc during the review process. Does this sound good to you? Let me know if you have suggestions.