Sheaves in HoTT with applications to synthetic algebraic geometry

Abstract

In this talk we will give an overview of the machinery which was developed during the quest for constructive models of Synthetic Algebraic Geometry. We will avoid technical semantic considerations, and focus on what this machinery can give us, i.e. models of HoTT satisfying various additional axioms. The main applications so far are to build constructive models for synthetic algebraic geometry and synthetic Stone duality, leading to the synthetic study of Zariski sheaves and light condensed sets. We expect more applications in the future.
We will start by explaining how results from Thierry Coquand, Jonas Höfer and Christian Sattler can be used to work internally in classifying higher presheaf topoi. Their machinery takes as input an algebraic theory (e.g. the theory of rings) and as output gives a presheaf model of HoTT with a generic model (e.g. a generic ring) satisfying 3 axioms.
From these axioms we can give an internal definition for topologies and their associated sheaves. Given such an internal topology satisfying mild conditions, we will explain how to build a sheaf model of HoTT satisfying a variant of the presheaf axioms. This relies crucially on sheafification being a lex modality internal to HoTT.
We will then use this machinery to build 4 models of HoTT: the presheaf topos classifying rings, the Zariski topos, the étale topos and the fppf topos. We will contrast the additional axioms satisfied by each of these models, giving a new perspective on the ubiquitous use of these sheaf topoi in algebraic geometry.
We will conclude with some considerations on synthetic Stone duality, as well as on future applications and extensions of this framework.