19 citations · 19 across the 6 of their papers we have counts for
Showing math.LOShow all
3 papers · 1 filter
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…
math.LO2022
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…
math.LO2022
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…