4 papers
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…
Eliminating reversals from cubical type theories
Evan Cavallo, Christian Sattler
Cubical type theories are designed around an abstract unit interval from which types of paths, used to represent equalities, are defined. Varying the operations available on this i…
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…
The algebraic small object argument as a saturation
Evan Cavallo, Christian Sattler
We analyze the structure of left maps in algebraic weak factorization systems constructed using Garner's algebraic small object argument. We find that any left map can be construct…