Univalence for inverse diagrams and homotopy canonicity

TL;DR

This paper develops a homotopical framework for inverse diagrams in type theory, leading to new models of univalence in higher toposes and partial progress on Voevodsky's homotopy-canonicity conjecture.

Contribution

It introduces a homotopical approach to inverse diagrams and applies it to construct new univalent models and address the homotopy-canonicity conjecture.

Findings

New models of univalence in (infinity,1)-toposes.

Partial proof of homotopy-canonicity for 1-truncated type theory.

Application of Reedy homotopy theory to type-theoretic contexts.

Abstract

We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory on inverse diagrams, and relies on the fact that Reedy fibrant diagrams correspond to contexts of a certain shape in type theory. This has two main applications. First, by considering inverse diagrams in Voevodsky's univalent model in simplicial sets, we obtain new models of univalence in a number of (infinity,1)-toposes; this answers a question raised at the Oberwolfach workshop on homotopical type theory. Second, by gluing the syntactic category of univalent type theory along its global sections functor to groupoids, we obtain a partial answer to Voevodsky's homotopy-canonicity conjecture: in 1-truncated type theory with one univalent universe of sets, any closed term of natural number type is homotopic to a numeral.