Homotopy Type Theory spectrum > history (Rev #2)

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.

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