一句话：在预层模型中以 sconing 论证证明立方类型理论的同伦典范性与典范性。
立方类型理论为同伦类型论提供构造性解释，其关键要素是路径提升操作；该操作按类型归纳计算，并涉及若干非典范选择。本文研究该理论的典范性，即每个自然数都路径等于一个数字。作者在预层模型中内部使用 sconing 论证，给出两个结果：一是同伦典范性，即使去掉类型结构上定义提升操作的等式，每个自然数仍路径等于一个数字；二是通常的典范性，其中这些等式在证明中起关键作用。两个证明均在预层模型内部完成。
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.
@article{paperbot1726,
title = {Canonicity and homotopy canonicity for cubical type theory},
author = {Thierry Coquand and Simon Huber and Christian Sattler},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:28)2022}
}