By a delooping of a space \(X\) we mean a connected pointed space \(Y\) such that \(X ≅ ΩY\). Using higher inductive types in HoTT, one can construct deloopings of 1-groups, i.e. sets with a group structure. This follows from the more general construction of Eilenberg-MacLane spaces [1].

Based on the fact that 1-groups can be delooped, one can define an \(∞\)-group to be a space that can be delooped. Classically, there are more concrete definitions of \(∞\)-groups, often as algebras of certain operads, but they are not directly replicable in HoTT. Examples of \(∞\)-groups that are not \(1\)-groups include matrix Lie Groups such as \(O(n)\), \(SO(n)\), \(U(n)\) and \(SU(n)\). Neither these groups themselves, nor their deloopings, have been constructed in HoTT, except for a few special cases (for example, \(U(1) = S^1\), \(SO(3) = ℝP^3\) and \(SU(2) = S^3\)).

Furthermore, there is no general technique that allows us to construct deloopings of such objects. In a way, this is to be expected, since we don’t yet know how to express their full \(∞\)-group structure in HoTT in way that is not simply exhibiting a delooping. Therefore, it is not yet known whether deloopings of \(S^3\) or \(ℝP^3\) exist in HoTT.

However, some special cases can be dealt with, for example, automorphism groups \(\mathsf{Aut}(X)\), for a type \(X\) in a universe \(\mathcal{U}\), defined as \(\mathsf{Aut}(X) :≡ (X =_{\mathcal{U}} X)\). In fact, if we define \(B\mathsf{Aut}(X)\) to be the image of the map \(1 → \mathcal{U}\) determined by \(X\), it is easy to see that \(ΩB\mathsf{Aut}(X) ≅ (X =_{\mathcal{U}} X) ≡ \mathsf{Aut}(X)\). These kinds of definitions are quite convenient, since they are only based on the existence of a univalent universe containing \(X\), and propositional truncation (needed to define images of maps). In particular, they do not require the existence of any other higher inductive type besides propositional truncation.

One downside is that this construction of \(B\mathsf{Aut}(X)\) raises the universe level, since it ends up being as large as the universe \(\mathcal{U}\), hence larger than \(X\) and \(\mathsf{Aut}(X)\). Furthermore, clearly not all \(∞\)-groups are of the form \(\mathsf{Aut}(X)\) for some space \(X\). On the other hand, we are not limited to considering only bare types \(X\), but we can look at automorphism groups in other categories. Using this observation, we can actually replicate the construction of Eilenberg-MacLane spaces of the form \(K(G,1)\) only using a univalent universe of sets and propositional truncation. The idea is to express any \(1\)-group \(G\) as the group of automorphism of an object in a univalent category, and then use the same construction as in the case of \(B\mathsf{Aut}(X)\).

Let \(G\) be a 1-group, i.e. a set with a group structure. A \(G\)-set is defined to be a set \(X\), together with a group homomorphism \({G}^{\mathrm{op}} → (X ≅ X)\). If \(g : G\) and \(x : X\), let \(x · g\) denote the result of the action of \(g\) on \(x\).

If \(X\) and \(Y\) are \(G\)-sets, and \(f : X → Y\) is a function, we say that \(f\) is equivariant if for all \(x : X\) and \(g : G\), we have that \(f(x) · g = f(x · g)\).

More abstractly, we can regard \(G\) as a category with one object, denoted \(\mathbf{B}G\), and define a \(G\)-set to be a presheaf on \(\mathbf{B}G\). Then an equivariant function is simply a natural transformation, and \(G\)-sets with equivariant functions form a univalent category \(G\text{-}\mathsf{Set}\). Note, however, that \(\mathbf{B}G\) itself is not univalent, unless \(G\) is the trivial group.

Clearly, \(G\) itself can be made into a \(G\)-set via its right multiplication action. We will use the notation \(\underline G\) to refer to \(G\) regarded as a \(G\)-set. Note that \(\underline G\) can be thought of as the representable presheaf corresponding to the unique object of \(\mathbf{B}G\). It then follows from the Yoneda lemma that there is an equivalence \(G ≅ G\text{-}\mathsf{Set}(\underline G, \underline G)\). Since \(\mathbf{B}G\) is a groupoid, the monoid of endomorphisms of \(\underline G\) is a group, which together with the previously stated equivalence and univalence of \(G\text{-}\mathsf{Set}\) implies that \(G ≅ (\underline G = \underline G)\).

Now let \(BG\) denote the image of the map \(1 → G\text{-}\mathsf{Set}\) corresponding to \(\underline G\). In other words, we factor the map \(1 → G\text{-}\mathsf{Set}\) into a \((-1)\)-connected map \(b : 1 → BG\) followed by a \((-1)\)-truncated map \(i : BG → G\text{-}\mathsf{Set}\). In particular, \(BG\) is pointed and connected, and we will denote its basepoint also by \(b\).

Now we can calculate: \[ \begin{aligned} & G ≅ \\ & (\underline G = \underline G) ≅ \\ & (i(b) = i(b)) ≅ \\ & (b = b) ≅ \\ & \Omega B G, \end{aligned} \]

which shows that \(BG\) is a delooping of \(G\).

I formalised the above construction of \(BG\) in agda. You can find it here.

References

[1]: Licata, Daniel R., and Eric Finster. 2014. “Eilenberg-MacLane Spaces in Homotopy Type Theory.” In Proceedings of the joint meeting of the twenty-third EACSL annual conference on Computer Science Logic (CSL) and the twenty-ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 66:1–66:9. CSL-Lics ’14. ACM. https://doi.org/10.1145/2603088.2603153.