一句话：证明所有有限1-截断高阶归纳类型均可由群胚商构造，并在Coq中形式化。
本文在同伦类型论中研究有限1-截断高阶归纳类型（HITs），目标是从群胚商统一构造此类类型。作者为HIT定义内部签名，对每个签名构造1-类型与群胚中的代数双范畴，并证明初始代数语义；进而证明群胚商在两类代数双范畴间诱导双伴随，并在群胚代数双范畴中构造双初始对象，从而得到目标代数。由此证明所有有限1-截断HITs均可由群胚商构造。文中给出多个HIT实例，包括由签名自由生成的代数结构，初步发展1-类型中的泛代数，证明代数双范畴具有PIE极限及第一同构定理的1-类型版本，并给出某些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.
@article{paperbot1319,
title = {Constructing Higher Inductive Types as Groupoid Quotients},
author = {Niccolò Veltri and Niels van der Weide},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 2},
year = {2021},
doi = {10.23638/lmcs-17(2:8)2021}
}