Constructive sheaf models of type theory
Abstract
We generalise sheaf models of intuitionistic logic to univalent type theory over a small category with a Grothendieck topology. We use in a crucial way that we have constructive models of univalence, that can then be relativized to any presheaf models, and these sheaf models are obtained by localisation for a left exact modality. We provide first an abstract notion of descent data which can be thought of as a higher version of the notion of prenucleus on frames, from which can be generated a nucleus (left exact modality) by transfinite iteration. We then provide several examples.
Cite
@article{arxiv.1912.10407,
title = {Constructive sheaf models of type theory},
author = {Thierry Coquand and Fabian Ruch and Christian Sattler},
journal= {arXiv preprint arXiv:1912.10407},
year = {2020}
}
Comments
Simplified the definition of lex operation, simplified the encoding of the homotopy limit and remark that the homotopy descent data is a lex modality without using higher inductive types