This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Iterated loop spaces

module synthetic-homotopy-theory.iterated-loop-spaces where

open import elementary-number-theory.natural-numbers

open import foundation.iterating-functions
open import foundation.universe-levels

open import structured-types.h-spaces
open import structured-types.pointed-types

open import synthetic-homotopy-theory.loop-spaces

Idea

An iterated loop space Ωⁿ A is the pointed type obtained by n times iterating the loop space functor Ω : Pointed-Type → Pointed-Type.

Definitions

Iterated loop spaces

module _
  {l : Level}
  where

  iterated-loop-space : ℕ → Pointed-Type l → Pointed-Type l
  iterated-loop-space n = iterate n Ω

Iterated loop spaces of H-spaces

module _
  {l : Level}
  where

  iterated-loop-space-H-Space : ℕ → H-Space l → H-Space l
  iterated-loop-space-H-Space zero-ℕ X = X
  iterated-loop-space-H-Space (succ-ℕ n) X =
    Ω-H-Space (iterated-loop-space n (pointed-type-H-Space X))

See also

• Double loop spaces
• Triple loop spaces