Synthetic topos theory
[003R] Proposition

Let \(T\) be a base type theory. We work in \(T\). Let \(X_{1}\) and \(X_{2}\) be toposes and let \(f:X_{1}\rightarrow X_{2}\) be a morphism. If \(f\) has a right adjoint, then \(f\) is essential.

Proof

This is because the operation \(X\mapsto \mathcal {S}(X,i)\) is \(2\)-functorial and reverses \(1\)-cells.