立方类型论的正则性与同伦正则性
逻辑
2023-06-22 v6 计算机科学中的逻辑
摘要
立方类型论为同伦类型论提供了构造性辩护。立方类型论的一个关键要素是路径提升操作，该操作通过对类型上的归纳以计算方式解释，涉及若干非正则选择。我们在本文中给出两个正则性结果，均通过 sconing 论证证明：一个同伦正则性结果，即每个自然数都路径等于一个数值，即使我们去掉类型结构上定义提升操作的等式；以及一个正则性结果，它在关键处使用了这些等式。两个证明均在预层模型内部完成。
引用
@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}
}