spectrum

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 : \PreSpectrum} \prod_{n : \mathbb{Z}} \IsEquiv (e_n)$

- spectrification?
- homotopy group of spectrum?
- smash product of spectra?
- coproduct of spectra?
- product of spectra?
- Eilienberg-MacLane spectrum?
- Suspension spectrum?

- cohomology
- homology?
- spectral sequences
- synthetic homotopy theory?