Iterated loop spaces

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-03-10.
Last modified on 2023-10-22.

module synthetic-homotopy-theory.iterated-loop-spaces where
Imports
open import elementary-number-theory.natural-numbers

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

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.

module _
  {l : Level}
  where

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

See also

Recent changes