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. Then \({f}_{*}:\mathcal {S}(X_{1},i)\rightarrow \mathcal {S}(X_{2},i)\) is a right adjoint of \({f}^{*}:\mathcal {S}(X_{2},i)\rightarrow \mathcal {S}(X_{1},i)\).