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
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 times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.
Last revised on June 9, 2022 at 13:17:09. See the history of this page for a list of all contributions to it.