The $\mathrm{\infty }$-category of $\mathrm{\infty }$-categories in simplicial type theory

Simplicial type theory (STT) was introduced by Riehl and Shulman [1] to leverage homotopy type theory to prove results about $(\mathrm{\infty },1)$-categories. Initial work on simplicial type theory focused on “formal” arguments in higher category theory and, in particular, no non-trivial examples of $\mathrm{\infty }$-category theory were constructible within STT. More recent work has changed this state of affairs by applying techniques developed initially for cubical type theory to construct the $\mathrm{\infty }$-category of spaces. In [2], we complete this process by constructing the $\mathrm{\infty }$-category of $\mathrm{\infty }$-categories, recovering one of the main foundational results of $\mathrm{\infty }$-category theory (straightening–unstraightening) purely type-theoretically. STT extends HoTT with a directed interval, a postulated totally ordered lattice $(𝕀,0,1,\le )$. This new type is meant to represent the category $0\to 1$—an interpretation justified by the model of STT in simplicial spaces—and we then use $𝕀$ to define morphisms in an arbitrary type $A$ as ordinary functions $𝕀\to A$ constraining the endpoints: ${\mathrm{hom}}_A(a,b)={\sum }_{f:𝕀\to A}f\mathrm{\hspace{0.17em}0}=a\times f\mathrm{\hspace{0.17em}1}=b$. [1] then demonstrate that the definition of an $\mathrm{\infty }$-category can be formulated concisely as a predicate $\mathrm{𝗂𝗌𝖢𝖺𝗍}$ on types, essentially requiring every pair of composable morphisms have a unique composite. Furthermore, they show that ordinary functions between such types constitute functors and that other classical definitions in $\mathrm{\infty }$-category theory become expressible. Subsequent work has further expanded this approach, developing fibered category theory, (co)limits, etc. As an extension of HoTT, STT comes equipped with a (hierarchy of) universes and it is therefore natural to ask: Is $𝒰$ a recognizable category, e.g., the category of categories?

Unfortunately, the answer is negative; $𝒰$ is the canonical example of a type that is not an $\mathrm{\infty }$-category in STT. In fact, even if one considers simple subtypes of the universe (e.g., ${\sum }_{A:𝒰}\mathrm{𝗂𝗌𝖢𝖺𝗍}(A)$) one does not obtain a category, as synthetic morphisms $𝕀\to {\sum }_{A:𝒰}\mathrm{𝗂𝗌𝖢𝖺𝗍}(A)$ neither compose nor faithfully represent functors. However, it has long been conjectured that the category of categories should be constructible in STT as a certain subtype of the universe. We address this final gap in the foundations of STT by settling this conjecture affirmatively and constructing the category of categories as a subtype $\mathrm{Cat}\hookrightarrow 𝒰$ and verifying its essential properties:

1. 1.

   $\mathrm{Cat}$ is the base of the universal cocartesian fibration

2. 2.

   $\mathrm{Cat}$ is directed univalent, i.e., for global elements $A,B$ in $\mathrm{Cat}$ we have ${\mathrm{hom}}_{\mathrm{Cat}}(A,B)\simeq {(A\to B)}^{\simeq }$.

3. 3.

   $\mathrm{Cat}$ is a category (i.e., Segal and Rezk) and simplicial.

We promote this to a straightening–unstraightening theorem à la [5] and give first applications such as defining monoidal $\mathrm{\infty }$-categories, $K$-theory of monoidal $1$-categories, and using $\mathrm{Cat}$’s structure homomorphism principle to compute the morphisms of the lax slice $1\downarrow \mathrm{Cat}$ and of the category of marked categories.