Homotopy Type Theory spectrum (changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

Definition

A prespectrum spectrum is (or a sequence ofpointed types?$\Omega$ -$E: \mathbb{Z} \to \mathcal{U}_*$spectrum ) and is a sequence of pointed maps$e : (n : \mathbb{Z}) \to E_n \to \Omega E_{n+1}$prespectrum . Typically a prespectrum is denoted$E$ when in it which is each clear. pointed map$e_n$ is an equivalence.

A spectrum (or $\Omega$-spectrum) is a prespectrum in which each $e_n$ is an equivalence.

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

Properties

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