Let \(T\) be a base type theory. We work in the type theory of spaces \(T\). Let \(n:\mathord {\textnormal {\textsf {Nat}}}\) in \(T\) and let \(A:\mathord {\textnormal {\textsf {LO}}}\). Then the morphisms from \({\langle n\rangle }_{\mathord {\textnormal {\textsf {LO}}}}\) to \(A\) are equivalent to the (non-strictly) increasing chains of points of \(A\) of length \(n\).
Proof
By [0045], the morphisms \({\langle n\rangle }_{\mathord {\textnormal {\textsf {LO}}}}\rightarrow A\) are equivalent to the functions \({\langle n\rangle }_{\mathord {\textnormal {\textsf {LO}}}}\rightarrow A\) preserving orderings, bottom elements, and top elements. By the construction of \({\langle n\rangle }_{\mathord {\textnormal {\textsf {LO}}}}\), they are equivalent to the functions \(\mathord {\textnormal {\textsf {Fin}}}(n)\rightarrow A\) preserving orderings, which are equivalent to the increasing chains of points of \(A\) of length \(n\).