Contents

# Contents

## Idea

This entry is about the formulation of Omega-spectra in homotopy type theory, i.e. sequential spectrum types that are stable homotopy types.

## Definition

In homotopy type theory, a spectrum or $\Omega$-spectrum is a sequential spectrum type $E$ in which each pointed map $e_n$ is an equivalence.

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