A Note About Models of Synthetic Algebraic Geometry
Logic
2025-12-09 v1
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.
Cite
@article{arxiv.2512.06025,
title = {A Note About Models of Synthetic Algebraic Geometry},
author = {Thierry Coquand and Jonas Hofer and Christian Sattler},
journal= {arXiv preprint arXiv:2512.06025},
year = {2025}
}