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