Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). Let \(n:\mathord {\textnormal {\textsf {Nat}}}\). Then the point \({\langle n\rangle }_{\mathord {\textnormal {\textsf {LO}}}}:\mathord {\textnormal {\textsf {LO}}}\) is coétale.
Proof
Let \(A:\mathord {\textnormal {\textsf {LO}}}\). By [004A], the type \({\langle n\rangle }_{\mathord {\textnormal {\textsf {LO}}}}\Rightarrow A\) is equivalent to the type of increasing chains of points of \(A\) of length \(n\). That type is constructible from \(A.\mathord {\textnormal {\textsf {Carrier}}}\) and \(A.\le \) by finite limits and thus étale.