Directed univalence for simplicial objects in an $\infty$-topos

Abstract

A fundamental component of homotopy type theory, a synthetic theory of $\infty$-groupoids, is Voevodsky's univalence axiom. Univalence characterizes the identity types in the universal fibration, a classifier for small type families: identity types in the universe are equivalent to types of equivalences. The directed univalence axiom plays a similar foundational role in simplicial type theory, a synthetic theory of $\infty$-categories. In its original form, which does not include universes or directed univalence, the simplicial type theory has semantics in categories of simplicial objects in an $\infty$-topos, with synthetic $\infty$-categories corresponding to internal $\infty$-categories. We verify that directed univalence holds in this semantic setting, constructing an equivalence between hom types in the universal left fibration and function types. In fact, we verify a higher version of this result, constructing an equivalence between homotopy coherent composites in the universal left fibration and composable sequences of functions between types. Using the technique of weighted limits, we reduce this theorem for simplicial objects in an arbitrary $\infty$-topos to calculations "on the left" with simplicial sets.