将高阶归纳类型构造为群胚商
Constructing Higher Inductive Types as Groupoid Quotients
AI总结：
本文在同伦类型论中证明所有有限一截断高阶归纳类型可由群胚商构造，定义签名及代数双范畴，并给出例子、极限与第一同构定理，形式化于Coq。
摘要：
在本文中，我们在同伦类型论中研究有限的一截断高阶归纳类型（HITs）。我们首先证明所有这些类型都可以从群胚商构造出来。我们为HITs定义了一个内部的签名概念，并且对于每个签名，我们在1-类型和群胚中构造了一个代数双范畴。我们继续证明我们签名的初始代数语义。之后，我们证明群胚商在1-类型和群胚的代数双范畴之间诱导了一个双伴随。然后我们在群胚的代数双范畴中构造一个双初始对象，这给出了所需的代数。从所有这些，我们得出结论，所有有限的一截断HITs都可以从群胚商构造出来。我们给出了几个使用我们的签名概念可定义的HITs的例子。特别地，我们证明每个签名都对应一个HIT，该HIT对应于在其上自由生成的代数结构。我们还开始了1-类型中的泛代数的发展。我们证明了代数双范畴具有PIE极限，即积、插入子和等化子，并且我们证明了1-类型的第一同构定理的一个版本。最后，我们利用我们通过群胚商构造HITs的方法，给出了一些HITs的基本群的另一种刻画。所有结果都在Coq中的UniMath单值数学库中形式化。
英文摘要：
In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. We define an internal notion of signatures for HITs, and for each signature, we construct a bicategory of algebras in 1-types and in groupoids. We continue by proving initial algebra semantics for our signatures. After that, we show that the groupoid quotient induces a biadjunction between the bicategories of algebras in 1-types and in groupoids. Then we construct a biinitial object in the bicategory of algebras in groupoids, which gives the desired algebra. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. We present several examples of HITs which are definable using our notion of signature. In particular, we show that each signature gives rise to a HIT corresponding to the freely generated algebraic structure over it. We also start the development of universal algebra in 1-types. We show that the bicategory of algebras has PIE limits, i.e. products, inserters and equifiers, and we prove a version of the first isomorphism theorem for 1-types. Finally, we give an alternative characterization of the foundamental groups of some HITs, exploiting our construction of HITs via the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
