Constructive sheaf models of type theory

TL;DR

This paper extends sheaf models of intuitionistic logic to univalent type theory, enabling constructive models of univalence over categories with Grothendieck topologies, and introduces a higher descent data framework.

Contribution

It introduces a novel framework for sheaf models of univalent type theory using constructive univalence models and higher descent data, generalizing previous models.

Findings

Constructive models of univalence can be relativized to presheaf and sheaf models.

A higher notion of descent data analogous to prenucleus is developed.

Several concrete examples of the generalized sheaf models are provided.

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.