Homotopy Type Theory prespectrum > history (Rev #1)

Definition

A prespectrum is a sequence of pointed types? $E: \mathbb{Z} \to \mathcal{U}_*$ and a sequence of pointed maps $n:\mathbb{Z} \vdash e_n:E_n \to \Omega E_{n+1}$. Typically a prespectrum is denoted $E$ when it is clear.

See also

• spectrum
• chain complex?

References

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