Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\).

• -\(\mathbb {I}:\mathcal {T}\)
• -\(\le :\mathbb {I}\rightarrow \mathbb {I}\rightarrow \lbrace X:\mathcal {T}\mid \mathord {\textnormal {\textsf {IsTrunc}}}_{-1}(X)\rbrace \)
• -\(\mathord {\textnormal {\textsf {b}}}:\mathbb {I}\)
• -\(\mathord {\textnormal {\textsf {t}}}:\mathbb {I}\)
• -\(\le \) is a partial order on \(\mathbb {I}\).
• -\(\mathord {\textnormal {\textsf {b}}}\) is the least element.
• -\(\mathord {\textnormal {\textsf {t}}}\) is the greatest element.
• -\(\mathord {\textnormal {\textsf {b}}}\) and \(\mathord {\textnormal {\textsf {t}}}\) are distinct.