立方类型理论的规范性同伦规范性
Canonicity and homotopy canonicity for cubical type theory
AI总结：
本文通过锥形论证，在预层模型内证明了立方类型理论的两个规范性结果：同伦规范性和规范性，分别在不使用和使用路径提升方程的情况下，确保每个自然数与数字路径相等。
摘要：
立方类型理论为同伦类型理论提供了构造性的辩护。立方类型理论的一个关键成分是路径提升操作，该操作通过类型上的归纳进行计算性解释，涉及若干非规范选择。本文提出了两个规范性结果，均通过锥形论证证明：一个同伦规范性结果，即每个自然数都与一个数字路径相等，即使我们去掉类型结构上定义提升操作的方程；以及一个规范性结果，该结果以关键方式使用这些方程。两个证明均在预层模型内部完成。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
