This page compiles pointers related to:
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
(2018) 205-214
on -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 January 1, 2023 at 20:27:47. See the history of this page for a list of all contributions to it.