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.
Ian Price (Aug 07 2026 at 13:17):In Altenkirch, Levy & Staton's "Higher Order Containers" they give a proof that the category of containers over Set (aka Poly) is cartesian closed. I would like to know if there are proofs that Cont(C) is cartesian closed for other C, e.g., when C is complete. (Specifically I'm interested in categories of assemblies/modest sets)
It's possible that their proof generalises easily, and my lack of familiarity with ends prevents me from seeing that.
Tom de Jong (Aug 07 2026 at 13:48):Reading the start of Section 2, I believe all mentions of Set are really mentions to some type-theoretic universe, so I would expect most of the paper (for instance, without the alternative proof sketched right before Section 5) to apply to any category C that is a model of extensional MLTT with the type formers described at the start of Section 2. (The requirement on the booleans being disjoint actually follows from having the type of booleans in the universe.) In particular, it should work for the category of assemblies.
(Link to a publicly available copy of the paper)
Ian Price (Aug 07 2026 at 14:17):thanks tom
Evan Cavallo (Aug 07 2026 at 18:45):Another presentation of this result in some generality is Theorem 4.4 In Von Glehn's thesis https://doi.org/10.17863/CAM.16245. (You'll have to chase down the ambient hypotheses...)
Ian Price (Aug 09 2026 at 09:45):Thanks Evan, this was a reference I should have checked by somehow slipped my mind