nLab Higher Groups in Homotopy Type Theory

• Ulrik Buchholtz, Floris van Doorn, Egbert Rijke:

  Higher Groups in Homotopy Type Theory

  LICS ‘18:

  Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

  arXiv:1802.04315

  doi:10.1145/3209108.3209150

on infinity-groups in homotopy type theory.

Abtract. 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.

category: reference