nLab homotopy canonicity

Idea

A version of canonicity where the definitional equalities are replaced with identity types.

In the case for the natural numbers type homotopy canonicity states that every natural number $n:\mathbb{N}$ comes with a natural number $m:\mathbb{N}$ and an identification to the canonical form $p:n =_\mathbb{N} \mathrm{succ}^m(0)$.

Examples

• Chris Kapulkin and Christian Sattler have an unpublished proof that homotopy type theory has homotopy canonicity, even though HoTT does not have canonicity

• Rafaël Bocquet has a published proof that HoTT has homotopy canonicity

• cubical type theory has homotopy canonicity

References

• Michael Shulman, Univalence for inverse diagrams, oplax limits, and gluing, and homotopy canonicity (arXiv:1203.3253)

• Thierry Coquand, Simon Huber, Christian Sattler, Canonicity and homotopy canonicity for cubical type theory, Logical Methods in Computer Science, Volume 18, Issue 1 (February 3, 2022) lmcs:9043, (doi:10.46298/lmcs-18%281%3A28%292022, arXiv:1902.06572)

• Benno van den Berg, Martijn den Besten, Quadratic type checking for objective type theory (arXiv:2102.00905)

• Christian Sattler, Homotopy canonicity of homotopy type theory. Talk at the International Conference on Homotopy Type Theory 2019. (slides)

• Rafaël Bocquet, Strict Rezk completions of models of HoTT and homotopy canonicity, 2023, (arXiv:2311.05849)