Higher Groups in Homotopy Type Theory

TL;DR

This paper develops the theory of higher groups within homotopy type theory, exploring their structures, properties, and the stabilization theorem, with formalization in the Lean proof assistant.

Contribution

It introduces a formalized framework for higher groups and infinity groups in homotopy type theory, including the stabilization theorem and multiple deloopings.

Findings

Higher groups are modeled as loops in pointed, connected types.

The stabilization theorem links deloopings to infinite loop types.

Most results are formalized in the Lean proof assistant.

Abstract

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\"of 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.