Contents

# Contents

## Idea

This entry is about the formulation of sequential spectra in homotopy type theory, specifically of sequential spectra that need not be genuine stable homotopy types in the sense of Omega-spectra and thus may be regarded as “pre-spectra” (they become genuine spectra under spectrification).

## Definition

In homotopy type theory, a prespectrum or sequential spectrum is a dependent bi-infinite sequence of types $n:\mathbb{Z} \vdash E_n\;\mathrm{type}$ with a dependent bi-infinite sequence of types $n \colon \mathbb{Z} \vdash *_n \colon E_n$ and a dependent bi-infinite sequence of functions $n \colon \mathbb{Z} \vdash e_n \colon E_n \to \Omega E_{n+1}$ which preserves the point, where $\Omega A$ is the loop space type of $A$.

In Coq pseudocode, this becomes

Definition prespectrum :=
{X \colon int -> Type &
{ pt \colon forall n, X n &
{ glue \colon forall n, X n -> pt (S n) == pt (S n) &
forall n, glue n (pt n) == idpath (pt (S n)) }}}.