References & Citations
Mathematics > Logic
Title: Constructive sheaf models of type theory
(Submitted on 22 Dec 2019 (v1), last revised 8 Jul 2020 (this version, v4))
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.
Submission history
From: Thierry Coquand [view email][v1] Sun, 22 Dec 2019 10:02:06 GMT (17kb)
[v2] Wed, 19 Feb 2020 16:53:09 GMT (33kb)
[v3] Tue, 14 Apr 2020 19:06:42 GMT (34kb)
[v4] Wed, 8 Jul 2020 07:42:54 GMT (43kb)
Link back to: arXiv, form interface, contact.