2 rearranged a bit, improved formatting

The question of local toposes and similar categories was discussed a couple of years ago on the categories list by Peter Johnstone and others, if I recall correctly. I don't know anywhere that they appear in print, but I don't know the topos theory literature nearly well enough to be an authoratitive source on this.


But local equivalences into a fixed category $\newcommand{\C}{\mathcal{C}} \C$, in turn, correspond (up to equivalence-over-$\C$) to functors $\C^\mathrm{op} \to \mathbf{Sets}$. ($F : \mathcal{D} \to \C$ corresponds to the functor taking $C \in \C$ to the set of isomorphism classes of objects of $\mathcal{D}$ over $C$.) Of course, there's a size consideration: whatever size of $\mathbf{Sets}$ we use constrains the essential size of the fibers.

In terms of local toposes seen as categories in their own right, one point of interest is that you can interpret pretty much all the logic in them that you can in toposes (i.e. higher-order type theory; and geometric logic if you go Grothendieck-y)… except that of course you have to abandon the “empty context”, since you don't have a terminal object. (Everything else in the interpretation of logic is purely local.) In a local topos, there is no “global validity”: all truth is relative :-)

This topic was discussed a couple of years ago on the categories list by Peter Johnstone and others, if I recall correctly. I don't know anywhere that they appear in print, but I don't know the topos theory literature nearly well enough to be a good source on this.

[1] The uniqueness issues here are a little subtle: if I'm not mistaken we need to either assume (large) choice, or use anafunctors instead of functors, or restrict the size of $\E$ enough that each slice will itself literally be an object of $\Topos$.

1

$\newcommand{\Topos}{\mathbf{Topos}_\mathit{slice}}$ One other in-some-sense-trivial example, if I'm not mistaken, is the category $\Topos$, with objects all (small, fsvo small) elementary toposes, and with maps just the geometric morphisms that are (up to equivalence) induced by slicing, modulo natural isomorphism. (If we wanted to cover our tracks a little, we could say “the geometric morphisms whose inverse image functors are logical”; the equivalence of this is shown in Mac Lane and Moerdijk in their chapter on logical morphisms, iirc.)

But this is the universal example: any other local topos $\newcommand{\E}{\mathcal{E}}$has a unique-up-to-equivalence “local equivalence” $\E \to \Topos$, sending $A$ to $\E/A$[1], and any local equivalence into $\Topos$ must come from a local topos.

But local equivalences into a fixed category $\newcommand{\C}{\mathcal{C}} \C$, in turn, correspond (up to equivalence-over-$\C$) to functors $\C^\mathrm{op} \to \mathbf{Sets}$. ($F : \mathcal{D} \to \C$ corresponds to the functor taking $C \in \C$ to the set of isomorphism classes of objects of $\mathcal{D}$ over $C$.) Of course, there's a size consideration: whatever size of $\mathbf{Sets}$ we use constrains the essential size of the fibers.

In terms of local toposes seen as categories in their own right, one point of interest is that you can interpret pretty much all the logic in them that you can in toposes (i.e. higher-order type theory; and geometric logic if you go Grothendieck-y)… except that of course you have to abandon the “empty context”, since you don't have a terminal object. (Everything else in the interpretation of logic is purely local.) In a local topos, there is no “global validity”: all truth is relative :-)

This topic was discussed a couple of years ago on the categories list by Peter Johnstone and others, if I recall correctly. I don't know anywhere that they appear in print, but I don't know the topos theory literature nearly well enough to be a good source on this.

[1] The uniqueness issues here are a little subtle: if I'm not mistaken we need to either assume (large) choice, or use anafunctors instead of functors, or restrict the size of $\E$ enough that each slice will itself literally be an object of $\Topos$.