Strict Rezk completions of models of HoTT and homotopy canonicity

2023/09/25 by Rafaël Bocquet, Bocquet, Rafaël · 1 citation
Mathematics · Medicine · #Advanced Topics in Algebra #Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic in Computer Science (cs.LO) #Pituitary Gland Disorders and Treatments

paper · pdf · doi:10.48550/arxiv.2311.05849

openalex publication_date 2023/09/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Cited by

• Extension Types for Free

Related

• The HoTT Library: A formalization of homotopy type theory in Coq
• Semi-simplicial Types in Logic-enriched Homotopy Type Theory
• The category of iterative sets in homotopy type theory and univalent foundations
• Canonicity and Computability in Homotopy Type Theory
• Rzk: a Proof Assistant for Synthetic ∞-Categories