4 papers
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…
Chatelet's Theorem in Synthetic Algebraic Geometry
Thierry Coquand, Hugo Moeneclaey
We prove a version of Chatelet's Theorem about Severi-Brauer variety having rational points in the setting of synthetic algebraic geometry. We work over an arbitrary base ring.
A Foundation for Synthetic Stone Duality
Felix Cherubini, Thierry Coquand, Freek Geerligs +1
The language of homotopy type theory has proved to be appropriate as an internal language for various higher toposes, for example with Synthetic Algebraic Geometry for the Zariski…