# Deloopable H-spaces

Content created by Egbert Rijke.

Created on 2024-03-23.

module higher-group-theory.deloopable-h-spaces where

Imports
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


## Idea

Consider an H-space with underlying pointed type (X , *) and with multiplication μ satisfying

   left-unit-law : (x : X) → μ * x ＝ x
right-unit-law : (x : X) → μ x * ＝ x
coh-unit-law : left-unit-law * ＝ right-unit-law *.


A delooping of the H-space X consists of an ∞-group G and an equivalence of H-spaces

  X ≃ h-space-∞-Group G.


## Definitions

### Deloopings of H-spaces of a given universe level

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

module _
{l1 : Level} (A : H-Space l1)
where

delooping-H-Space : UU (lsuc l1)
delooping-H-Space = delooping-H-Space-Level l1 A