Let A be a (nice) H-space. We will start by studying the moduli space of H-space structures on A, and in particular we will generalize a formula of Copeland and Arkowitz–Curjel for counting H-space structures on A. These considerations will lead us to define what we call central H-spaces, which are generalizations of Eilenberg–Mac Lane spaces. Centrality is a simple condition with remarkable consequences: it implies that A is an infinite loop space, in a unique way. Our proof of this crucially uses the notion of a univalent universe, which is a fundamental notion in homotopy type theory (HoTT) due to Voevodsky. This we will explain, and we will see how univalence enables us to write curious formulas for (iteratively) delooping both A and self-maps of A.

These results have been shown and formalized in HoTT, with which we will assume no familiarity. The work is joint with Ulrik Buchholtz, Dan Christensen, and Egbert Rijke.