HoTT 库：同伦类型论在 Coq 中的形式化
计算机科学中的逻辑
2017-05-02 v2 逻辑
摘要
我们报告 HoTT 库的开发，这是同伦类型论在 Coq 证明助手中的形式化。它形式化了同伦类型论的大部分基础内容，包括单值性、高阶归纳类型，以及大量的综合同伦论，还有范畴论和模态。该库已被用作若干独立开发的基础。我们讨论了导致该库设计的决策，并评论了同伦类型论与 Coq 最近引入的特性（如宇宙多态和私有归纳类型）之间的交互。
引用
@article{arxiv.1610.04591,
title = {The HoTT Library: A formalization of homotopy type theory in Coq},
author = {Andrej Bauer and Jason Gross and Peter LeFanu Lumsdaine and Mike Shulman and Matthieu Sozeau and Bas Spitters},
journal= {arXiv preprint arXiv:1610.04591},
year = {2017}
}