同伦类型论中高阶归纳类型的路径空间
逻辑
2019-05-16 v2 计算机科学中的逻辑
摘要
等式类型的研究是同伦类型论的核心。刻画这些类型通常颇为棘手,并已发展出诸如编码-解码法等多种策略。我们证明了一个关于余等化子与推出等式类型的定理,令人联想到归纳原理且对任何截断层级均无限制。该结果使得直接推理某些等式类型成为可能,并通过消除辅助构造的必要性来简化既有证明。为展示这一点,我们给出计算圆的基本群(Licata 与 Shulman '13)以及推出保持嵌入这一事实的极简论证。此外,我们的研究暗示了一个更高版本的 Seifert-van Kampen 定理,且集合截断算子将其映射为标准 Seifert-van Kampen 定理(源于 Favonia 与 Shulman '16)。我们在证明助手 Lean 中提供了主要技术结果的形式化。
引用
@article{arxiv.1901.06022,
title = {Path Spaces of Higher Inductive Types in Homotopy Type Theory},
author = {Nicolai Kraus and Jakob von Raumer},
journal= {arXiv preprint arXiv:1901.06022},
year = {2019}
}
备注
v1: 23 pages; v2: 24 pages, small reformulations and reorganizations