Prespectra
Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.
Created on 2022-05-16.
Last modified on 2023-05-03.
module synthetic-homotopy-theory.prespectra where
Imports
open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types open import foundation.universe-levels open import structured-types.pointed-maps open import structured-types.pointed-types open import synthetic-homotopy-theory.loop-spaces
Idea
A prespectrum is a sequence of pointed types A n
equipped with pointed maps
ε : A n →∗ Ω (A (n+1))
.
Definition
Prespectrum : (l : Level) → UU (lsuc l) Prespectrum l = Σ (ℕ → Pointed-Type l) (λ A → (n : ℕ) → A n →∗ Ω (A (succ-ℕ n)))
Recent changes
- 2023-05-03. Fredrik Bakke. Define the smash product of pointed types and refactor pointed types (#583).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 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).