Strict Rezk completions of models of HoTT and homotopy canonicity

TL;DR

This work provides a constructive proof of homotopy canonicity for HoTT by internalizing gluing along a strict Rezk completion of HoTT syntax inside the topos of cartesian cubical sets. The completion, denoted $\overline{\mathcal{S}}$, is built as the free extension of the syntax by extension structures and shown to have fibrant components and completeness, enabling a homotopical global sections functor and a gluing argument that yields canonicity. The construction parallels Rezk completions for categories but requires two-level (strict) equalities, made possible by cubical set semantics, and it yields a bridge between set-valued and space-valued perspectives without invoking higher-categorical machinery. The results include an Agda formalization and suggest broad applicability to generalized algebraic theories, potentially generalizing to De Morgan cubical sets and beyond, with ongoing work on stability of extension structures and broader applications of strict Rezk completions to coherence problems in type theory.

Abstract

We give a new constructive proof of homotopy canonicity for homotopy type theory (HoTT). Canonicity proofs typically involve gluing constructions over the syntax of type theory. We instead use a gluing construction over a "strict Rezk completion" of the syntax of HoTT. The strict Rezk completion is specified and constructed in the topos of cartesian cubical sets. It completes a model of HoTT to an equivalent model satisfying a completeness condition, providing an equivalence between terms of identity types and cubical paths between terms. This generalizes the ordinary Rezk completion of a 1-category.

Theorems & Definitions (136)

• Lemma 2.1: CanonicityCubical
• Definition 2.2
• Lemma 2.3
• Definition 2.4
• Proposition 2.5: CCHM17
• proof
• Lemma 2.6
• proof
• Lemma 2.7
• proof