Classifying certain group extensions in HoTT

Homotopy type theory is a formal language for reasoning about spaces [6]. It has semantics in higher toposes [5]. One family of spaces which are of particular interest in contemporary (higher) category theory are the so-called higher groups. A higher group is a space $X$ equipped with a delooping, that is, a further space $Y$ and an equivalence $X\simeq (\mathrm{\Omega }Y)$ where $\mathrm{\Omega }Y$ is the loop-space of $Y$. In the setting of homotopy type theory, a particular class of higher groups, the central higher groups, was introduced by [1]. The central higher groups have many remarkable properties: for example, their deloopings are themselves central higher groups – which implies that the central higher groups can be delooped infinitely many times.

In this talk I will present a classification theorem for certain higher group extensions: extensions of truncated groups by central groups, in the setting of homotopy type theory. This builds on the work of Myers and Yasser on higher Schreier theory [3], and, as a special case, recovers a variant of the classical classification of $2$-groups by their Postnikov invariants due in different forms to Mac Lane-Whitehead, and Sính [2, 4].