Iterated suspensions of pointed types

Content created by Fredrik Bakke.

Created on 2023-10-12.
Last modified on 2023-10-12.

module synthetic-homotopy-theory.iterated-suspensions-of-pointed-types 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.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

Recent changes