2019/12/22 by Coquand, Thierry, Ruch, Fabian, Sattler, Christian · 1 citation
#FOS: Mathematics #Logic (math.LO)
paper · doi:10.48550/arxiv.1912.10407
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.