Synthetic topos theory
[003S] Proposition

Let \(T\) be a base type theory. We work in \(T\). Let \(X_{1}\) be a topos and let \(X_{2}:X_{1}\rightarrow \mathcal {E}(0)\). Then the first projection \((x:X_{1})\times X_{2}(x)\rightarrow X_{1}\) is essential.

Proof

Using [002Y], the claim is reduced to the case when \(X_{1}\) is the terminal topos. It is thus enough to show that \(\Delta _{X}:\mathcal {U}(0)\rightarrow \mathcal {S}(X,0)\) has a left adjoint for every \(X:\mathcal {E}(0)\). Let \(A:\mathcal {U}(0)\) correspond to \(X\) by [002S]. By [004W], \(\Delta _{X}\) is equivalent to the constant-function functor \(\mathcal {U}(0)\rightarrow (A\rightarrow \mathcal {U}(0))\). It has the left adjoint \(B\mapsto (x:A)\times B(x)\).