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 point…