This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The sphere prespectrum

module synthetic-homotopy-theory.sphere-prespectrum where

open import foundation.dependent-pair-types
open import foundation.universe-levels

open import synthetic-homotopy-theory.prespectra
open import synthetic-homotopy-theory.suspension-prespectra

open import univalent-combinatorics.standard-finite-types

Idea

The spheres Sⁿ define a prespectrum

  Sⁿ →∗ ΩSⁿ⁺¹

which we call the sphere prespectrum.

Note: Even though the sphere prespectrum is defined degreewise by the adjoint to the identity map, it is not in general a spectrum, as the transposing map of the loop-suspension adjunction does not generally send equivalences to equivalences.

Definition

The sphere prespectrum

sphere-Prespectrum : Prespectrum lzero
sphere-Prespectrum = suspension-Prespectrum (Fin  , zero-Fin )