9 papers
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…
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…
Two Remarks about Game Semantics of Classical Logic
Thierry Coquand
We present and explain two unpublished remarks of Stefano Berardi connected to game semantics.
A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism
Marc Bezem, Thierry Coquand, Peter Dybjer +1
We present generalized algebraic theories corresponding to slightly modified versions of two of the type theories in our paper Type Theory with Explicit Universe Polymorphism. We f…
Local structure of etale algebras
Thierry Coquand
The goal of this note is to provide a constructive version of the proof of local structure of etale algebras.
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…