Constructive sheaf models of type theory. (18th October 2021)

• Record Type: Journal Article
• Authors: Coquand, Thierry; Ruch, Fabian; Sattler, Christian
• Is Part Of: Mathematical structures in computer science. Volume 31:Number 9(2021)
• Page Start: 979
• Page End: 1002
• Publication Date: 2021-10-18
• Subjects: Dependent type theory -- homotopy type theory -- sheaf models -- constructive models of univalence -- left-exact modalities; Computer science -- Mathematics -- Periodicals; 004.015105
• DOI: 10.1017/S0960129521000359
• Languages: English
• ISSNs: 0960-1295

Abstract

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.