Canonicity and homotopy canonicity for cubical type theory
Logic
2023-06-22 v6 Logic in Computer Science
Abstract
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.
Keywords
Cite
@article{arxiv.1902.06572,
title = {Canonicity and homotopy canonicity for cubical type theory},
author = {Thierry Coquand and Simon Huber and Christian Sattler},
journal= {arXiv preprint arXiv:1902.06572},
year = {2023}
}