# Maps of prespectra

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-12.

{-# OPTIONS --guardedness #-}

module synthetic-homotopy-theory.maps-of-prespectra where

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

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.homotopies
open import foundation.universe-levels

open import structured-types.commuting-squares-of-pointed-maps
open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import structured-types.whiskering-pointed-homotopies-composition
open import structured-types.wild-category-of-pointed-types

open import synthetic-homotopy-theory.functoriality-loop-spaces
open import synthetic-homotopy-theory.prespectra


## Idea

A map of prespectra f : A → B is a sequence of pointed maps

  fₙ : Aₙ →∗ Bₙ


such that the squares

        fₙ
Aₙ --------> Bₙ
|            |
|            |
|            |
∨            ∨
ΩAₙ₊₁ -----> ΩBₙ₊₁
Ωfₙ₊₁


commute in the category of pointed types.

## Definitions

### Maps of prespectra

coherence-map-Prespectrum :
{l1 l2 : Level} (A : Prespectrum l1) (B : Prespectrum l2) →
( (n : ℕ) →
pointed-type-Prespectrum A n →∗ pointed-type-Prespectrum B n) →
UU (l1 ⊔ l2)
coherence-map-Prespectrum A B f =
(n : ℕ) →
coherence-square-pointed-maps
( f n)
( pointed-map-Ω (f (succ-ℕ n)))

map-Prespectrum :
{l1 l2 : Level} (A : Prespectrum l1) (B : Prespectrum l2) →
UU (l1 ⊔ l2)
map-Prespectrum A B =
Σ ( (n : ℕ) →
pointed-type-Prespectrum A n →∗ pointed-type-Prespectrum B n)
( λ f → coherence-map-Prespectrum A B f)


## Properties

### The identity map on a prespectrum

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

map-id-map-Prespectrum :
(n : ℕ) → pointed-type-Prespectrum A n →∗ pointed-type-Prespectrum A n
map-id-map-Prespectrum _ = id-pointed-map

coherence-id-map-id-map-Prespectrum :
coherence-map-Prespectrum A A map-id-map-Prespectrum
coherence-id-map-id-map-Prespectrum n =
pointed-homotopy-reasoning
( pointed-map-Ω id-pointed-map ∘∗
~∗ id-pointed-map ∘∗ pointed-adjoint-structure-map-Prespectrum A n
by
right-whisker-comp-pointed-htpy
( pointed-map-Ω id-pointed-map)
( id-pointed-map)
( preserves-id-pointed-map-Ω)
by
left-unit-law-id-pointed-map
~∗ pointed-adjoint-structure-map-Prespectrum A n ∘∗ id-pointed-map
by
inv-pointed-htpy
( right-unit-law-id-pointed-map