# Prespectra

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-05-16.

module synthetic-homotopy-theory.prespectra where

Imports
open import elementary-number-theory.natural-numbers

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

open import structured-types.pointed-maps
open import structured-types.pointed-types

open import synthetic-homotopy-theory.loop-spaces
open import synthetic-homotopy-theory.suspensions-of-pointed-types
open import synthetic-homotopy-theory.suspensions-of-types
open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types


## Idea

A prespectrum is a sequence of pointed types Aₙ equipped with pointed maps

  ε : Aₙ →∗ ΩAₙ₊₁


for each n : ℕ, called the adjoint structure maps of the prespectrum.

By the loop-suspension adjunction, specifying structure maps Aₙ →∗ Ω Aₙ₊₁ is equivalent to specifying their adjoint maps

  ΣAₙ → Aₙ₊₁.


## Definition

Prespectrum : (l : Level) → UU (lsuc l)
Prespectrum l =
Σ (ℕ → Pointed-Type l) (λ A → (n : ℕ) → A n →∗ Ω (A (succ-ℕ n)))

module _
{l : Level} (A : Prespectrum l) (n : ℕ)
where

pointed-type-Prespectrum : Pointed-Type l
pointed-type-Prespectrum = pr1 A n

type-Prespectrum : UU l
type-Prespectrum = type-Pointed-Type pointed-type-Prespectrum

point-Prespectrum : type-Prespectrum
point-Prespectrum = point-Pointed-Type pointed-type-Prespectrum

module _
{l : Level} (A : Prespectrum l) (n : ℕ)
where

pointed-type-Prespectrum A n →∗ Ω (pointed-type-Prespectrum A (succ-ℕ n))

type-Prespectrum A n → type-Ω (pointed-type-Prespectrum A (succ-ℕ n))

refl-Ω (pointed-type-Prespectrum A (succ-ℕ n))


### The structure maps of a prespectrum

module _
{l : Level} (A : Prespectrum l) (n : ℕ)
where

pointed-structure-map-Prespectrum :
suspension-Pointed-Type (pointed-type-Prespectrum A n) →∗
pointed-type-Prespectrum A (succ-ℕ n)
pointed-structure-map-Prespectrum =
( pointed-type-Prespectrum A n)
( pointed-type-Prespectrum A (succ-ℕ n))

structure-map-Prespectrum :
suspension (type-Prespectrum A n) → type-Prespectrum A (succ-ℕ n)
structure-map-Prespectrum = map-pointed-map pointed-structure-map-Prespectrum

preserves-point-structure-map-Prespectrum :
structure-map-Prespectrum north-suspension ＝ point-Prespectrum A (succ-ℕ n)
preserves-point-structure-map-Prespectrum =
preserves-point-pointed-map pointed-structure-map-Prespectrum


## References

[May99]
J. P. May. A Concise Course in Algebraic Topology. University of Chicago Press, 09 1999. ISBN 978-0-226-51183-2. URL: https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf.