Synthetic topos theory

[004C] Internal topos theory

Topos theory is relative to a base logos. The topos theory we have presented is the topos theory relative to the category of types. For every topos \(X\), we can also develop the topos theory relative to \(\mathord {\textnormal {\textsf {Sh}}}(X)\) by understanding every word internally to \(\mathord {\textnormal {\textsf {Sh}}}(X)\).

[004D] Notation

Let \(U\) be a universe and let \(X\) be a \(U\)-topos. If \(A\) is a construction in the category of types, then we write \(A\mathrel {@}X\) for the same construction but performed in the category of sheaves on \(X\).

[004E] Exercise

Let \(U\) be a universe, let \(V\) be a universe strictly greater than \(U\), and let \(X\) be a \(U\)-topos. Then we have a canonical equivalence

\(\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V)/X\simeq \mathord {\textnormal {\textsf {Hom}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}(\mathord {\textnormal {\textsf {1}}},(\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V))\mathrel {@}X)\)