paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Types Are Internal ∞-Groupoids

类型是内部 ∞-群胚
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 1/10 · 该论文属于纯类型论与高阶范畴语义的基础研究，讨论类型内部的 ∞-群胚定义，未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析，与用户当前研究画像几乎没有交集。引用 0 inbox
Eric Finster, Antoine Allioux, Matthieu Sozeau
类型系统形式语义
crossref: 2026-09-12

AI 速览

一句话：通过多项式单子与 opetopic 类型，在类型论内部定义 ∞-群胚，并证明其与类型宇宙等价。

本文研究如何在类型论内部以完全一致的方式编码 ∞-群胚等高等代数结构。作者扩展类型论，引入一个由定义性结合且含单位的 polynomial monads 构成的宇宙，并由此给出 opetopic type 的定义，使其能够编码多种完全一致的代数结构。基于这一框架，作者在类型论内部定义了 ∞-群胚，并证明该 ∞-群胚的类型与类型宇宙等价。这意味着每个类型都在内部承认 ∞-群胚结构，并且这种结构是唯一的，从而建立了类型与内部 ∞-群胚之间的精确对应。

问题
如何在类型论内部以完全一致的方式编码 ∞-群胚等高等代数结构，并刻画类型与内部 ∞-群胚之间的关系。
方法
扩展类型论，引入定义性结合且含单位的 polynomial monads 宇宙，定义 opetopic type，并据此构造类型论内部的 ∞-群胚。
评估
证明类型论中 ∞-群胚的类型与类型宇宙等价，从而每个类型都唯一地具有内部 ∞-群胚结构。
原文摘要（Abstract）

By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode a number of fully coherent algebraic structures. In particular, our approach leads to a definition of ∞-groupoid internal to type theory and we prove that the type of such ∞-groupoids is equivalent to the universe of types. That is, every type admits the structure of an ∞-groupoid internally, and this structure is unique.

链接与引用

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

BibTeX 
@inproceedings{paperbot6174,
  title = {Types Are Internal ∞-Groupoids},
  author = {Eric Finster and Antoine Allioux and Matthieu Sozeau},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470541}
}