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.

We study the $E_2$ -algebra $\Lambda \mathfrak {M}_{*,1}:= \coprod _{g\geqslant 0}\Lambda \mathfrak {M}_{g,1}$ consisting of free loop spaces of moduli spaces of Riemann surfaces with one parametrised boundary component, and compute the homotopy type of the group completion $\Omega B\Lambda \mathfrak {M}_{*,1}$ : it is the product of $\Omega ^{\infty }\mathbf {MTSO}(2)$ with a certain free $\Omega ^{\infty }$ -space depending on the family of all boundary-irreducible mapping classes in all mapping class groups $\Gamma _{g,n}$ with $g\geqslant 0$ and $n\geqslant 1$ .

We study quotients of mapping class groups ${\Gamma _{g,1}}$ of oriented surfaces with one boundary component by the subgroups ${{\cal I}_{g,1}}(k)$ in the Johnson filtrations, and we show that the stable classifying spaces ${\mathbb {Z}} \times B{({\Gamma _\infty }/{{\cal I}_\infty }(k))^ + }$ after plus-construction are infinite loop spaces, fitting into a tower of infinite loop space maps that interpolates between the infinite loop spaces ${\mathbb {Z}} \times B\Gamma _\infty ^ + $ and ${\mathbb {Z}} \times B{({\Gamma _\infty }/{{\cal I}_\infty }(1))^ + } \simeq {\mathbb {Z}} \times B{\rm{Sp}}{({\mathbb {Z}})^ + }$ . We also show that for each level k of the Johnson filtration, the homology of these quotients with suitable systems of twisted coefficients stabilises as the genus of the surface goes to infinity.

For a path connected space X, the homology algebra $H_*(QX; \mathbb{Z}/2)$ is a polynomial algebra over certain generators QIx. We reinterpret a technical observation, of Curtis and Wellington, on the action of the Steenrod algebra A on the Λ algebra in our terms. We then introduce a partial order on each grading of H*QX which allows us to separate terms in a useful way when computing the action of dual Steenrod operations $Sq^i_*$ on $H_*(QX; \mathbb{Z}/2)$. We use these to completely characterise the A-annihilated generators of this polynomial algebra. We then propose a construction for sequences I so that QIx is A-annihilated. As an application, we offer some results on the form of potential spherical classes in H*QX upon some stability condition under homology suspension. Our computations provide new numerical conditions in the context of hit problem.

Dendroidal sets have been introduced as a combinatorial model for homotopy coherent operads. We introduce the notion of fully Kan dendroidal sets and show that there is a model structure on the category of dendroidal sets with fibrant objects given by fully Kan dendroidal sets. Moreover we show that the resulting homotopy theory is equivalent to the homotopy theory of connective spectra.