Thierry Coquand ; Simon Huber ; Christian Sattler - Canonicity and homotopy canonicity for cubical type theory

lmcs:6309 - Logical Methods in Computer Science, February 3, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:28)2022
Canonicity and homotopy canonicity for cubical type theoryArticle

Authors: Thierry Coquand ; Simon Huber ; Christian Sattler

    Cubical type theory provides a constructive justification of homotopy type theory. 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. We present in this article two canonicity results, both proved by a sconing argument: a homotopy canonicity result, every natural number is path equal to a numeral, even if we take away the equations defining the lifting operation on the type structure, and a canonicity result, which uses these equations in a crucial way. Both proofs are done internally in a presheaf model.


    Volume: Volume 18, Issue 1
    Published on: February 3, 2022
    Accepted on: December 23, 2021
    Submitted on: April 20, 2020
    Keywords: Mathematics - Logic,Computer Science - Logic in Computer Science

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1385 times.
    This article's PDF has been downloaded 627 times.