高等归纳型的形式化与综合同伦理论
On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory
摘要：
本论文的目的是在同伦型理论的背景下提出综合同伦理论。我们将提出各种结果在这个框架中，最值得注意的是建设的Atiyah-Hirzebruch和塞尔谱序列的上同调，已完全正式的精益证明助手。
英文摘要：
The goal of this dissertation is to present synthetic homotopy theory in the setting of homotopy type theory. We will present various results in this framework, most notably the construction of the Atiyah-Hirzebruch and Serre spectral sequences for cohomology, which have been fully formalized in the Lean proof assistant.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
