Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). We define the topos of linear orders \(\mathord {\textnormal {\textsf {LO}}}\) by the following record type.

• -\(\mathord {\textnormal {\textsf {Carrier}}}:\mathcal {E}\)
• -\({\le }:\mathord {\textnormal {\textsf {Carrier}}}\rightarrow \mathord {\textnormal {\textsf {Carrier}}}\rightarrow \Omega \)
• -\(\mathord {\textnormal {\textsf {b}}}:\mathord {\textnormal {\textsf {Carrier}}}\)
• -\(\mathord {\textnormal {\textsf {t}}}:\mathord {\textnormal {\textsf {Carrier}}}\)
• -\(\_:\mathop {\forall }_{x:\mathord {\textnormal {\textsf {Carrier}}}}x\le x\)
• -\(\_:\mathop {\forall }_{x,y,z:\mathord {\textnormal {\textsf {Carrier}}}}x\le y\rightarrow y\le z\rightarrow x\le z\)
• -\(\_:\mathop {\forall }_{x:\mathord {\textnormal {\textsf {Carrier}}}}\mathord {\textnormal {\textsf {IsContr}}}((y:\mathord {\textnormal {\textsf {Carrier}}})\times (x\le y)\times (y\le x))\)
• -\(\_:\mathop {\forall }_{x:\mathord {\textnormal {\textsf {Carrier}}}}\mathord {\textnormal {\textsf {b}}}\le x\)
• -\(\_:\mathop {\forall }_{x:\mathord {\textnormal {\textsf {Carrier}}}}x\le \mathord {\textnormal {\textsf {t}}}\)
• -\(\_:\neg (\mathord {\textnormal {\textsf {b}}}=\mathord {\textnormal {\textsf {t}}})\)
• -\(\_:\mathop {\forall }_{x,y:\mathord {\textnormal {\textsf {Carrier}}}}(x\le y)\lor (y\le x)\)