Constructive sheaf models of type theory. (18th October 2021) - Coquand, Thierry; Ruch, Fabian; Sattler, Christian
Abstract: We provide a constructive version of the notion of sheaf models of univalent type theory. We start by relativizing existing constructive models of univalent type theory to presheaves over a base category. Any Grothendieck topology of the base category then gives rise to a family of left-exact modalities, and we recover a model of type theory by localizing the presheaf model with respect to this family of left-exact modalities. We provide then some examples.