Simplicial Homotopy Type Theory is not just Simplicial: What are ∞-Categories?

∞-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 ∞-categories internal to the foundation of an arbitrary Grothendieck ∞-topos, meaning they used categorical foundations. Another approach, due to Riehl and Shulman, developed a theory of ∞-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 ∞-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 ∞-categories internal to Grothendieck ∞-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 ∞-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 ∞-category is more general than previously assumed.