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. We define the direct image functor

\({f}_{*}:\mathcal {S}(X_{1},i)\rightarrow \mathcal {S}(X_{2},i)\) by the following composite. \(\mathcal {S}(X_{1},i)\)\(\simeq \) {fibrant replacement}\(\mathcal {S}((y:X_{2})\times \mathord {\textnormal {\textsf {Fib}}}(f,y),i)\)\(\simeq \) {[003L]}\(\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sh}}}(X_{2})}({}\vdash \mathcal {S}(\mathord {\textnormal {\textsf {Fib}}}(f,\mathord {\textnormal {\textsf {w}}}_{X_{2}}),i))\)\(\rightarrow \) {\(\Gamma _{\mathord {\textnormal {\textsf {Fib}}}(f,\mathord {\textnormal {\textsf {w}}}_{X_{2}})}\)}\(\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sh}}}(X_{2})}({}\vdash \mathcal {U}(i))\)\(\simeq \) {[003G]}\(\mathcal {S}(X_{2},i)\)