3 papers
math.CT2026
Directed univalence for simplicial objects in an -topos
Evan Cavallo, Emily Riehl, Christian Sattler
A fundamental component of homotopy type theory, a synthetic theory of -groupoids, is Voevodsky's univalence axiom. Univalence characterizes the identity types in the unive…
math.CT2025
Synthetic perspectives on spaces and categories
Emily Riehl
Recently discovered domain-specific formal systems -- specifically homotopy type theory and simplicial type theory -- provide new perspectives on spaces and categories in a nativel…
math.AT2024
The equivariant model structure on cartesian cubical sets
Steve Awodey, Evan Cavallo, Thierry Coquand +2
We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves…