Homotopy Type Theory spectrum > history (Rev #4)

Idea

Definition

A spectrum (or $\Omega$-spectrum) is a prespectrum $E$ in which each pointed map $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?
• prespectrum

References

• HoTT book
• On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory