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.

翻译：立方体类型理论为同质式理论提供了建设性的理由。 立方体类型理论的一个关键要素是路径提升操作, 由涉及若干非天性选择的诱导来计算解释。 我们在本条中给出了两种二次二次二次曲线结果, 两者都由一个趋同的争论所证明: 单质式大通性结果, 每个自然数字都等于数字路径, 即使我们删除了定义类型结构上升动操作的方程式, 以及一个以关键方式使用这些方程式的罐头结果。 两种证据都是在预壳模型中内部完成的 。