Canonicity and homotopy canonicity for cubical type theory

TL;DR

This paper proves two canonicity results for cubical type theory using a sconing argument within a presheaf model, demonstrating that natural numbers are path equal to numerals even without certain equations.

Contribution

It introduces two canonicity theorems for cubical type theory, including a homotopy canonicity result, using an internal sconing argument.

Findings

Homotopy canonicity: natural numbers are path equal to numerals.

Canonicity: equations on the lifting operation are crucial.

Proofs are conducted internally in a presheaf model.

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.