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