19 citations · 19 across the 6 of their papers we have counts for
6 papers
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…
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 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…
Families of Sets in Constructive Measure Theory
Max Zeuner
We present the first steps of a predicative reconstruction of the constructive Bishop-Cheng measure theory. Working in a semi-formal elaboration of Bishop's set theory and invoking…
Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory
Iosif Petrakis, Max Zeuner
Bishop's measure theory (BMT) is an abstraction of the measure theory of a locally compact metric space , and the use of an informal notion of a set-indexed family of complement…
Internalizing Representation Independence with Univalence
Carlo Angiuli, Evan Cavallo, Anders Mörtberg +1
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are rela…