Iterated loop spaces
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-03-10.
Last modified on 2023-03-14.
module synthetic-homotopy-theory.iterated-loop-spaces where
Imports
open import elementary-number-theory.natural-numbers open import foundation.universe-levels open import structured-types.pointed-types open import synthetic-homotopy-theory.loop-spaces
module _ {l : Level} where iterated-loop-space : ℕ → Pointed-Type l → Pointed-Type l iterated-loop-space zero-ℕ A = A iterated-loop-space (succ-ℕ n) A = Ω (iterated-loop-space n A)
Recent changes
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).