[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)