Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos and let \(a\) be a point of \(X\). Suppose that \(a\) is coétale. Then \(a\) is essential.
Proof
The morphism \(\_\mapsto a:\mathord {\textnormal {\textsf {1}}}\rightarrow X\) factors as \(\_\mapsto (a,\mathord {\textnormal {\textsf {id}}}):\mathord {\textnormal {\textsf {1}}}\rightarrow (x:X)\times (a\Rightarrow x)\) followed by the first projection \((x:X)\times (a\Rightarrow x)\rightarrow X\). The former is a left adjoint and thus essential by [003R]. The latter is essentialy by [003S] and by the assumption that \(a\) is coétale. Thus, their composite is also essential.