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 suspensions of pointed types

module synthetic-homotopy-theory.iterated-suspensions-of-pointed-types where

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.suspensions-of-pointed-types

Idea

Given a pointed type X and a natural number n, we can form the n-iterated suspension of X.

Definitions

The iterated suspension of a pointed type

iterated-suspension-Pointed-Type :
  {l : Level} (n : ℕ) → Pointed-Type l → Pointed-Type l
iterated-suspension-Pointed-Type n = iterate n suspension-Pointed-Type