论文标题
将较高的电感类型构建为群体素定型商
Constructing Higher Inductive Types as Groupoid Quotients
论文作者
论文摘要
在本文中，我们研究了同型类型理论中的1截断较高的归纳类型（hits）。首先，我们可以证明所有这些类型都可以从groupoid商中构建。我们为命中的签名定义了一个内部概念，对于每个签名，我们在1型和类固醇中构建了代数的生物。我们继续为我们的签名证明最初的代数语义。之后，我们表明类固醇的商在1型和群体素中诱导代数的生物学之间的双基因。然后，我们在组素的代数构造中构建一个生物对象，该对象给出了所需的代数。从所有这些中，我们得出结论，所有限制1截断的命中均可用Gloperoid商构建。 我们提供了几个命中示例，可以使用我们的签名概念来定义。特别是，我们表明，每个签名都会产生对应于它上面自由产生的代数结构的命中。我们还开始以1型的通用代数开发。我们表明，代数的生物具有PIE限制，即产品，插入器和等级，我们证明了1型的第一个同构定理的版本。最后，我们给出了一些热门单曲的创始人组的替代表征，从而利用了我们通过Groupoid商的命中构建。所有结果均在COQ中的单价数学图书馆中正式化。
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.
