Spectra

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.spectra 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-equivalences
open import structured-types.pointed-types

open import synthetic-homotopy-theory.loop-spaces

Idea

A spectrum is an infinite sequence of pointed types A such that A n ≃∗ Ω (A (n+1)) for each n : ℕ.

Definition

Spectrum : (l : Level)  UU (lsuc l)
Spectrum l =
  Σ (  Pointed-Type l)  A  (n : )  A n ≃∗ Ω (A (succ-ℕ n)))

Recent changes