On synthetic algebraic geometry:
Ingo Blechschmidt: Using the internal language of toposes in algebraic geometry, talk at Toposes at IHES (November 2015) [pdf, recording]
Ingo Blechschmidt: Using the internal language of toposes in algebraic geometry, PhD thesis (2017) [original:pdf, arXiv:2111.03685]
On constructive algebra:
Introduction to the Agda proof assistant:
An online Agda interface:
Last revised on May 2, 2026 at 13:06:48. See the history of this page for a list of all contributions to it.