[003R] -- 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.