Types are Internal $\infty$-Groupoids
Types are Internal $\infty$-Groupoids
复制标题
类型是内部$infty$-Groupoids
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Matthieu Sozeau
中科院分区：
文献类型：
--
作者：
A. Allioux;Eric Finster;Matthieu Sozeau
通过将类型理论推广到具有确定结合和一元多项式单调的宇宙中，我们展示了如何得到一个能够编码许多完全相干的代数结构的opetoptopy型的定义。特别地，我们的方法引出了类型理论内部的$\inty$-群胚的定义，并证明了这种$\inty$-群胚的类型等价于类型的宇宙。也就是说，每种类型在内部都接受$\inty$-群组的结构，并且这种结构是唯一的。
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 $\infty$-groupoid internal to type theory and we prove that the type of such $\infty$-groupoids is equivalent to the universe of types. That is, every type admits the structure of an $\infty$-groupoid internally, and this structure is unique.
-作为分析单子的操作
影响因子：
1
作者：
Gepner, David;Haugseng, Rune;Kock, Joachim
通讯作者：
Kock, Joachim
影响因子：
1.1
作者：
Altenkirch, Thorsten;Ghani, Neil;Morris, Peter
通讯作者：
Morris, Peter