Groupoid-Valued Presheaf Models of Univalent Type Theory

Abstract

One main goal of this thesis is to study constructive models of type theory with one univalent universe that interpret types by “presheaves” of groupoids.

A starting point is the fact that the groupoid model can be defined in a constructive metatheory. Therefore, its definition relativizes to presheaf models over arbitrary small index categories. This way we obtain what we call “naive” presheaf groupoid models of type theory with one univalent universe and propositional truncation.

These naive presheaf groupoid models of univalent type theory can for instance be used to refute the principle of excluded middle. However, they seem inadequate for using univalent type theory as an internal language for groupoids varying over a category.

One inadequacy of these models is that levelwise surjections in general fail to be internally surjective in that the propositional truncations of their fibres are not contractible. The reason for this failure is that propositional truncation in these models captures global rather than levelwise inhabitation of a type.

To resolve the inadequacies of these models we refine their interpretation of types. The interpretation of types in the refined models will be restricted to presheaves of groupoids that satisfy a non-trivial patch condition to account for levelwise inhabited propositions being forced to be contractible.

That patch condition can be expressed as having an algebra structure for a particular kind of lex modality which we call a descent data operation. Such a lex modality is in particular a strictly functorial operation on types and terms that preserves unit and dependent sum types up to isomorphism.

In this thesis we develop the notion of descent data operation as an extension of type theory. In particular, we show that its algebras are closed under type formers so that they can be used in an internal model construction. We apply this construction to the concrete descent data operation on the naive presheaf groupoid models. Finally, we show that a map in the resulting models is indeed internally surjective if and only if it is levelwise surjective.