# Homotopy Type Theory spectrum (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

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

 \Spectrum \equiv \sum_{E : \Spectrum} \prod_{n : \mathbb{Z}} \IsEquiv (e_n) e_n)

## Properties

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