paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Constructing Higher Inductive Types as Groupoid Quotients

将高阶归纳类型构造为群胚商
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 2/10 · 该论文属于纯类型论与形式化验证，使用 Coq/UniMath 形式化高阶归纳类型构造，未涉及 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析，因此与研究方向仅有非常间接的关联。引用 1 inbox
Niels van der Weide
形式语义定理证明与证明工程
crossref: 2026-09-12

AI 速览

一句话：证明所有有限 1-截断高阶归纳类型都可由群胚商构造，并在 Coq/UniMath 中形式化。

论文研究单价类型论中高阶归纳类型（HITs）的构造与语义。作者首先在内部定义 HIT 的签名，并为每个签名构造以 1-type 和以 groupoid 为对象的代数双范畴，进而证明相应的初始代数语义。随后，论文证明 groupoid quotient 在两个代数双范畴之间诱导一个双伴随，并在 groupoid 代数双范畴中构造双初始对象。由此推出：所有有限 1-截断 HITs 都可以从 groupoid quotient 构造出来。全部结果均在 Coq 的 UniMath 单价数学库中形式化。

问题
在单价类型论中，如何用群胚商这一基本构造得到所有有限 1-截断高阶归纳类型，并给出其初始代数语义？
方法
在内部定义 HIT 签名；为每个签名构造 1-type 与 groupoid 中代数的双范畴，证明初始代数语义；证明群胚商诱导双伴随并构造群胚代数双范畴中的双初始对象；全部在 Coq/UniMath 中形式化。
评估
通过 Coq/UniMath 进行机器化证明，验证所有构造与语义结果的正确性。
原文摘要（Abstract）

In this paper, we show that all finitary 1-truncated higher inductive types (HITs) can be constructed from the groupoid quotient. We start by defining internally a 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. We finish by constructing a biinitial object in the bicategory of algebras in groupoids. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot5484,
  title = {Constructing Higher Inductive Types as Groupoid Quotients},
  author = {Niels van der Weide},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394803}
}