You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Jacques Carette (Dec 08 2021 at 17:16):In a category with pullbacks, a slice category, i.e. [[over category]], gives rise to a [[codomain fibration]]. The question: is it possible to define what a [[locally cartesian closed category]] is purely in terms of that fibration, never referring to slices at all?
Perhaps this is done in Streicher's Fibered Categories a la Jean Benabou or in Jacobs' book? What I see in Streicher's work is too dense for my comprehension.
Mike Shulman (Dec 08 2021 at 17:22):Yes; a category is LCCC iff that fibration has fibered products, i.e. right adjoints to restriction functors.
Jacques Carette (Dec 08 2021 at 18:30):Is there somewhere that is explained slowly, with details? My googling has not generated anything that seems 'on point'.
Mike Shulman (Dec 08 2021 at 18:33):It's Proposition 1.9.8(iii) in Jacobs' book. The proof is kind of brief and calls out to an exercise, though.
Mike Shulman (Dec 08 2021 at 18:37):It's also B1.4.7(iii) in Sketches of an Elephant, where the role of the crucial exercise is played by A1.5.3, which is a corollary of A1.5.2 whose proof is written out in reasonable detail.
Jacques Carette (Dec 08 2021 at 18:39):I've been meaning to rework my way through Jacob's book - additional incentive. And I do own it. I've looked to purchase sketches of an elephant but the price is prohibitive. Hopefully my university library has it.
Thanks for the very detailed references.
Mike Shulman (Dec 08 2021 at 18:59):Yeah, I agree the price is kind of ridiculous. If your library doesn't have it you can try ILL.
dusko (Dec 09 2021 at 00:21):Jacques Carette said:
In a category with pullbacks, a slice category, i.e. [[over category]], gives rise to a [[codomain fibration]]. The question: is it possible to define what a [[locally cartesian closed category]] is purely in terms of that fibration, never referring to slices at all?
Perhaps this is done in Streicher's Fibered Categories a la Jean Benabou or in Jacobs' book? What I see in Streicher's work is too dense for my comprehension.
i imagine that thomas streicher might be hurrying past LCCCs because he spent a lot of time on them when he worked on semantics of type theories. so a more careful presentation might be in his earlier books. in any case, benabou was only talking about his calibrations, since "LCCCs were sufficiently covered in SGA4" :)
if the reason why you want to see LCCCs as fibrations is that you want to think of them as "fibered cartesian closure", that goes back to seely's paper which everyone read and cited. it should be on his page, aha: http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf
funny enough, the perverse idea of presenting the LCCC structure entirely in terms of fibrations occurred to me and my macintosh mk II when we were writing my thesis, just as a "why not", but then i needed it for comprehension, so it's there. i am not sure whether it is comprehensible :upside_down: but here it is: https://www.dropbox.com/s/z1xdw903xzy3u4u/1990-proefschrift-dusko.pdf?dl=0
Morgan Rogers (he/him) (Dec 09 2021 at 10:46):@Riccardo Zanfa and I have an ongoing project on the relationship between local cartesian closedness and fibrations. The relation is actually surprisingly strong and natural!
Jacques Carette (Dec 09 2021 at 12:35):Thanks @dusko , will read. @Morgan Rogers (he/him) anything written?
Jacques Carette (Dec 09 2021 at 12:38):I had read Seely's paper, but was only able to absorb parts of it, as I was quite new to category theory at the time. Looks like it needs another read!
Morgan Rogers (he/him) (Dec 09 2021 at 12:56):Nothing online yet. It's one of those things where the essential observation is very simple but we're hesitant to put it out into the world until we've done something more with it.