Fundamental theorem of topos theory

In mathematics, The fundamental theorem of topos theory states that the slice formula_1 of a topos formula_2 over any one of its objects formula_3 is itself a topos. Moreover, if there is a morphism formula_4 in formula_2 then there is a functor formula_6 which preserves exponentials and the subobject classifier.
The pullback functor.
For any morphism "f" in formula_2 there is an associated "pullback functor" formula_8 which is key in the proof of the theorem. For any other morphism "g" in formula_2 which shares the same codomain as "f", their product formula_10 is the diagonal of their pullback square, and the morphism which goes from the domain of formula_10 to the domain of "f" is opposite to "g" in the pullback square, so it is the pullback of "g" along "f", which can be denoted as formula_12.
Note that a topos formula_2 is isomorphic to the slice over its own terminal object, i.e. formula_14, so for any object "A" in formula_2 there is a morphism formula_16 and thereby a pullback functor formula_17, which is why any slice formula_18 is also a topos.
For a given slice formula_19 let formula_20 denote an object of it, where "X" is an object of the base category. Then formula_21 is a functor which maps: formula_22. Now apply formula_23 to formula_21. This yields
so this is how the pullback functor formula_23 maps objects of formula_19 to formula_28. Furthermore, note that any element "C" of the base topos is isomorphic to formula_29, therefore if formula_30 then formula_31 and formula_32 so that formula_23 is indeed a functor from the base topos formula_2 to its slice formula_28.
Logical interpretation.
Consider a pair of ground formulas formula_36 and formula_37 whose extensions formula_38 and formula_39 (where the underscore here denotes the null context) are objects of the base topos. Then formula_36 implies formula_37 if and only if there is a monic from formula_38 to formula_39. If these are the case then, by theorem, the formula formula_37 is true in the slice formula_45, because the terminal object formula_46 of the slice factors through its extension formula_39. In logical terms, this could be expressed as
so that slicing formula_2 by the extension of formula_36 would correspond to assuming formula_36 as a hypothesis. Then the theorem would say that making a logical assumption does not change the rules of topos logic.