Homotopy Type Theory
Higher Groups in Homotopy Type Theory (Rev #1, changes)

Showing changes from revision #0 to #1: Added | Removed | Changed

Higher Groups in Homotopy Type Theory, Ulrik Buchholtz, Floris van Doorn, Egbert Rijke



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

Revision on January 19, 2019 at 13:10:56 by Ali Caglayan. See the history of this page for a list of all contributions to it.