HIGHER SCHREIER THEORY IN CUBICAL AGDA

Abstract 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.