Homotopy type theory (HoTT) enables reasoning about groups directly as the types of symmetries (automorphisms) of mathematical structures. The HoTT approach to groups—first put forward by Buchholtz, van Doorn, and Rijke—identifies a group with the type of objects of which it is the symmetries. This type is called the “delooping” of the group, taking a term from algebraic topology. This approach naturally extends the group theory to higher groups which have symmetries between symmetries, and so on. In this paper, we formulate and prove a higher version of Schreier’s classification of all group extensions of a given group. Specifically, we prove that extensions of a group G by a group K are classified by actions of G on a delooping of K. Our proof is formalized in Cubical Agda, a dependently typed programming language and proof assistant which implements HoTT.

Working in homotopy type theory, we introduce the notion of n-exactness for a short sequence $F\to E\to B$ of pointed types and show that any fiber sequence $F\hookrightarrow E \twoheadrightarrow B$ of arbitrary types induces a short sequence

that is n-exact at $\| E\|_{n-1}$. We explain how the indexing makes sense when interpreted in terms of n-groups, and we compare our definition to the existing definitions of an exact sequence of n-groups for $n=1,2$. As the main application, we obtain the long n-exact sequence of homotopy n-groups of a fiber sequence.