## Idea ## Definition A **prespectrum** is a sequence of [[pointed types]] $E: \mathbb{Z} \to \mathcal{U}_*$ and a sequence of pointed maps $e : (n : \mathbb{Z}) \to E_n \to \Omega E_{n+1}$. Typically a prespectrum is denoted $E$ when it is clear. A **spectrum** (or $\Omega$-**spectrum**) is a prespectrum in which each $e_n$ is an equivalence. $$\Spectrum \equiv \sum_{E : \Spectrum} \prod_{n : \mathbb{Z}} \IsEquiv e_n)$$ ## Properties * [[spectrification]] * [[homotopy group of spectrum]] * [[smash product of spectra]] * [[coproduct of spectra]] * [[product of spectra]] * [[Eilienberg-MacLane spectrum]] * [[Suspension spectrum]] ## See also * [[cohomology]] * [[homology]] * [[spectral sequences]] * [[synthetic homotopy theory]] ## References * [[HoTT book]] * [[On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory]]