Let \(T\) be a base type theory. We work in \(T\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\), let \(X_{1}\) and \(X_{2}\) be toposes, and let \(f:X_{1}\rightarrow X_{2}\) be a morphism. The inverse image functor

\({f}^{*}:\mathcal {S}(X_{2},i)\rightarrow \mathcal {S}(X_{1},i)\) is defined by precomposition with \(f\).