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.
Nathanael Arkor (Jan 15 2021 at 15:01):Most discussions regarding theories in the setting of topoi are in the context of geometric theories and Grothendieck topoi. Where can I find a discussion of "elementary theories" (a theory specified by the Mitchell-Bénabou language?) for elementary toposes? In particular, is there a proof in the literature that the category of models of an elementary theory is equivalent to some category of logical morphisms from the corresponding "classifying elementary topos"? My feeling is that the situation should be much less well-behaved for elementary topoi, due to the awkwardness of modelling exponentials and their contravariance.
Nathanael Arkor (Jan 15 2021 at 23:41):(The Elephant calls these "-theories", but only considers isomorphisms between models.)
Mike Shulman (Jan 16 2021 at 02:17):Nathanael Arkor said:
(The Elephant calls these "-theories", but only considers isomorphisms between models.)
There's a reason for that. Because of contravariance, it's not really clear what it would mean to talk about a non-invertible morphism between models of a higher-order theory.
Mike Shulman (Jan 16 2021 at 02:19):For instance, there is a higher-order theory whose models are topological spaces. What should the morphisms be? Continuous maps? Open maps? Closed maps?
Nathanael Arkor (Jan 16 2021 at 13:29):Yes, I imagine the right question to ask is: "Is there a notion of morphism for general higher-order theories that captures some existing kinds of morphisms for specific higher-order theories?"
Nathanael Arkor (Jan 16 2021 at 13:29):E.g. some kind of dinatural transformation.
Nathanael Arkor (Jan 16 2021 at 13:29):This sounds like an interesting question, but perhaps it hasn't been studied before.