Deloopings and Eilenberg-Mac Lane spaces (#1079)

In this pull request we add:

- A definition of what it means for a pointed type to be deloopable
- A definition of what it means for an H-space to be deloopable
- A definition of Eilenberg-Mac Lane spaces

There were some universe level questions that one can ask about the type
of deloopings. One can show that the type of deloopings of `X` in
universe `l2` is equivalent to the type of deloopings of `X` in the
universe level of `X`. Showing the forward implication required me to do
some work on smallness of pointed types and higher groups, which is
included in this pull request.

Furthermore, the file about morphisms of H-spaces has been revamped, for
better formalization of the preservation of the coherence law. This was
needed for the notion of equivalence of H-spaces, which was prerequisite
to the notion of delooping of H-spaces.

src/foundation-core/small-types.lagda.md

@@ -195,6 +195,13 @@ pr1 (is-small-is-contr l H) = raise-unit l
 pr2 (is-small-is-contr l H) = equiv-is-contr H is-contr-raise-unit
 ```
 
+### The unit type is small with respect to any universe
+
+```agda
+is-small-unit : {l : Level} → is-small l unit
+is-small-unit = is-small-is-contr _ is-contr-unit
+```
+
 ### Small types are closed under dependent pair types
 
 ```agda

src/group-theory/groups.lagda.md

@@ -34,6 +34,7 @@ open import group-theory.semigroups
 open import lists.concatenation-lists
 open import lists.lists
 
+open import structured-types.h-spaces
 open import structured-types.pointed-types
 open import structured-types.pointed-types-equipped-with-automorphisms
 ```
@@ -158,10 +159,22 @@ module _
     (x : type-Group) → Id (mul-Group x unit-Group) x
   right-unit-law-mul-Group = pr2 (pr2 is-unital-Group)
 
+  coherence-unit-laws-mul-Group :
+    left-unit-law-mul-Group unit-Group ＝ right-unit-law-mul-Group unit-Group
+  coherence-unit-laws-mul-Group =
+    eq-is-prop (is-set-type-Group _ _)
+
   pointed-type-Group : Pointed-Type l
   pr1 pointed-type-Group = type-Group
   pr2 pointed-type-Group = unit-Group
 
+  h-space-Group : H-Space l
+  pr1 h-space-Group = pointed-type-Group
+  pr1 (pr2 h-space-Group) = mul-Group
+  pr1 (pr2 (pr2 h-space-Group)) = left-unit-law-mul-Group
+  pr1 (pr2 (pr2 (pr2 h-space-Group))) = right-unit-law-mul-Group
+  pr2 (pr2 (pr2 (pr2 h-space-Group))) = coherence-unit-laws-mul-Group
+
   has-inverses-Group :
     is-group-is-unital-Semigroup semigroup-Group is-unital-Group
   has-inverses-Group = pr2 is-group-Group

src/group-theory/wild-representations-monoids.lagda.md

@@ -69,7 +69,7 @@ module _
     ( ( action-wild-representation-type-Monoid x) ∘
       ( action-wild-representation-type-Monoid y))
   preserves-mul-action-wild-representation-type-Monoid =
-    preserves-mul-map-hom-Wild-Monoid
+    preserves-mul-hom-Wild-Monoid
       ( wild-monoid-Monoid M)
       ( endo-Wild-Monoid type-wild-representation-type-Monoid)
       ( hom-action-wild-representation-type-Monoid)

src/higher-group-theory.lagda.md

@@ -8,6 +8,10 @@ module higher-group-theory where
 open import higher-group-theory.cartesian-products-higher-groups public
 open import higher-group-theory.conjugation public
 open import higher-group-theory.cyclic-higher-groups public
+open import higher-group-theory.deloopable-groups public
+open import higher-group-theory.deloopable-h-spaces public
+open import higher-group-theory.deloopable-types public
+open import higher-group-theory.eilenberg-mac-lane-spaces public
 open import higher-group-theory.equivalences-higher-groups public
 open import higher-group-theory.fixed-points-higher-group-actions public
 open import higher-group-theory.free-higher-group-actions public
@@ -17,7 +21,9 @@ open import higher-group-theory.homomorphisms-higher-group-actions public
 open import higher-group-theory.homomorphisms-higher-groups public
 open import higher-group-theory.integers-higher-group public
 open import higher-group-theory.iterated-cartesian-products-higher-groups public
+open import higher-group-theory.iterated-deloopings-of-pointed-types public
 open import higher-group-theory.orbits-higher-group-actions public
+open import higher-group-theory.small-higher-groups public
 open import higher-group-theory.subgroups-higher-groups public
 open import higher-group-theory.symmetric-higher-groups public
 open import higher-group-theory.transitive-higher-group-actions public

src/higher-group-theory/deloopable-groups.lagda.md

@@ -0,0 +1,58 @@
+# Deloopable groups
+
+```agda
+module higher-group-theory.deloopable-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import group-theory.groups
+
+open import higher-group-theory.deloopable-h-spaces
+```
+
+</details>
+
+## Idea
+
+A {{#concept "delooping" Disambiguation="group" Agda=delooping-Group}} of a
+[group](group-theory.groups.md) `G` is a
+[delooping](higher-group-theory.deloopable-h-spaces.md) of the underlying
+[H-space](structured-types.h-spaces.md) of `G`. In other words, a delooping of a
+group `G` consists of a [higher group](higher-group-theory.higher-groups.md)
+`H`, which is defined to be a [pointed](structured-types.pointed-types.md)
+[connected](foundation.0-connected-types.md) type, equipped with an
+[equivalence of H-spaces](structured-types.equivalences-h-spaces.md)
+`G ≃ h-space-∞-Group H` from `G` to the underlying H-space of `H`.
+
+## Definitions
+
+### Deloopings of groups of a given universe level
+
+```agda
+module _
+  {l1 : Level} (l2 : Level) (G : Group l1)
+  where
+
+  delooping-Group-Level : UU (l1 ⊔ lsuc l2)
+  delooping-Group-Level = delooping-H-Space-Level l2 (h-space-Group G)
+```
+
+### Deloopings of groups
+
+```agda
+module _
+  {l1 : Level} (G : Group l1)
+  where
+
+  delooping-Group : UU (lsuc l1)
+  delooping-Group = delooping-Group-Level l1 G
+```
+
+## See also
+
+- [Eilenberg-Mac Lane spaces](higher-group-theory.eilenberg-mac-lane-spaces.md)

src/higher-group-theory/deloopable-h-spaces.lagda.md

@@ -0,0 +1,68 @@
+# Deloopable H-spaces
+
+```agda
+module higher-group-theory.deloopable-h-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import higher-group-theory.higher-groups
+
+open import structured-types.equivalences-h-spaces
+open import structured-types.h-spaces
+```
+
+</details>
+
+## Idea
+
+Consider an [H-space](structured-types.h-spaces.md) with underlying
+[pointed type](structured-types.pointed-types.md) `(X , *)` and with
+multiplication `μ` satisfying
+
+```text
+   left-unit-law : (x : X) → μ * x ＝ x
+  right-unit-law : (x : X) → μ x * ＝ x
+    coh-unit-law : left-unit-law * ＝ right-unit-law *.
+```
+
+A {{#concept "delooping" Disambiguation="H-space" Agda=delooping-H-Space}} of
+the H-space `X` consists of an [∞-group](higher-group-theory.higher-groups.md)
+`G` and an [equivalence of H-spaces](structured-types.equivalences-h-spaces.md)
+
+```text
+  X ≃ h-space-∞-Group G.
+```
+
+## Definitions
+
+### Deloopings of H-spaces of a given universe level
+
+```agda
+module _
+  {l1 : Level} (l2 : Level) (A : H-Space l1)
+  where
+
+  delooping-H-Space-Level : UU (l1 ⊔ lsuc l2)
+  delooping-H-Space-Level =
+    Σ (∞-Group l2) (λ G → equiv-H-Space A (h-space-∞-Group G))
+```
+
+### Deloopings of H-spaces
+
+```agda
+module _
+  {l1 : Level} (A : H-Space l1)
+  where
+
+  delooping-H-Space : UU (lsuc l1)
+  delooping-H-Space = delooping-H-Space-Level l1 A
+```
+
+## See also
+
+- [Deloopable groups](higher-group-theory.deloopable-groups.md)