2 citations · 3 across the 5 of their papers we have counts for
5 papers
Differential Geometry of Synthetic Schemes
Felix Cherubini, Matthias Hutzler, Hugo Moeneclaey +1
Synthetic algebraic geometry uses homotopy type theory extended with three axioms to develop algebraic geometry internal to a higher version of the Zariski topos. In this article w…
The Functor of Points Approach to Schemes in Cubical Agda
Max Zeuner, Matthias Hutzler
We present a formalization of quasi-compact and quasi-separated schemes (qcqs-schemes) in the Cubical Agda proof assistant. We follow Grothendieck's functor of points approach, whi…
A Foundation for Synthetic Algebraic Geometry
Felix Cherubini, Thierry Coquand, Matthias Hutzler
This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt. The Zariski topos consists of sheaves on the si…
Syntactic presentations for glued toposes and for crystalline toposes
Matthias Hutzler
We regard a geometric theory classified by a topos as a syntactic presentation for the topos and develop tools for finding such presentations. Extensions of geometric theories, whi…
A constructive Knaster-Tarski proof of the uncountability of the reals
Ingo Blechschmidt, Matthias Hutzler
We give an uncountability proof of the reals which relies on their order completeness instead of their sequential completeness. We use neither a form of the axiom of choice nor the…