Back to Search
Start Over
Constructive sheaf models of type theory
- Source :
- Mathematical Structures in Computer Science. 31:979-1002
- Publication Year :
- 2021
- Publisher :
- Cambridge University Press (CUP), 2021.
-
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.<br />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
- Subjects :
- Pure mathematics
Presheaf
Mathematics - Logic
Intuitionistic logic
Constructive
Computer Science Applications
Mathematics (miscellaneous)
Type theory
Grothendieck topology
Mathematics::Category Theory
FOS: Mathematics
Sheaf
Logic (math.LO)
Computer Science::Databases
Transfinite number
Descent (mathematics)
Mathematics
Subjects
Details
- ISSN :
- 14698072 and 09601295
- Volume :
- 31
- Database :
- OpenAIRE
- Journal :
- Mathematical Structures in Computer Science
- Accession number :
- edsair.doi.dedup.....3be0e41b616f3cad6037024cc82e58a3