5 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…
Constructive higher sheaf models with applications to synthetic mathematics
Thierry Coquand, Jonas Höfer, Christian Sattler
There have recently been several developments in synthetic mathematics using extensions of dependent type theory with univalence and higher inductive types: simplicial homotopy typ…
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…
A Note About Models of Synthetic Algebraic Geometry
Thierry Coquand, Jonas Hofer, Christian Sattler
We show how to build models of Synthetic Algebraic Geometry over rings k such that finitely presented k-algebra have a decidable equality. The construction is done in a constructiv…