{"id":"arxiv/2607.02420","url":"https://arxiv.org/abs/2607.02420","tags":["math.CT","math.AT"],"score":0,"title":"Directed univalence for simplicial objects in an $\\infty$-topos","domain":"math.CT","source":"arxiv","authors":["Evan Cavallo","Emily Riehl","Christian Sattler"],"reviews":0,"subject":"math.CT","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-07-02","reactions":{}}