Dear Thomas, -
On 6 Nov 2016, at 10:26, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote:
If SS is a (base) topos then P : EE -> SS is a fibration of toposes iff P is a Grothendieck fibration whose fibers are toposes and whose reindexing functors are logical. One may characterize them as fibrations P such that P is a logical morphism of toposes. Fibrations of cocomplete toposes over SS correspond to finite limit preserving functors from SS to some topos (namely Delta(I) = \coprod_I 1_I). Fibrations of locally small cocomplete toposes correspond to finite limit preserving functors to some topos which, moreover, have a right adjoint. The bounded gm's to SS correspond to fibrations of locally small cocomplete toposes which moreover admot a small generating family.
This is to check that I understand what you said correctly. First, technically, the topos EE that is the domain of P is not itself the domain of the geometric morphism, but an arrow topos. For example, for the identity geometric morphism, EE is [->,SS] and P is the codomain functor. Then the fibres are the slices of SS, still toposes, and the pullback functors are logical. (I think you said that before, but I didn't understand it then.) Then what is gained from using fibrations is a more secure understanding of "SS-cocomplete", having all SS-small colimits, in other words how SS supplies the infinities used in the geometric logic. Elephant B1.4.2 says for indexed categories that having all SS-indexed coproducts is to say that the reindexing functors have left adjoints, with Beck-Chevalley, and I imagine there's an analogous and possibly improved way to do it with fibrations. Is that right? All the best, Steve. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]