arXiv · 2512.06025
A Note About Models of Synthetic Algebraic Geometry
Abstract
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 constructive and weak (same proof theoretic strength as dependent type theory with universes) meta theory.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Thierry Coquand, Jonas Hofer, Christian Sattler. 2025-12-04. A Note About Models of Synthetic Algebraic Geometry. https://arxiv.org/abs/2512.06025
Cite the original work for its findings. Save a collection to share your selection of sources.