构建高归纳类型作为群组合取
摘要：研究了同伦类型理论中有限一侧截断高阶归纳类型（HIT）。首先证明了所有这些类型都可以从群oid商构造出来。定义了HIT的内部签名的概念，并为每个签名构造了一种在1-类型和群oid中的代数的双范畴。然后证明了签名的初始代数语义。接下来，证明了群oid商在1-类型和群oid中的代数范畴之间存在一个双伴隶关系。然后在群oid代数的双范畴中构造了一个双初始对象，从而得到了所需的代数。据此，得出了所有有限一侧截断HIT都可以由群oid商构造出来的结论。 给出了使用我们的签名概念可以定义的几个HIT的例子。特别地，证明了每个签名都对应于一个由该签名自由生成的代数结构的HIT。还开始了在1-类型中通用代数的发展。证明了代数的双范畴具有PIE极限（即乘积，插入器和等均器），并证明了在1-类型中的第一个同构定理的一个版本。最后，通过利用通过群oid商构造HIT的方法，给出了一些HIT的基本群的另一种表征。所有结果都在Coq的UniMath库中的唯一性数学中进行了形式化。
作者：Niccol`o Veltri and Niels van der Weide
论文ID：2002.08150
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22