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

Evan Cavallo, Emily Riehl, Christian Sattler

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 unive…