[0042] Linear orders and simplicial types

We want to use simplicial types in homotopy type theory. They will be used to define the type of $(\infty , 1)$ -categories. However, simplicial types are functors to the $(\infty , 1)$ -category of types. To define the type of those functors, we have to already know what $(\infty , 1)$ -categories are, so we get stuck.

A good news is that the category of simplicial types is the category of sheaves on the topos of linear orders; see, for example, Section VIII.8 of [Mac-Lane--Moerdijk--1992-0000]. Thus, in a type theory with a generic linear order, we can do some simplicial type theory and then some $(\infty , 1)$ -category theory. This is indeed the idea of synthetic $(\infty , 1)$ -category theory [Riehl--Shulman--2017-0000].

The type theory proposed in [Riehl--Shulman--2017-0000] is intended to be the internal language of the category of simplicial types. However, some important properties of this category is not internal. For example, the standard $$n$$ -simplex is tiny. Tininess refers to the hom functor to the “base” category of types. To speak about tininess in the internal language, some base type theory would be needed. Our topical type theory perfectly fits.

[0043] Definition

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)$

[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.

[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.

[004A] Proposition

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$$ .

[0046] Proposition

Let $$T$$ be a base type theory. We work in the type theory of spaces in $$T$$ . Let $n:\mathord {\textnormal {\textsf {Nat}}}$ . Then the point ${\langle n\rangle }_{\mathord {\textnormal {\textsf {LO}}}}:\mathord {\textnormal {\textsf {LO}}}$ is coétale.

Proof

Let $A:\mathord {\textnormal {\textsf {LO}}}$ . By [004A], the type ${\langle n\rangle }_{\mathord {\textnormal {\textsf {LO}}}}\Rightarrow A$ is equivalent to the type of increasing chains of points of $$A$$ of length $$n$$ . That type is constructible from $A.\mathord {\textnormal {\textsf {Carrier}}}$ and $A.\le$ by finite limits and thus étale.

[0049] Definition

Let $$T$$ be a base type theory. We work in $$T$$ . Let $n:\mathord {\textnormal {\textsf {Nat}}}$ . We define the standard $$n$$ -simplex $\Delta \lbrack n\rbrack :\mathcal {S}(\mathord {\textnormal {\textsf {LO}}},0)$ to be $\mathord {\textnormal {\textsf {e}}}_{{\langle n\rangle }_{\mathord {\textnormal {\textsf {LO}}}}}$ .