Synthetic topos theory
[0045] Exercise

Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). Then the morphisms between points of \(\mathord {\textnormal {\textsf {LO}}}\) are equivalent to the functions between carrier types preserving orderings, bottom elements, and top elements.