同伦型理论中圆的基本群的计算
Calculating the Fundamental Group of the Circle in Homotopy Type Theory
摘要：
最近的工作同伦类型理论利用了一个令人兴奋的新的对应马丁-洛夫的依赖型理论和数学学科的范畴论和同伦理论。范畴论和同伦理论提出了新的原则，以增加类型论，类型论可以用新的方式来形式化这些数学领域。本文给出了代数拓扑学中的一个基本结果：圆的基本群是整数。虽然简单，这个例子是有趣的几个原因：它说明了同伦类型论的新原则;它混合了传统同伦理论证明的结果与类型理论归纳推理的想法;它提供了一个上下文来理解现有的类型理论难题-一个宇宙（类型）是必要的，以证明归纳类型的构造函数是不相交的和单射的。
英文摘要：
Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The category theory and homotopy theory suggest new principles to add to type theory, and type theory can be used in novel ways to formalize these areas of mathematics. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Though simple, this example is interesting for several reasons: it illustrates the new principles in homotopy type theory; it mixes ideas from traditional homotopy-theoretic proofs of the result with type-theoretic inductive reasoning; and it provides a context for understanding an existing puzzle in type theory---that a universe (type of types) is necessary to prove that the constructors of inductive types are disjoint and injective.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
