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

TL;DR

This paper explores the relationship between different foundations of $ abla$-category theory, showing that models of simplicial homotopy type theory are more diverse than just simplicial objects, indicating a broader notion of $ abla$-categories.

Contribution

It demonstrates that models of simplicial homotopy type theory extend beyond simplicial objects, challenging previous assumptions about their categorical representations.

Findings

Models of sHoTT are not limited to simplicial objects.

The notion of $ abla$-categories is more general than previously thought.

There exist models of sHoTT outside the simplicial framework.

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.