Higher Groups in Homotopy Type Theory
Higher Groups in Homotopy Type Theory
复制标题
同伦类型论中的高级群
DOI：
10.1145/3209108.3209150
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
E. Rijke
中科院分区：
文献类型：
--
作者：
Ulrik Buchholtz;Floris van Doorn;E. Rijke
本文在同伦型理论中发展了高阶群理论，包括无穷群和联结谱。无穷群只是一个指向的连通类型中的环，其中群结构来自马丁-洛夫类型理论的单位类型中固有的结构。我们从这个角度研究普通的群体，以及高维群体和群体，可以不止一次地去圈。一个主要的结果是稳定性定理，它指出，如果一个n型可以去环n + 2次，那么它是一个无限循环类型。大部分结果已经在精益证明助手中正式化。
We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Löf type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an n-type can be delooped n + 2 times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.