# Deloopable types

Content created by Egbert Rijke.

Created on 2024-03-23.

module higher-group-theory.deloopable-types where

Imports
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.small-types
open import foundation.universe-levels

open import higher-group-theory.equivalences-higher-groups
open import higher-group-theory.higher-groups
open import higher-group-theory.small-higher-groups

open import structured-types.pointed-equivalences
open import structured-types.pointed-types
open import structured-types.small-pointed-types


## Idea

Consider a pointed type X and a pointed connected type Y. We say that Y is a delooping of X if we have a pointed equivalence

  X ≃∗ Ω Y.


Recall that a pointed connected type is an ∞-group. An ∞-group G is therefore a delooping of X if its underlying pointed type is pointed equivalent to X. A delooping of X therefore consist of an ∞-group G and a pointed equivalence

  X ≃∗ type-∞-Group G


In other words, the type of deloopings of X is defined to be

  delooping X := Σ (Y : ∞-Group), X ≃∗ Ω Y.


### Relation to higher group structures

A delooping of a pointed type X is, in quite a literal way, an ∞-group structure on X. In other words, the type delooping X is the type of ∞-group structures on X. Indeed, the type of all pointed types equipped with deloopings is equivalent to the type of ∞-groups, by extensionality of the type of pointed types.

Being deloopable is therefore a structure, and usually not a property. If there are multiple distinct ways to equip a pointed type X with the structure of an ∞-group, or even with the structure of a group, then the type of deloopings of X will not be a proposition. For instance, the standard 4-element type Fin 4 is deloopable in multiple distinct ways, by equipping it with the cyclic group structure of ℤ₄ or by equipping it with the group structure of ℤ₂ × ℤ₂.

### Universe levels in the definition of being deloopable

Note that there is a small question about universe levels in the definition of being a deloopable type. We say that a type is deloopable in a universe 𝒰 if there is an ∞-group Y in the universe 𝒰 that is a delooping of X. However, by the type theoretic replacement principle it follows that any delooping of X is always small with respect to the universe of X itself. Therefore we simply say that X is deloopable, i.e., without reference to any universes, if X is deloopable in its own universe.

## Definitions

### The predicate of being a delooping

module _
{l1 l2 : Level} (X : Pointed-Type l1)
where

is-delooping : (G : ∞-Group l2) → UU (l1 ⊔ l2)
is-delooping G = X ≃∗ pointed-type-∞-Group G


### The type of deloopings of a pointed type, in a given universe

module _
{l1 : Level} (X : Pointed-Type l1)
where

delooping-Level : (l : Level) → UU (l1 ⊔ lsuc l)
delooping-Level l = Σ (∞-Group l) (is-delooping X)

module _
{l : Level} (Y : delooping-Level l)
where

∞-group-delooping-Level : ∞-Group l
∞-group-delooping-Level = pr1 Y

classifying-pointed-type-∞-group-delooping-Level : Pointed-Type l
classifying-pointed-type-∞-group-delooping-Level =
classifying-pointed-type-∞-Group ∞-group-delooping-Level

classifying-type-∞-group-delooping-Level : UU l
classifying-type-∞-group-delooping-Level =
classifying-type-∞-Group ∞-group-delooping-Level

is-delooping-delooping-Level : is-delooping X ∞-group-delooping-Level
is-delooping-delooping-Level = pr2 Y

equiv-is-delooping-delooping-Level :
type-Pointed-Type X ≃ type-∞-Group ∞-group-delooping-Level
equiv-is-delooping-delooping-Level =
equiv-pointed-equiv is-delooping-delooping-Level


### The type of deloopings of a pointed type

module _
{l1 : Level} (X : Pointed-Type l1)
where

delooping : UU (lsuc l1)
delooping = delooping-Level X l1


## Properties

### The delooping of a pointed type in a universe 𝒰 is a 𝒰-small ∞-group

module _
{l1 l2 : Level} (X : Pointed-Type l1) (H : delooping-Level X l2)
where

abstract
is-small-∞-group-delooping-Level :
is-small-∞-Group l1 (∞-group-delooping-Level X H)
pr1 is-small-∞-group-delooping-Level = type-Pointed-Type X
pr2 is-small-∞-group-delooping-Level =
inv-equiv (equiv-is-delooping-delooping-Level X H)

abstract
is-small-classifying-type-∞-group-delooping-Level :
is-small l1 (classifying-type-∞-group-delooping-Level X H)
is-small-classifying-type-∞-group-delooping-Level =
is-small-classifying-type-is-small-∞-Group
( ∞-group-delooping-Level X H)
( is-small-∞-group-delooping-Level)

abstract
is-pointed-small-classifying-pointed-type-∞-group-delooping-Level :
is-pointed-small-Pointed-Type l1
( classifying-pointed-type-∞-group-delooping-Level X H)
is-pointed-small-classifying-pointed-type-∞-group-delooping-Level =
is-pointed-small-is-small-Pointed-Type
( classifying-pointed-type-∞-group-delooping-Level X H)
( is-small-classifying-type-∞-group-delooping-Level)


### If a pointed type in universe 𝒰 l1 is deloopable in any universe, then it is deloopable in 𝒰 l1

Suppose X is a pointed type of universe level l1, which is deloopable in universe level l2. Then there is an ∞-group H of universe level l2 equipped with a pointed equivalence

  X ≃∗ type-∞-Group H.


This implies that the ∞-group H is l1-small, because its underlying type is equivalent to the underlying type of X. Hence there is an ∞-group K equipped with an equivalence of ∞-groups

  H ≃ K.

module _
{l1 l2 : Level} (X : Pointed-Type l1) (H : delooping-Level X l2)
where

∞-group-delooping-delooping-level : ∞-Group l1
∞-group-delooping-delooping-level =
∞-group-is-small-∞-Group
( ∞-group-delooping-Level X H)
( type-Pointed-Type X ,
equiv-inv-pointed-equiv (is-delooping-delooping-Level X H))

is-delooping-delooping-delooping-Level :
is-delooping X ∞-group-delooping-delooping-level
is-delooping-delooping-delooping-Level =
comp-pointed-equiv
( pointed-equiv-equiv-∞-Group
( ∞-group-delooping-Level X H)
( ∞-group-delooping-delooping-level)
( equiv-∞-group-is-small-∞-Group
( ∞-group-delooping-Level X H)
( type-Pointed-Type X ,
equiv-inv-pointed-equiv (is-delooping-delooping-Level X H))))
( is-delooping-delooping-Level X H)

delooping-delooping-Level : delooping X
pr1 delooping-delooping-Level = ∞-group-delooping-delooping-level
pr2 delooping-delooping-Level = is-delooping-delooping-delooping-Level