Homotopy Type Theory Electronic Seminar Talks, 2023-10-19
https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html
In this [1] joint work with Thierry Coquand and Matthias Hutzler, we develop a foundation for a synthetic treatment of algebraic geometry, which is much in the same spirit as synthetic differential geometry. The language we use for the synthetic reasoning is homotopy type theory together with a postulated ring and three axioms. Two of the axioms were already present in previous work of Blechschmidt and a weaker variant already in work of Kock.
Our third axiom, which we call "Zariski-local choice", postulates a local-triviality with respect to a topology called the Zariski-topology. Using this axiom, it is possible to compute cohomology groups which we define using internal Eilenbeg-MacLane spaces. In the talk, I will explain this central new feature of our setup and conclude with an overview of recent results in synthetic algebraic geometry.
[1] https://felix-cherubini.de/iag.pdf