Synthetic topos theory
[003P] Definition

Let \(T\) be a base type theory. We work in \(T\). Let \(X_{1}\) and \(X_{2}\) be toposes. We say a morphism \(f:X_{1}\rightarrow X_{2}\) is essential if \({f}^{*}:\mathcal {S}(X_{2},0)\rightarrow \mathcal {S}(X_{1},0)\) has a left adjoint \({f}_{!}\).