## 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]]