Synthetic topos theory
[0044] Definition

Let \(T\) be a base type theory. We work in \(T\). Let \(n:\mathord {\textnormal {\textsf {Nat}}}\). We define a point \({\langle n\rangle }_{\mathord {\textnormal {\textsf {LO}}}}:\mathord {\textnormal {\textsf {LO}}}\) by adjoining a new bottom element \(\mathord {\textnormal {\textsf {b}}}\) and a new top element \(\mathord {\textnormal {\textsf {t}}}\) to \(\mathord {\textnormal {\textsf {Fin}}}(n)\) with the standard order.