Simplicial Homotopy Type Theory is not just Simplicial: What are $\infty$-Categories?

Abstract

$\infty$-category theory was originally developed in the context of classical homotopy theory using standard set theoretical assumptions, but has since been extended to a variety of mathematical foundations. One such successful effort, primarily due to Martini and Wolf, introduced a theory of $\infty$-categories internal to the foundation of an arbitrary Grothendieck $\infty$-topos, meaning they used categorical foundations. Another approach, due to Riehl and Shulman, developed a theory of $\infty$-categories internal to their own type theory: simplicial homotopy type theory (sHoTT), meaning they employed a (homotopy) type theoretic foundation. One aspect of developing a theory of $\infty$-categories in different foundations consists of introducing ways to translate from one foundation to another. Concretely, as part of their work, Riehl and Shulman prove that $\infty$-categories internal to Grothendieck $\infty$-topoi give us categorical models of sHoTT. In fact the name ``simplicial'' in sHoTT suggests that all categorical models of sHoTT should be given by simplicial objects in suitable $\infty$-categories. In this paper we prove that contrary to this expectation, there are models of sHoTT that are not simply simplicial objects. This suggests that in a general foundations, the notion of $\infty$-category is more general than previously assumed.