2026-08-05T19:36:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10518 2024-03-06T10:46:07Z ddc:004 open_access

Homotopy Canonicity for Cubical Type Theory Coquand, Thierry Huber, Simon Sattler, Christian cubical type theory univalence canonicity sconing Artin glueing Cubical type theory provides a constructive justification of homotopy type theory and satisfies canonicity: every natural number is convertible to a numeral. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. In this paper we show by a sconing argument that if we remove these equations for the path lifting operation from the system, we still retain homotopy canonicity: every natural number is path equal to a numeral. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thierry Coquand and Simon Huber and Christian Sattler 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.11 urn:nbn:de:0030-drops-105188 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.11 eng https://creativecommons.org/licenses/by/3.0/legalcode