1: \begin{abstract}

2:   We present a development of the theory of higher groups, including

3:   infinity groups and connective spectra, in homotopy type theory. An

4:   infinity group is simply the loops in a pointed, connected type,

5:   where the group structure comes from the structure inherent in the

6:   identity types of Martin-L{\"o}f type theory. We investigate

7:   ordinary groups from this viewpoint, as well as higher dimensional

8:   groups and groups that can be delooped more than once. A major result

9:   is the stabilization theorem, which states that if an $n$-type can be

10:   delooped $n+2$ times, then it is an infinite loop type. Most of the

11:   results have been formalized in the Lean proof assistant.

12: \end{abstract}