3 papers
math.AG2024
Univalent Foundations of Constructive Algebraic Geometry
Max Zeuner
We investigate two constructive approaches to defining quasi-compact and quasi-separated schemes (qcqs-schemes), namely qcqs-schemes as locally ringed lattices and as functors from…
math.AG2024
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…
math.LO2022
A Univalent Formalization of Constructive Affine Schemes
Max Zeuner, Anders Mörtberg
We present a formalization of constructive affine schemes in the Cubical Agda proof assistant. This development is not only fully constructive and predicative, it also makes crucia…