Iterated deloopings of pointed types

Content created by Egbert Rijke.

Created on 2024-03-23.
Last modified on 2024-03-23.

module higher-group-theory.iterated-deloopings-of-pointed-types where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.cartesian-product-types
open import foundation.connected-types
open import foundation.dependent-pair-types
open import foundation.truncation-levels
open import foundation.universe-levels

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

open import synthetic-homotopy-theory.iterated-loop-spaces

Idea

The type of n-fold deloopings of a pointed type X is the type

  Σ (Y : Pointed-Type), is-connected (n-1) Y × (Ωⁿ X ≃∗ Y).

Here, the pointed type Ωⁿ X is the n-th iterated loop space of X.

Definitions

The type of n-fold deloopings of a pointed type, with respect to a universe level

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

  iterated-delooping-Level : UU (l1 ⊔ lsuc l2)
  iterated-delooping-Level =
    Σ ( Pointed-Type l2)
      ( λ Y →
        ( is-connected (truncation-level-minus-one-ℕ n) (type-Pointed-Type Y)) ×
        ( iterated-loop-space n X ≃∗ Y))

The type of n-fold deloopings of a pointed type

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

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

Recent changes