Synthetic topos theory
[003X] Proposition

Let \(T\) be a base type theory. We work in the type theory of spaces \(T\). Then the point \(\mathord {\textnormal {\textsf {1}}}:\mathcal {E}\) is coétale.

Proof

For any \(X:\mathcal {E}\), we have \((\mathord {\textnormal {\textsf {1}}}\Rightarrow X)\simeq X\), and thus \(\mathord {\textnormal {\textsf {1}}}\Rightarrow X\) is in \(\mathcal {E}(0)\).