论高阶归纳类型与合成同伦理论的形式化
代数拓扑
2018-09-03 v1 计算机科学中的逻辑
逻辑
摘要
本学位论文的目标是在同伦类型论的框架下呈现合成同伦理论。我们将在此框架中给出若干结果，最值得注意的是为上同调构造 Atiyah-Hirzebruch 与 Serre 谱序列，这些已完全在 Lean 证明助手中形式化。
引用
@article{arxiv.1808.10690,
title = {On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory},
author = {Floris van Doorn},
journal= {arXiv preprint arXiv:1808.10690},
year = {2018}
}
备注
Dissertation, 146 pages