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 (Jan 15 2021 at 14:45):I'm trying to work through that the category of categories is not locally cartesian closed. One such explicit proof makes use of the fact that in LCCCs "pullbacks preserve colimits" (fourth paragraph of Definition section on nLab page on LCCC. My problem is, I don't see why that latter 'fact' is the case, and I can't find another source that is more explicit about that.
I should not that proving that the first diagram in the above proof is actually a pushout is... tedious. The definition of the universal arrow and that it has the right properties is quite a bit of work. Furthermore, it's not even obvious, in the sense that this is real data in that arrow that can be defined incorrectly!
Nathanael Arkor (Jan 15 2021 at 15:06):Pullbacks preserve colimits in a LCCC because each pullback functor has a right adjoint , and left adjoints preserve colimits.
Jacques Carette (Jan 15 2021 at 15:17):Ah, indeed. I'll need to make sure that the proof of all those pieces are around too. I think I've seen some of them [where by 'proof', I always mean fully formalized.]
Todd Trimble (Jan 15 2021 at 15:19):@Jacques Carette To relieve the tedium of verifying that pushout, one thing to do is verify that the obvious analogue in the category of directed graphs is clearly a pushout (pushouts are computed "pointwise" or "objectwise" because directed graphs form a presheaf topos), and then apply the free category construction (taking paths in directed graphs). That free construction, being a left adjoint, preserves pushouts.
Jacques Carette (Jan 15 2021 at 17:17):I will indeed try to do just that. Let's see if enough of these things are already implemented in agda-categories. I know some are. And they all ought to be.