From 4fb98ae83fd9a3ef3d976f1d89d2a34dfce7adcd Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 01:18:31 +0200
Subject: [PATCH 01/17] infrastructure `prespectra`

---
 .../prespectra.lagda.md                       | 43 ++++++++++++++++++-
 1 file changed, 41 insertions(+), 2 deletions(-)

diff --git a/src/synthetic-homotopy-theory/prespectra.lagda.md b/src/synthetic-homotopy-theory/prespectra.lagda.md
index 6b8827e384..cc34adb452 100644
--- a/src/synthetic-homotopy-theory/prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/prespectra.lagda.md
@@ -10,6 +10,8 @@ module synthetic-homotopy-theory.prespectra where
 open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
 open import foundation.universe-levels
 
 open import structured-types.pointed-maps
@@ -22,8 +24,14 @@ open import synthetic-homotopy-theory.loop-spaces
 
 ## Idea
 
-A prespectrum is a sequence of pointed types `A n` equipped with pointed maps
-`ε : A n →∗ Ω (A (n+1))`.
+A **prespectrum** is a [sequence](foundation.sequences.md) of
+[pointed types](structured-types.pointed-types.md) `A n`
+[equipped](foundation.structure.md) with
+[pointed maps](structured-types.pointed-maps.md)
+
+```text
+  ε : Aₙ →∗ Ω Aₙ₊₁.
+```
 
 ## Definition
 
@@ -31,4 +39,35 @@ A prespectrum is a sequence of pointed types `A n` equipped with pointed maps
 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-structure-map-Prespectrum :
+    pointed-type-Prespectrum A n →∗ Ω (pointed-type-Prespectrum A (succ-ℕ n))
+  pointed-structure-map-Prespectrum = pr2 A n
+
+  structure-map-Prespectrum :
+    type-Prespectrum A n → type-Ω (pointed-type-Prespectrum A (succ-ℕ n))
+  structure-map-Prespectrum = map-pointed-map pointed-structure-map-Prespectrum
+
+  preserves-point-structure-map-Prespectrum :
+    structure-map-Prespectrum (point-Prespectrum A n) ＝
+    refl-Ω (pointed-type-Prespectrum A (succ-ℕ n))
+  preserves-point-structure-map-Prespectrum =
+    preserves-point-pointed-map pointed-structure-map-Prespectrum
 ```

From cd8a95ff1f54531bcd4699441e0f196777974ef4 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 01:19:18 +0200
Subject: [PATCH 02/17] a few formatting fixes suspensions

---
 .../dependent-cocones-under-spans.lagda.md    | 10 +--
 .../suspension-structures.lagda.md            | 21 +++---
 .../suspensions-of-types.lagda.md             | 67 ++++++++++---------
 ...erty-suspensions-of-pointed-types.lagda.md | 26 +++----
 4 files changed, 65 insertions(+), 59 deletions(-)

diff --git a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
index bdabbcd01f..d8631c6fb7 100644
--- a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
@@ -99,10 +99,12 @@ dependent-cocone-map :
   { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   ( f : S → A) (g : S → B) (c : cocone f g X) (P : X → UU l5) →
   ( (x : X) → P x) → dependent-cocone f g c P
-dependent-cocone-map f g c P h =
-  ( λ a → h (horizontal-map-cocone f g c a)) ,
-  ( λ b → h (vertical-map-cocone f g c b)) ,
-  ( λ s → apd h (coherence-square-cocone f g c s))
+pr1 (dependent-cocone-map f g c P h) a =
+  h (horizontal-map-cocone f g c a)
+pr1 (pr2 (dependent-cocone-map f g c P h)) b =
+  h (vertical-map-cocone f g c b)
+pr2 (pr2 (dependent-cocone-map f g c P h)) s =
+  apd h (coherence-square-cocone f g c s)
 ```
 
 ## Properties
diff --git a/src/synthetic-homotopy-theory/suspension-structures.lagda.md b/src/synthetic-homotopy-theory/suspension-structures.lagda.md
index 28e806f73d..97cb1286a1 100644
--- a/src/synthetic-homotopy-theory/suspension-structures.lagda.md
+++ b/src/synthetic-homotopy-theory/suspension-structures.lagda.md
@@ -109,12 +109,11 @@ module _
 cocone-suspension-structure :
   {l1 l2 : Level} (X : UU l1) (Y : UU l2) →
   suspension-structure X Y → suspension-cocone X Y
-cocone-suspension-structure X Y (pair N (pair S merid)) =
-  pair
-    ( const unit Y N)
-    ( pair
-      ( const unit Y S)
-      ( merid))
+pr1 (cocone-suspension-structure X Y (N , S , merid)) = point N
+pr1 (pr2 (cocone-suspension-structure X Y (N , S , merid))) = point S
+pr2 (pr2 (cocone-suspension-structure X Y (N , S , merid))) = merid
+
+
 
 equiv-suspension-structure-suspension-cocone :
   {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
@@ -221,7 +220,9 @@ module _
   where
 
   refl-htpy-suspension-structure : htpy-suspension-structure c c
-  refl-htpy-suspension-structure = refl , (refl , right-unit-htpy)
+  pr1 refl-htpy-suspension-structure = refl
+  pr1 (pr2 refl-htpy-suspension-structure) = refl
+  pr2 (pr2 refl-htpy-suspension-structure) = right-unit-htpy
 
   is-refl-refl-htpy-suspension-structure :
     refl-htpy-suspension-structure ＝ htpy-eq-suspension-structure refl
@@ -238,9 +239,9 @@ module _
       ( htpy-suspension-structure c c') →
       UU l) →
     ( P c refl-htpy-suspension-structure) →
-    ( ( c' : suspension-structure X Z)
-      ( H : htpy-suspension-structure c c') →
-      P c' H)
+    ( c' : suspension-structure X Z)
+    ( H : htpy-suspension-structure c c') →
+    P c' H
   ind-htpy-suspension-structure P =
     pr1
       ( is-identity-system-is-torsorial
diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index 1c37e70746..a3caa9f79f 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -26,6 +26,7 @@ open import foundation.universe-levels
 open import synthetic-homotopy-theory.dependent-cocones-under-spans
 open import synthetic-homotopy-theory.dependent-suspension-structures
 open import synthetic-homotopy-theory.dependent-universal-property-suspensions
+open import synthetic-homotopy-theory.cocones-under-spans
 open import synthetic-homotopy-theory.pushouts
 open import synthetic-homotopy-theory.suspension-structures
 open import synthetic-homotopy-theory.universal-property-pushouts
@@ -36,8 +37,9 @@ open import synthetic-homotopy-theory.universal-property-suspensions
 
 ## Idea
 
-The suspension of a type `X` is the
-[pushout](synthetic-homotopy-theory.pushouts.md) of the span
+The **suspension** of a type `X` is the
+[pushout](synthetic-homotopy-theory.pushouts.md) of the
+[span](foundation.spans.md)
 
 ```text
 unit <-- X --> unit
@@ -54,23 +56,23 @@ they star in the freudenthal suspension theorem and give us a definition of
 ```agda
 suspension :
   {l : Level} → UU l → UU l
-suspension X = pushout (const X unit star) (const X unit star)
+suspension X = pushout (terminal-map {A = X}) (terminal-map {A = X})
 
 north-suspension :
   {l : Level} {X : UU l} → suspension X
 north-suspension {X = X} =
-  inl-pushout (const X unit star) (const X unit star) star
+  inl-pushout terminal-map terminal-map star
 
 south-suspension :
   {l : Level} {X : UU l} → suspension X
 south-suspension {X = X} =
-  inr-pushout (const X unit star) (const X unit star) star
+  inr-pushout terminal-map terminal-map star
 
 meridian-suspension :
   {l : Level} {X : UU l} → X →
   Id (north-suspension {X = X}) (south-suspension {X = X})
 meridian-suspension {X = X} =
-  glue-pushout (const X unit star) (const X unit star)
+  glue-pushout terminal-map terminal-map
 
 suspension-structure-suspension :
   {l : Level} (X : UU l) → suspension-structure X (suspension X)
@@ -99,10 +101,11 @@ module _
       ( triangle-ev-suspension
         { X = X}
         { Y = suspension X}
-        ( suspension-structure-suspension X) Z)
+        ( suspension-structure-suspension X)
+        ( Z))
       ( is-equiv-map-equiv
         ( ( equiv-suspension-structure-suspension-cocone X Z) ∘e
-          ( equiv-up-pushout (const X unit star) (const X unit star) Z)))
+          ( equiv-up-pushout terminal-map terminal-map Z)))
 
   equiv-up-suspension :
     {l : Level} (Z : UU l) → (suspension X → Z) ≃ (suspension-structure X Z)
@@ -134,7 +137,7 @@ module _
     ( map-inv-up-suspension Z c north-suspension) ＝
     ( north-suspension-structure c)
   up-suspension-north-suspension Z c =
-    pr1 (htpy-eq-suspension-structure ((is-section-map-inv-up-suspension Z) c))
+    pr1 (htpy-eq-suspension-structure (is-section-map-inv-up-suspension Z c))
 
   up-suspension-south-suspension :
     {l : Level} (Z : UU l) (c : suspension-structure X Z) →
@@ -184,8 +187,8 @@ dependent-up-suspension l {X = X} B =
         ( suspension-structure-suspension X)
         ( B)) ∘
       ( dependent-cocone-map
-        ( const X unit star)
-        ( const X unit star)
+        ( terminal-map)
+        ( terminal-map)
         ( cocone-suspension-structure
           ( X)
           ( suspension X)
@@ -201,20 +204,20 @@ dependent-up-suspension l {X = X} B =
           ( suspension-structure-suspension X)
           ( B)))
       ( dependent-cocone-map
-        ( const X unit star)
-        ( const X unit star)
+        ( terminal-map)
+        ( terminal-map)
         ( cocone-suspension-structure X
           ( suspension X)
           ( suspension-structure-suspension X))
         ( B))
-      ( dependent-up-pushout (const X unit star) (const X unit star) B)
+      ( dependent-up-pushout terminal-map terminal-map B)
       ( is-equiv-map-equiv
         ( equiv-dependent-suspension-structure-suspension-cocone
           ( suspension-structure-suspension X)
           ( B))))
 
 equiv-dependent-up-suspension :
-    {l1 l2 : Level} {X : UU l1} (B : (suspension X) → UU l2) →
+    {l1 l2 : Level} {X : UU l1} (B : suspension X → UU l2) →
     ((x : suspension X) → B x) ≃
     ( dependent-suspension-structure B (suspension-structure-suspension X))
 pr1 (equiv-dependent-up-suspension {l2 = l2} {X = X} B) =
@@ -223,7 +226,7 @@ pr2 (equiv-dependent-up-suspension {l2 = l2} B) =
   dependent-up-suspension l2 B
 
 module _
-  {l1 l2 : Level} {X : UU l1} (B : (suspension X) → UU l2)
+  {l1 l2 : Level} {X : UU l1} (B : suspension X → UU l2)
   where
 
   map-inv-dependent-up-suspension :
@@ -248,8 +251,8 @@ module _
     (d : dependent-suspension-structure
       ( B)
       ( suspension-structure-suspension X)) →
-      ( map-inv-dependent-up-suspension d north-suspension) ＝
-      ( north-dependent-suspension-structure d)
+    ( map-inv-dependent-up-suspension d north-suspension) ＝
+    ( north-dependent-suspension-structure d)
   dependent-up-suspension-north-suspension d =
     north-htpy-dependent-suspension-structure
       ( B)
@@ -301,14 +304,14 @@ suspension
 ```agda
 module _
   {l1 l2 : Level} (X : UU l1) {Y : UU l2}
-  (f g : (suspension X) → Y)
+  (f g : suspension X → Y)
   where
 
   htpy-function-out-of-suspension : UU (l1 ⊔ l2)
   htpy-function-out-of-suspension =
-    Σ ( f (north-suspension) ＝ g (north-suspension))
+    Σ ( f north-suspension ＝ g north-suspension)
       ( λ p →
-        Σ ( f (south-suspension) ＝ g (south-suspension))
+        Σ ( f south-suspension ＝ g south-suspension)
           ( λ q →
             (x : X) →
             coherence-square-identifications
@@ -319,12 +322,12 @@ module _
 
   north-htpy-function-out-of-suspension :
     htpy-function-out-of-suspension →
-    f (north-suspension) ＝ g (north-suspension)
+    f north-suspension ＝ g north-suspension
   north-htpy-function-out-of-suspension = pr1
 
   south-htpy-function-out-of-suspension :
     htpy-function-out-of-suspension →
-    f (south-suspension) ＝ g (south-suspension)
+    f south-suspension ＝ g south-suspension
   south-htpy-function-out-of-suspension = pr1 ∘ pr2
 
   meridian-htpy-function-out-of-suspension :
@@ -377,9 +380,9 @@ module _
     map-equiv (equiv-htpy-function-out-of-suspension-htpy)
 
   htpy-htpy-function-out-of-suspension :
-      htpy-function-out-of-suspension → (f ~ g)
+    htpy-function-out-of-suspension → (f ~ g)
   htpy-htpy-function-out-of-suspension =
-      map-inv-equiv (equiv-htpy-function-out-of-suspension-htpy)
+    map-inv-equiv (equiv-htpy-function-out-of-suspension-htpy)
 
   equiv-htpy-htpy-function-out-of-suspension :
     htpy-function-out-of-suspension ≃ (f ~ g)
@@ -395,14 +398,14 @@ is-contr-suspension-is-contr :
 is-contr-suspension-is-contr {l} {X} is-contr-X =
   is-contr-is-equiv'
     ( unit)
-    ( pr1 (pr2 (cocone-pushout (const X unit star) (const X unit star))))
+    ( pr1 (pr2 (cocone-pushout terminal-map terminal-map)))
     ( is-equiv-universal-property-pushout
-      ( const X unit star)
-      ( const X unit star)
+      ( terminal-map)
+      ( terminal-map)
       ( cocone-pushout
-        ( const X unit star)
-        ( const X unit star))
-      ( is-equiv-is-contr (const X unit star) is-contr-X is-contr-unit)
-      ( up-pushout (const X unit star) (const X unit star)))
+        ( terminal-map)
+        ( terminal-map))
+      ( is-equiv-is-contr terminal-map is-contr-X is-contr-unit)
+      ( up-pushout terminal-map terminal-map))
     ( is-contr-unit)
 ```
diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md
index 38ab886c89..96a9963aaa 100644
--- a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md
+++ b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md
@@ -108,7 +108,7 @@ module _
   where
 
   map-equiv-susp-loop-adj :
-    ((suspension-Pointed-Type X) →∗ Y) → (X →∗ Ω Y)
+    (suspension-Pointed-Type X →∗ Y) → (X →∗ Ω Y)
   map-equiv-susp-loop-adj f∗ =
     ((pointed-map-Ω f∗) ∘∗ (pointed-map-unit-susp-loop-adj X))
 ```
@@ -121,7 +121,7 @@ module _
   where
 
   map-inv-equiv-susp-loop-adj :
-    (X →∗ Ω Y) → ((suspension-Pointed-Type X) →∗ Y)
+    (X →∗ Ω Y) → (suspension-Pointed-Type X →∗ Y)
   pr1 (map-inv-equiv-susp-loop-adj f∗) =
     map-inv-up-suspension
       ( type-Pointed-Type X)
@@ -135,9 +135,9 @@ module _
       ( type-Pointed-Type X)
       ( type-Pointed-Type Y)
       ( suspension-structure-map-into-Ω
-      ( type-Pointed-Type X)
-      ( Y)
-      ( map-pointed-map f∗))
+        ( type-Pointed-Type X)
+        ( Y)
+        ( map-pointed-map f∗))
 ```
 
 We now show these maps are inverses of each other.
@@ -171,19 +171,19 @@ module _
               Σ ( Id (point-Pointed-Type Y) (pr1 z))
                 ( λ x → pr2 z (point-Pointed-Type X) ＝ x))) ∘e
           ( ( inv-equiv
-            ( right-unit-law-Σ-is-contr
-              ( λ ( z : Σ ( type-Pointed-Type Y)
-                ( λ y1 →
-                  type-Pointed-Type X →
-                  point-Pointed-Type Y ＝ y1)) →
-                    ( is-contr-total-path
-                      ( (pr2 z) (point-Pointed-Type X)))))) ∘e
+              ( right-unit-law-Σ-is-contr
+                ( λ ( z : Σ ( type-Pointed-Type Y)
+                  ( λ y1 →
+                    type-Pointed-Type X →
+                    point-Pointed-Type Y ＝ y1)) →
+                      ( is-contr-total-path
+                        ( pr2 z (point-Pointed-Type X)))))) ∘e
             ( ( left-unit-law-Σ-is-contr
                 ( is-contr-total-path' (point-Pointed-Type Y))
                 ( (point-Pointed-Type Y) , refl)) ∘e
               ( ( equiv-right-swap-Σ) ∘e
                 ( equiv-Σ-equiv-base
-                  ( λ c → (pr1 c) ＝ (point-Pointed-Type Y))
+                  ( λ c → pr1 c ＝ point-Pointed-Type Y)
                   ( equiv-up-suspension
                     ( type-Pointed-Type X)
                     ( type-Pointed-Type Y)))))))))

From 38f23067369e5bfd8b57ec4650ae4f2c1b6e8d50 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 01:28:49 +0200
Subject: [PATCH 03/17] infrastructure `spectra`

---
 .../spectra.lagda.md                          | 42 ++++++++++++++++++-
 1 file changed, 40 insertions(+), 2 deletions(-)

diff --git a/src/synthetic-homotopy-theory/spectra.lagda.md b/src/synthetic-homotopy-theory/spectra.lagda.md
index b59eb28164..d53f211286 100644
--- a/src/synthetic-homotopy-theory/spectra.lagda.md
+++ b/src/synthetic-homotopy-theory/spectra.lagda.md
@@ -10,10 +10,13 @@ module synthetic-homotopy-theory.spectra where
 open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
+open import foundation.function-types
 open import foundation.universe-levels
 
 open import structured-types.pointed-equivalences
+open import structured-types.pointed-maps
 open import structured-types.pointed-types
+open import synthetic-homotopy-theory.prespectra
 
 open import synthetic-homotopy-theory.loop-spaces
 ```
@@ -22,8 +25,14 @@ open import synthetic-homotopy-theory.loop-spaces
 
 ## Idea
 
-A spectrum is an infinite sequence of pointed types `A` such that
-`A n ≃∗ Ω (A (n+1))` for each `n : ℕ`.
+A **spectrum** is a [sequence](foundation.sequences.md) of
+[pointed types](structured-types.pointed-types.md) `A` such that
+
+```text
+  Aₙ ≃∗ Ω Aₙ₊₁
+```
+
+for each `n : ℕ`.
 
 ## Definition
 
@@ -31,4 +40,33 @@ A spectrum is an infinite sequence of pointed types `A` such that
 Spectrum : (l : Level) → UU (lsuc l)
 Spectrum l =
   Σ (ℕ → Pointed-Type l) (λ A → (n : ℕ) → A n ≃∗ Ω (A (succ-ℕ n)))
+
+module _
+  {l : Level} (A : Spectrum l)
+  where
+
+  pointed-type-Spectrum : ℕ → Pointed-Type l
+  pointed-type-Spectrum = pr1 A
+
+  type-Spectrum : ℕ → UU l
+  type-Spectrum = type-Pointed-Type ∘ pointed-type-Spectrum
+
+  point-Spectrum : (n : ℕ) → type-Spectrum n
+  point-Spectrum = point-Pointed-Type ∘ pointed-type-Spectrum
+
+  pointed-equiv-Spectrum :
+    (n : ℕ) → pointed-type-Spectrum n ≃∗ Ω (pointed-type-Spectrum (succ-ℕ n))
+  pointed-equiv-Spectrum = pr2 A
+
+  pointed-map-Spectrum :
+    (n : ℕ) → pointed-type-Spectrum n →∗ Ω (pointed-type-Spectrum (succ-ℕ n))
+  pointed-map-Spectrum = pointed-map-pointed-equiv ∘ pointed-equiv-Spectrum
+
+  map-Spectrum :
+    (n : ℕ) → type-Spectrum n → type-Ω (pointed-type-Spectrum (succ-ℕ n))
+  map-Spectrum = map-pointed-map ∘ pointed-map-Spectrum
+
+  prespectrum-Spectrum : Prespectrum l
+  pr1 prespectrum-Spectrum = pointed-type-Spectrum
+  pr2 prespectrum-Spectrum = pointed-map-Spectrum
 ```

From b30a78245dd8838a3a9afbb272ef3a7aa06aaf32 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 02:00:25 +0200
Subject: [PATCH 04/17] =?UTF-8?q?The=20functorial=20action=20of=20`=CE=A9`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../loop-spaces.lagda.md                      | 35 +++++++++++++++++--
 1 file changed, 32 insertions(+), 3 deletions(-)

diff --git a/src/synthetic-homotopy-theory/loop-spaces.lagda.md b/src/synthetic-homotopy-theory/loop-spaces.lagda.md
index b61195a3b2..ecd1e66c32 100644
--- a/src/synthetic-homotopy-theory/loop-spaces.lagda.md
+++ b/src/synthetic-homotopy-theory/loop-spaces.lagda.md
@@ -7,6 +7,7 @@ module synthetic-homotopy-theory.loop-spaces where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
@@ -15,6 +16,8 @@ open import foundation.universe-levels
 open import structured-types.h-spaces
 open import structured-types.magmas
 open import structured-types.pointed-equivalences
+open import structured-types.pointed-families-of-types
+open import structured-types.pointed-maps
 open import structured-types.pointed-types
 open import structured-types.wild-quasigroups
 ```
@@ -23,9 +26,11 @@ open import structured-types.wild-quasigroups
 
 ## Idea
 
-The loop space of a pointed type `A` is the pointed type of self-identifications
-of the base point of `A`. The loop space comes equipped with a group structure
-induced by the groupoidal structure on identifications.
+The **loop space** of a [pointed type](structured-types.pointed-types.md) `A` is
+the pointed type of self-[identifications](foundation-core.identity-types.md) of
+the base point of `A`. The loop space comes equipped with a
+[group](group-theory.groups.md) structure induced by the
+[groupoidal](category-theory.groupoids.md) structure on identifications.
 
 ## Table of files directly related to loop spaces
 
@@ -167,6 +172,30 @@ module _
   eq-tr-type-Ω refl q = inv right-unit
 ```
 
+### The functorial action of `Ω`
+
+```agda
+module _
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
+  where
+
+  map-pointed-map-Ω : (A →∗ B) → type-Ω A → type-Ω B
+  map-pointed-map-Ω f p =
+    ( inv (preserves-point-pointed-map f)) ∙
+    ( ( ap (map-pointed-map f) p) ∙
+      ( preserves-point-pointed-map f))
+
+  pointed-map-Ω : (A →∗ B) → Ω A →∗ Ω B
+  pr1 (pointed-map-Ω f) = map-pointed-map-Ω f
+  pr2 (pointed-map-Ω f) =
+      ( ap
+        ( λ p →
+          ( inv (preserves-point-pointed-map f)) ∙
+          ( p ∙ (preserves-point-pointed-map f)))
+        ( ap-refl (map-pointed-map f) (point-Pointed-Type A))) ∙
+      ( left-inv (preserves-point-pointed-map f))
+```
+
 ## Properties
 
 ### Every pointed identity type is equivalent to a loop space

From 7c91d1db21b64e111b48fe313e7ef08994d3581a Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 02:19:06 +0200
Subject: [PATCH 05/17] suspension prespectra

---
 src/synthetic-homotopy-theory.lagda.md        |  2 +
 ...ated-suspensions-of-pointed-types.lagda.md | 69 +++++++++++++++++++
 .../spectra.lagda.md                          | 11 +--
 .../suspension-prespectra.lagda.md            | 47 +++++++++++++
 .../suspension-structures.lagda.md            |  2 -
 .../suspensions-of-types.lagda.md             |  2 +-
 6 files changed, 125 insertions(+), 8 deletions(-)
 create mode 100644 src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md
 create mode 100644 src/synthetic-homotopy-theory/suspension-prespectra.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index bfae224a76..d46e157e80 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -48,6 +48,7 @@ open import synthetic-homotopy-theory.infinite-complex-projective-space public
 open import synthetic-homotopy-theory.infinite-cyclic-types public
 open import synthetic-homotopy-theory.interval-type public
 open import synthetic-homotopy-theory.iterated-loop-spaces public
+open import synthetic-homotopy-theory.iterated-suspensions-of-pointed-types public
 open import synthetic-homotopy-theory.join-powers-of-types public
 open import synthetic-homotopy-theory.joins-of-types public
 open import synthetic-homotopy-theory.loop-spaces public
@@ -63,6 +64,7 @@ open import synthetic-homotopy-theory.sections-descent-circle public
 open import synthetic-homotopy-theory.smash-products-of-pointed-types public
 open import synthetic-homotopy-theory.spectra public
 open import synthetic-homotopy-theory.spheres public
+open import synthetic-homotopy-theory.suspension-prespectra public
 open import synthetic-homotopy-theory.suspension-structures public
 open import synthetic-homotopy-theory.suspensions-of-pointed-types public
 open import synthetic-homotopy-theory.suspensions-of-types public
diff --git a/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md
new file mode 100644
index 0000000000..eba651d64c
--- /dev/null
+++ b/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md
@@ -0,0 +1,69 @@
+# Iterated suspensions of pointed types
+
+```agda
+module synthetic-homotopy-theory.iterated-suspensions-of-pointed-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.constant-maps
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import structured-types.pointed-types
+
+open import synthetic-homotopy-theory.loop-spaces
+open import synthetic-homotopy-theory.suspension-structures
+open import synthetic-homotopy-theory.suspensions-of-pointed-types
+open import synthetic-homotopy-theory.suspensions-of-types
+```
+
+</details>
+
+## Idea
+
+Given a [pointed type](structured-types.pointed-types.md) `X`
+
+### The iterated suspension of a pointed type
+
+```agda
+iterated-suspension-Pointed-Type :
+  {l : Level} (n : ℕ) → Pointed-Type l → Pointed-Type l
+iterated-suspension-Pointed-Type 0 X = X
+iterated-suspension-Pointed-Type (succ-ℕ n) X =
+  suspension-Pointed-Type (iterated-suspension-Pointed-Type n X)
+```
+
+#### Suspension structure induced by a pointed type
+
+```agda
+-- constant-suspension-structure-Pointed-Type :
+--   {l1 l2 : Level} (X : UU l1) (Y : Pointed-Type l2) →
+--   suspension-structure X (type-Pointed-Type Y)
+-- pr1 (constant-suspension-structure-Pointed-Type X Y) =
+--   point-Pointed-Type Y
+-- pr1 (pr2 (constant-suspension-structure-Pointed-Type X Y)) =
+--   point-Pointed-Type Y
+-- pr2 (pr2 (constant-suspension-structure-Pointed-Type X Y)) =
+--   const X (point-Pointed-Type Y ＝ point-Pointed-Type Y) refl
+```
+
+#### Suspension structure induced by a map into a loop space
+
+The following function takes a map `X → Ω Y` and returns a suspension structure
+on `Y`.
+
+```agda
+-- module _
+--   {l1 l2 : Level} (X : UU l1) (Y : Pointed-Type l2)
+--   where
+--   suspension-structure-map-into-Ω :
+--     (X → type-Ω Y) → suspension-structure X (type-Pointed-Type Y)
+--   pr1 (suspension-structure-map-into-Ω f) = point-Pointed-Type Y
+--   pr1 (pr2 (suspension-structure-map-into-Ω f)) = point-Pointed-Type Y
+--   pr2 (pr2 (suspension-structure-map-into-Ω f)) = f
+```
diff --git a/src/synthetic-homotopy-theory/spectra.lagda.md b/src/synthetic-homotopy-theory/spectra.lagda.md
index d53f211286..bfdeebae73 100644
--- a/src/synthetic-homotopy-theory/spectra.lagda.md
+++ b/src/synthetic-homotopy-theory/spectra.lagda.md
@@ -16,9 +16,9 @@ open import foundation.universe-levels
 open import structured-types.pointed-equivalences
 open import structured-types.pointed-maps
 open import structured-types.pointed-types
-open import synthetic-homotopy-theory.prespectra
 
 open import synthetic-homotopy-theory.loop-spaces
+open import synthetic-homotopy-theory.prespectra
 ```
 
 </details>
@@ -58,15 +58,16 @@ module _
     (n : ℕ) → pointed-type-Spectrum n ≃∗ Ω (pointed-type-Spectrum (succ-ℕ n))
   pointed-equiv-Spectrum = pr2 A
 
-  pointed-map-Spectrum :
+  pointed-structure-map-Spectrum :
     (n : ℕ) → pointed-type-Spectrum n →∗ Ω (pointed-type-Spectrum (succ-ℕ n))
-  pointed-map-Spectrum = pointed-map-pointed-equiv ∘ pointed-equiv-Spectrum
+  pointed-structure-map-Spectrum =
+    pointed-map-pointed-equiv ∘ pointed-equiv-Spectrum
 
   map-Spectrum :
     (n : ℕ) → type-Spectrum n → type-Ω (pointed-type-Spectrum (succ-ℕ n))
-  map-Spectrum = map-pointed-map ∘ pointed-map-Spectrum
+  map-Spectrum = map-pointed-map ∘ pointed-structure-map-Spectrum
 
   prespectrum-Spectrum : Prespectrum l
   pr1 prespectrum-Spectrum = pointed-type-Spectrum
-  pr2 prespectrum-Spectrum = pointed-map-Spectrum
+  pr2 prespectrum-Spectrum = pointed-structure-map-Spectrum
 ```
diff --git a/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md b/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
new file mode 100644
index 0000000000..60a99071c9
--- /dev/null
+++ b/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
@@ -0,0 +1,47 @@
+# Suspension prespectra
+
+```agda
+module synthetic-homotopy-theory.suspension-prespectra where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import structured-types.pointed-maps
+open import structured-types.pointed-types
+
+open import synthetic-homotopy-theory.iterated-suspensions-of-pointed-types
+open import synthetic-homotopy-theory.loop-spaces
+open import synthetic-homotopy-theory.prespectra
+open import synthetic-homotopy-theory.spectra
+open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types
+```
+
+</details>
+
+## Idea
+
+Given a [pointed type](structured-types.pointed-types.md) `A`, the
+[sequence](foundation.sequences.md) of iterated
+[suspensions](synthetic-homotopy-theory.suspensions-of-pointed-types.md) of `A`
+
+```text
+  A   Σ¹A   Σ² A   Σ³ A   ...
+```
+
+defines a [prespectrum](synthetic-homotopy-theory.prespectra.md) that we call
+the **suspension spectrum** of `A`.
+
+## Definition
+
+```agda
+suspension-Prespectrum : {l : Level} → Pointed-Type l → Prespectrum l
+pr1 (suspension-Prespectrum A) n = iterated-suspension-Pointed-Type n A
+pr2 (suspension-Prespectrum A) n =
+  pointed-map-unit-susp-loop-adj (iterated-suspension-Pointed-Type n A)
+```
diff --git a/src/synthetic-homotopy-theory/suspension-structures.lagda.md b/src/synthetic-homotopy-theory/suspension-structures.lagda.md
index 97cb1286a1..68e5ca611b 100644
--- a/src/synthetic-homotopy-theory/suspension-structures.lagda.md
+++ b/src/synthetic-homotopy-theory/suspension-structures.lagda.md
@@ -113,8 +113,6 @@ pr1 (cocone-suspension-structure X Y (N , S , merid)) = point N
 pr1 (pr2 (cocone-suspension-structure X Y (N , S , merid))) = point S
 pr2 (pr2 (cocone-suspension-structure X Y (N , S , merid))) = merid
 
-
-
 equiv-suspension-structure-suspension-cocone :
   {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
   suspension-cocone X Z ≃ suspension-structure X Z
diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index a3caa9f79f..b69dfaa20f 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -23,10 +23,10 @@ open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels
 
+open import synthetic-homotopy-theory.cocones-under-spans
 open import synthetic-homotopy-theory.dependent-cocones-under-spans
 open import synthetic-homotopy-theory.dependent-suspension-structures
 open import synthetic-homotopy-theory.dependent-universal-property-suspensions
-open import synthetic-homotopy-theory.cocones-under-spans
 open import synthetic-homotopy-theory.pushouts
 open import synthetic-homotopy-theory.suspension-structures
 open import synthetic-homotopy-theory.universal-property-pushouts

From 14f7a3ead9168862ed192d2df4c392a576dce783 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 02:20:02 +0200
Subject: [PATCH 06/17] strict maps of prespectra

---
 src/foundation/sequences.lagda.md             |  2 +-
 src/synthetic-homotopy-theory.lagda.md        |  1 +
 .../strict-maps-of-prespectra.lagda.md        | 82 +++++++++++++++++++
 3 files changed, 84 insertions(+), 1 deletion(-)
 create mode 100644 src/synthetic-homotopy-theory/strict-maps-of-prespectra.lagda.md

diff --git a/src/foundation/sequences.lagda.md b/src/foundation/sequences.lagda.md
index e2fa18053f..636fff2f05 100644
--- a/src/foundation/sequences.lagda.md
+++ b/src/foundation/sequences.lagda.md
@@ -18,7 +18,7 @@ open import foundation-core.function-types
 
 ## Idea
 
-A sequence of elements in a type `A` is a map `ℕ → A`.
+A **sequence** of elements in a type `A` is a map `ℕ → A`.
 
 ## Definition
 
diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index d46e157e80..e87e4889bd 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -64,6 +64,7 @@ open import synthetic-homotopy-theory.sections-descent-circle public
 open import synthetic-homotopy-theory.smash-products-of-pointed-types public
 open import synthetic-homotopy-theory.spectra public
 open import synthetic-homotopy-theory.spheres public
+open import synthetic-homotopy-theory.strict-maps-of-prespectra public
 open import synthetic-homotopy-theory.suspension-prespectra public
 open import synthetic-homotopy-theory.suspension-structures public
 open import synthetic-homotopy-theory.suspensions-of-pointed-types public
diff --git a/src/synthetic-homotopy-theory/strict-maps-of-prespectra.lagda.md b/src/synthetic-homotopy-theory/strict-maps-of-prespectra.lagda.md
new file mode 100644
index 0000000000..17269c8c0f
--- /dev/null
+++ b/src/synthetic-homotopy-theory/strict-maps-of-prespectra.lagda.md
@@ -0,0 +1,82 @@
+# Strict maps of prespectra
+
+```agda
+module synthetic-homotopy-theory.strict-maps-of-prespectra where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import structured-types.commuting-squares-of-pointed-maps
+open import structured-types.pointed-maps
+open import structured-types.pointed-types
+
+open import synthetic-homotopy-theory.loop-spaces
+open import synthetic-homotopy-theory.prespectra
+```
+
+</details>
+
+## Idea
+
+A **strict-map of presectra** `f : A → B` of degree `r` is a
+[sequence](foundation.sequences.md) of maps
+
+```text
+  fₙ : Eₙ₊ᵣ → Fₙ
+```
+
+such that
+
+```text
+        fₙ
+  Aₙ₊ᵣ ------> Bₙ
+  |            |
+  |            |
+  |            |
+  v            v
+  ΩAₙ₊ᵣ₊₁ ---> ΩBₙ₊₁
+          Ωfₙ₊₁
+```
+
+commute.
+
+## Definition
+
+```agda
+coherence-strict-map-Prespectrum :
+  {l1 l2 : Level} (n : ℕ) (r : ℕ) (A : Prespectrum l1) (B : Prespectrum l2) →
+  ( (n : ℕ) →
+    pointed-type-Prespectrum A (n +ℕ r) →∗ pointed-type-Prespectrum B n) →
+  UU (l1 ⊔ l2)
+coherence-strict-map-Prespectrum n r A B f =
+  coherence-square-pointed-maps
+    ( f n)
+    ( pointed-structure-map-Prespectrum A (n +ℕ r))
+    ( pointed-structure-map-Prespectrum B n)
+    ( pointed-map-Ω
+      ( tr
+        ( λ m →
+          pointed-map
+            ( pointed-type-Prespectrum A m)
+            ( pointed-type-Prespectrum B (succ-ℕ n)))
+        ( left-successor-law-add-ℕ n r)
+        ( f (succ-ℕ n))))
+
+strict-map-Prespectrum :
+  {l1 l2 : Level} (r : ℕ) (A : Prespectrum l1) (B : Prespectrum l2) →
+  UU (l1 ⊔ l2)
+strict-map-Prespectrum r A B =
+  Σ ( (n : ℕ) →
+      pointed-type-Prespectrum A (n +ℕ r) →∗ pointed-type-Prespectrum B n)
+    ( λ f → (n : ℕ) → coherence-strict-map-Prespectrum n r A B f)
+```

From be9a77c77ba50a2eeebbe205439c94fc9bc8e904 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 13:00:45 +0200
Subject: [PATCH 07/17] infrastructure `spectra`

---
 .../pointed-equivalences.lagda.md             | 13 +++-
 .../spectra.lagda.md                          | 66 ++++++++++++++-----
 2 files changed, 61 insertions(+), 18 deletions(-)

diff --git a/src/structured-types/pointed-equivalences.lagda.md b/src/structured-types/pointed-equivalences.lagda.md
index d0ae361439..d4d90f9605 100644
--- a/src/structured-types/pointed-equivalences.lagda.md
+++ b/src/structured-types/pointed-equivalences.lagda.md
@@ -34,9 +34,10 @@ open import structured-types.pointed-types
 
 ## Idea
 
-A pointed equivalence is an equivalence in the category of pointed spaces.
-Equivalently, a pointed equivalence is a pointed map of which the underlying
-function is an equivalence.
+A **pointed equivalence** is an equivalence in the category of pointed spaces.
+Equivalently, a pointed equivalence is a
+[pointed map](structured-types.pointed-maps.md) of which the underlying function
+is an [equivalence](foundation-core.equivalences.md).
 
 ## Definitions
 
@@ -50,6 +51,12 @@ module _
   is-equiv-pointed-map : (A →∗ B) → UU (l1 ⊔ l2)
   is-equiv-pointed-map f = is-equiv (map-pointed-map f)
 
+  is-prop-is-equiv-pointed-map : (f : A →∗ B) → is-prop (is-equiv-pointed-map f)
+  is-prop-is-equiv-pointed-map = is-property-is-equiv ∘ map-pointed-map
+
+  is-equiv-pointed-map-Prop : (A →∗ B) → Prop (l1 ⊔ l2)
+  is-equiv-pointed-map-Prop = is-equiv-Prop ∘ map-pointed-map
+
 pointed-equiv :
   {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) → UU (l1 ⊔ l2)
 pointed-equiv A B =
diff --git a/src/synthetic-homotopy-theory/spectra.lagda.md b/src/synthetic-homotopy-theory/spectra.lagda.md
index bfdeebae73..42ae7fb376 100644
--- a/src/synthetic-homotopy-theory/spectra.lagda.md
+++ b/src/synthetic-homotopy-theory/spectra.lagda.md
@@ -10,7 +10,10 @@ module synthetic-homotopy-theory.spectra where
 open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
+open import foundation.equivalences
 open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
 open import foundation.universe-levels
 
 open import structured-types.pointed-equivalences
@@ -36,38 +39,71 @@ for each `n : ℕ`.
 
 ## Definition
 
+### The predicate on prespectra of being a spectrum
+
+```agda
+is-spectrum-Prop : {l : Level} → Prespectrum l → Prop l
+is-spectrum-Prop A =
+  Π-Prop ℕ
+    ( λ n → is-equiv-pointed-map-Prop (pointed-structure-map-Prespectrum A n))
+
+is-spectrum : {l : Level} → Prespectrum l → UU l
+is-spectrum = type-Prop ∘ is-spectrum-Prop
+
+is-prop-is-spectrum : {l : Level} (A : Prespectrum l) → is-prop (is-spectrum A)
+is-prop-is-spectrum = is-prop-type-Prop ∘ is-spectrum-Prop
+```
+
+### The type of spectra
+
 ```agda
 Spectrum : (l : Level) → UU (lsuc l)
-Spectrum l =
-  Σ (ℕ → Pointed-Type l) (λ A → (n : ℕ) → A n ≃∗ Ω (A (succ-ℕ n)))
+Spectrum l = Σ (Prespectrum l) (is-spectrum)
 
 module _
   {l : Level} (A : Spectrum l)
   where
 
+  prespectrum-Spectrum : Prespectrum l
+  prespectrum-Spectrum = pr1 A
+
   pointed-type-Spectrum : ℕ → Pointed-Type l
-  pointed-type-Spectrum = pr1 A
+  pointed-type-Spectrum = pointed-type-Prespectrum prespectrum-Spectrum
 
   type-Spectrum : ℕ → UU l
-  type-Spectrum = type-Pointed-Type ∘ pointed-type-Spectrum
+  type-Spectrum = type-Prespectrum prespectrum-Spectrum
 
   point-Spectrum : (n : ℕ) → type-Spectrum n
-  point-Spectrum = point-Pointed-Type ∘ pointed-type-Spectrum
-
-  pointed-equiv-Spectrum :
-    (n : ℕ) → pointed-type-Spectrum n ≃∗ Ω (pointed-type-Spectrum (succ-ℕ n))
-  pointed-equiv-Spectrum = pr2 A
+  point-Spectrum = point-Prespectrum prespectrum-Spectrum
 
   pointed-structure-map-Spectrum :
     (n : ℕ) → pointed-type-Spectrum n →∗ Ω (pointed-type-Spectrum (succ-ℕ n))
   pointed-structure-map-Spectrum =
-    pointed-map-pointed-equiv ∘ pointed-equiv-Spectrum
+    pointed-structure-map-Prespectrum prespectrum-Spectrum
 
-  map-Spectrum :
+  structure-map-Spectrum :
     (n : ℕ) → type-Spectrum n → type-Ω (pointed-type-Spectrum (succ-ℕ n))
-  map-Spectrum = map-pointed-map ∘ pointed-structure-map-Spectrum
+  structure-map-Spectrum = structure-map-Prespectrum prespectrum-Spectrum
 
-  prespectrum-Spectrum : Prespectrum l
-  pr1 prespectrum-Spectrum = pointed-type-Spectrum
-  pr2 prespectrum-Spectrum = pointed-structure-map-Spectrum
+  preserves-point-structure-map-Spectrum :
+    (n : ℕ) →
+    structure-map-Prespectrum (pr1 A) n (point-Prespectrum (pr1 A) n) ＝
+    refl-Ω (pointed-type-Prespectrum (pr1 A) (succ-ℕ n))
+  preserves-point-structure-map-Spectrum =
+    preserves-point-structure-map-Prespectrum prespectrum-Spectrum
+
+  is-equiv-pointed-structure-map-Spectrum :
+    (n : ℕ) → is-equiv-pointed-map (pointed-structure-map-Spectrum n)
+  is-equiv-pointed-structure-map-Spectrum = pr2 A
+
+  structure-equiv-Spectrum :
+    (n : ℕ) → type-Spectrum n ≃ type-Ω (pointed-type-Spectrum (succ-ℕ n))
+  pr1 (structure-equiv-Spectrum n) = structure-map-Spectrum n
+  pr2 (structure-equiv-Spectrum n) = is-equiv-pointed-structure-map-Spectrum n
+
+  pointed-structure-equiv-Spectrum :
+    (n : ℕ) → pointed-type-Spectrum n ≃∗ Ω (pointed-type-Spectrum (succ-ℕ n))
+  pr1 (pointed-structure-equiv-Spectrum n) = structure-equiv-Spectrum n
+  pr2 (pointed-structure-equiv-Spectrum n) =
+    preserves-point-structure-map-Spectrum n
 ```

From 74287dc6356398bc5d58a1d75827647bd9a4f9de Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 17:45:24 +0200
Subject: [PATCH 08/17] the sphere prespectrum

---
 src/foundation-core/subtypes.lagda.md         |   2 +-
 ...ithmetic-dependent-function-types.lagda.md |  11 +-
 .../pointed-equivalences.lagda.md             |  53 ++++----
 src/synthetic-homotopy-theory.lagda.md        |   1 +
 .../dependent-suspension-structures.lagda.md  |   6 +-
 .../functoriality-loop-spaces.lagda.md        |  43 ++++---
 ...ated-suspensions-of-pointed-types.lagda.md |  40 +-----
 .../loop-spaces.lagda.md                      |  27 ----
 .../sphere-spectrum.lagda.md                  |  45 +++++++
 .../spheres.lagda.md                          |  19 ++-
 .../suspension-prespectra.lagda.md            |  15 ++-
 ...erty-suspensions-of-pointed-types.lagda.md | 116 ++++++++----------
 12 files changed, 177 insertions(+), 201 deletions(-)
 create mode 100644 src/synthetic-homotopy-theory/sphere-spectrum.lagda.md

diff --git a/src/foundation-core/subtypes.lagda.md b/src/foundation-core/subtypes.lagda.md
index 5d93921187..c58a2a3d8f 100644
--- a/src/foundation-core/subtypes.lagda.md
+++ b/src/foundation-core/subtypes.lagda.md
@@ -274,7 +274,7 @@ equiv-subtype-equiv :
   ((x : A) → type-Prop (C x) ↔ type-Prop (D (map-equiv e x))) →
   type-subtype C ≃ type-subtype D
 equiv-subtype-equiv e C D H =
-  equiv-Σ (type-Prop ∘ D) (e) (λ x → equiv-iff' (C x) (D (map-equiv e x)) (H x))
+  equiv-Σ (type-Prop ∘ D) e (λ x → equiv-iff' (C x) (D (map-equiv e x)) (H x))
 ```
 
 ```agda
diff --git a/src/foundation/type-arithmetic-dependent-function-types.lagda.md b/src/foundation/type-arithmetic-dependent-function-types.lagda.md
index 8ea2ca0e6e..1ac7670980 100644
--- a/src/foundation/type-arithmetic-dependent-function-types.lagda.md
+++ b/src/foundation/type-arithmetic-dependent-function-types.lagda.md
@@ -33,12 +33,11 @@ module _
 
   left-unit-law-Π-is-contr : ((a : A) → (B a)) ≃ B a
   left-unit-law-Π-is-contr =
-    ( ( left-unit-law-Π ( λ _ → B a)) ∘e
-      ( equiv-Π
-        ( λ _ → B a)
-        ( terminal-map , is-equiv-terminal-map-is-contr C)
-        ( λ a →
-          equiv-eq (ap B ( eq-is-contr C)))))
+    ( left-unit-law-Π ( λ _ → B a)) ∘e
+    ( equiv-Π
+      ( λ _ → B a)
+      ( terminal-map , is-equiv-terminal-map-is-contr C)
+      ( λ a → equiv-eq (ap B ( eq-is-contr C))))
 ```
 
 ### The swap function `((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)` is an equivalence
diff --git a/src/structured-types/pointed-equivalences.lagda.md b/src/structured-types/pointed-equivalences.lagda.md
index d4d90f9605..a32857b0e5 100644
--- a/src/structured-types/pointed-equivalences.lagda.md
+++ b/src/structured-types/pointed-equivalences.lagda.md
@@ -71,6 +71,11 @@ compute-pointed-equiv :
   (A ≃∗ B) ≃ Σ (A →∗ B) (is-equiv-pointed-map {A = A} {B})
 compute-pointed-equiv A B = equiv-right-swap-Σ
 
+inv-compute-pointed-equiv :
+  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) →
+  Σ (A →∗ B) (is-equiv-pointed-map {A = A} {B}) ≃ (A ≃∗ B)
+inv-compute-pointed-equiv A B = equiv-right-swap-Σ
+
 module _
   {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (e : A ≃∗ B)
   where
@@ -206,14 +211,14 @@ module _
             ( inv (preserves-point-pointed-map f))))
         ( equiv-tot
           ( λ p →
-            ( ( equiv-right-transpose-eq-concat
-                ( ap (map-pointed-map f) p)
-                ( preserves-point-pointed-map f)
-                ( is-section-map-inv-is-equiv H (point-Pointed-Type B))) ∘e
-              ( equiv-inv
-                ( is-section-map-inv-is-equiv H (point-Pointed-Type B))
-                ( ( ap (map-pointed-map f) p) ∙
-                  ( preserves-point-pointed-map f)))) ∘e
+            ( equiv-right-transpose-eq-concat
+              ( ap (map-pointed-map f) p)
+              ( preserves-point-pointed-map f)
+              ( is-section-map-inv-is-equiv H (point-Pointed-Type B))) ∘e
+            ( equiv-inv
+              ( is-section-map-inv-is-equiv H (point-Pointed-Type B))
+              ( ( ap (map-pointed-map f) p) ∙
+                ( preserves-point-pointed-map f))) ∘e
             ( equiv-concat'
               ( is-section-map-inv-is-equiv H (point-Pointed-Type B))
               ( right-unit))))
@@ -228,37 +233,22 @@ module _
     is-equiv-pointed-map f → is-contr (retraction-pointed-map f)
   is-contr-retraction-is-equiv-pointed-map H =
     is-contr-total-Eq-structure
-      ( λ g p (G : (g ∘ map-pointed-map f) ~ id) →
+      ( λ g p (G : g ∘ map-pointed-map f ~ id) →
         Id
-          { A =
-            Id
-              { A = type-Pointed-Type A}
-              ( g (map-pointed-map f (point-Pointed-Type A)))
-              ( point-Pointed-Type A)}
           ( G (point-Pointed-Type A))
-          ( ( ( ap g (preserves-point-pointed-map f)) ∙
-              ( p)) ∙
-            ( refl)))
+          ( ( ap g (preserves-point-pointed-map f) ∙ p) ∙ refl))
       ( is-contr-retraction-is-equiv H)
       ( pair (map-inv-is-equiv H) (is-retraction-map-inv-is-equiv H))
       ( is-contr-equiv
         ( fiber
           ( λ p →
-            ( ( ap
-                ( map-inv-is-equiv H)
-                ( preserves-point-pointed-map f)) ∙
-              ( p)) ∙
-            ( refl))
+            ap (map-inv-is-equiv H) (preserves-point-pointed-map f) ∙ p ∙ refl)
           ( is-retraction-map-inv-is-equiv H (point-Pointed-Type A)))
         ( equiv-tot (λ p → equiv-inv _ _))
         ( is-contr-map-is-equiv
           ( is-equiv-comp
-            ( λ q → q ∙ refl)
-            ( λ p →
-              ( ap
-                ( map-inv-is-equiv H)
-                ( preserves-point-pointed-map f)) ∙
-              ( p))
+            ( _∙ refl)
+            ( ap (map-inv-is-equiv H) (preserves-point-pointed-map f) ∙_)
             ( is-equiv-concat
               ( ap
                 ( map-inv-is-equiv H)
@@ -314,8 +304,7 @@ module _
   where
 
   is-equiv-is-equiv-precomp-pointed-map :
-    ( {l : Level} (C : Pointed-Type l) →
-      is-equiv (precomp-pointed-map C f)) →
+    ( {l : Level} (C : Pointed-Type l) → is-equiv (precomp-pointed-map C f)) →
     is-equiv-pointed-map f
   is-equiv-is-equiv-precomp-pointed-map H =
     is-equiv-is-invertible
@@ -438,8 +427,8 @@ module _
   where
 
   is-equiv-is-equiv-comp-pointed-map :
-    ({l : Level} (X : Pointed-Type l) →
-    is-equiv (comp-pointed-map {A = X} f)) → is-equiv-pointed-map f
+    ({l : Level} (X : Pointed-Type l) → is-equiv (comp-pointed-map {A = X} f)) →
+    is-equiv-pointed-map f
   is-equiv-is-equiv-comp-pointed-map H =
     is-equiv-is-invertible
       ( map-pointed-map g)
diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index e87e4889bd..7095fc2aab 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -63,6 +63,7 @@ open import synthetic-homotopy-theory.pushouts-of-pointed-types public
 open import synthetic-homotopy-theory.sections-descent-circle public
 open import synthetic-homotopy-theory.smash-products-of-pointed-types public
 open import synthetic-homotopy-theory.spectra public
+open import synthetic-homotopy-theory.sphere-spectrum public
 open import synthetic-homotopy-theory.spheres public
 open import synthetic-homotopy-theory.strict-maps-of-prespectra public
 open import synthetic-homotopy-theory.suspension-prespectra public
diff --git a/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md b/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md
index e113b5a80e..16f582a0c6 100644
--- a/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md
@@ -179,7 +179,7 @@ module _
               ( s))))
       ( equiv-dependent-universal-property-unit
         ( λ x → B (north-suspension-structure c)))
-      ( λ N-susp-c →
+      ( λ north-suspension-c →
         ( equiv-Σ
           ( λ s →
             (x : X) →
@@ -189,11 +189,11 @@ module _
               ( map-equiv
                 ( equiv-dependent-universal-property-unit
                   ( λ _ → B (north-suspension-structure c)))
-                ( N-susp-c))
+                ( north-suspension-c))
               ( s)))
           ( equiv-dependent-universal-property-unit
             ( const unit (UU l3) (B (south-suspension-structure c))))
-          ( λ S-susp-c → id-equiv))))
+          ( λ south-suspension-c → id-equiv))))
 
   htpy-map-inv-equiv-dependent-suspension-structure-suspension-cocone-cocone-dependent-cocone-dependent-suspension-structure :
     map-inv-equiv equiv-dependent-suspension-structure-suspension-cocone ~
diff --git a/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md
index ad4aeac593..0207535d46 100644
--- a/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md
+++ b/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md
@@ -27,8 +27,10 @@ open import synthetic-homotopy-theory.loop-spaces
 
 ## Idea
 
-Any pointed map `f : A →∗ B` induces a map `map-Ω f : Ω A →∗ Ω B`. Furthermore,
-this operation respects the groupoidal operations on loop spaces.
+Any [pointed map](structured-types.pointed-maps.md) `f : A →∗ B` induces a
+pointed map `pointed-map-Ω f : Ω A →∗ Ω B`. Furthermore, this operation respects
+the groupoidal operations on
+[loop spaces](sytnhetic-homotopy-theory.loop-spaces.md).
 
 ## Definition
 
@@ -43,14 +45,15 @@ module _
       ( preserves-point-pointed-map f)
       ( ap (map-pointed-map f) p)
 
-  preserves-refl-map-Ω : Id (map-Ω refl) refl
+  preserves-refl-map-Ω : map-Ω refl ＝ refl
   preserves-refl-map-Ω = preserves-refl-tr-Ω (pr2 f)
 
   pointed-map-Ω : Ω A →∗ Ω B
-  pointed-map-Ω = pair map-Ω preserves-refl-map-Ω
+  pr1 pointed-map-Ω = map-Ω
+  pr2 pointed-map-Ω = preserves-refl-map-Ω
 
   preserves-mul-map-Ω :
-    (x y : type-Ω A) → Id (map-Ω (mul-Ω A x y)) (mul-Ω B (map-Ω x) (map-Ω y))
+    (x y : type-Ω A) → map-Ω (mul-Ω A x y) ＝ mul-Ω B (map-Ω x) (map-Ω y)
   preserves-mul-map-Ω x y =
     ( ap
       ( tr-type-Ω (preserves-point-pointed-map f))
@@ -61,7 +64,7 @@ module _
       ( ap (map-pointed-map f) y))
 
   preserves-inv-map-Ω :
-    (x : type-Ω A) → Id (map-Ω (inv-Ω A x)) (inv-Ω B (map-Ω x))
+    (x : type-Ω A) → map-Ω (inv-Ω A x) ＝ inv-Ω B (map-Ω x)
   preserves-inv-map-Ω x =
     ( ap
       ( tr-type-Ω (preserves-point-pointed-map f))
@@ -84,8 +87,7 @@ module _
     is-emb-comp
       ( tr-type-Ω (preserves-point-pointed-map f))
       ( ap (map-pointed-map f))
-      ( is-emb-is-equiv
-        ( is-equiv-tr-type-Ω (preserves-point-pointed-map f)))
+      ( is-emb-is-equiv (is-equiv-tr-type-Ω (preserves-point-pointed-map f)))
       ( H (point-Pointed-Type A) (point-Pointed-Type A))
 
   emb-Ω :
@@ -102,27 +104,24 @@ module _
 ```agda
 module _
   {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
-  (f : A →∗ B) (t : is-emb (map-pointed-map f))
+  (f : A →∗ B) (is-emb-f : is-emb (map-pointed-map f))
   where
 
-  is-equiv-map-Ω-emb :
-    is-equiv (map-Ω f)
-  is-equiv-map-Ω-emb =
+  is-equiv-map-Ω-is-emb : is-equiv (map-Ω f)
+  is-equiv-map-Ω-is-emb =
     is-equiv-comp
       ( tr-type-Ω (preserves-point-pointed-map f))
       ( ap (map-pointed-map f))
-      ( t (point-Pointed-Type A) (point-Pointed-Type A))
+      ( is-emb-f (point-Pointed-Type A) (point-Pointed-Type A))
       ( is-equiv-tr-type-Ω (preserves-point-pointed-map f))
 
-  equiv-map-Ω-emb :
-    type-Ω A ≃ type-Ω B
-  pr1 equiv-map-Ω-emb = map-Ω f
-  pr2 equiv-map-Ω-emb = is-equiv-map-Ω-emb
+  equiv-map-Ω-is-emb : type-Ω A ≃ type-Ω B
+  pr1 equiv-map-Ω-is-emb = map-Ω f
+  pr2 equiv-map-Ω-is-emb = is-equiv-map-Ω-is-emb
 
-  pointed-equiv-pointed-map-Ω-emb :
-    Ω A ≃∗ Ω B
-  pr1 pointed-equiv-pointed-map-Ω-emb = equiv-map-Ω-emb
-  pr2 pointed-equiv-pointed-map-Ω-emb = preserves-refl-map-Ω f
+  pointed-equiv-pointed-map-Ω-is-emb : Ω A ≃∗ Ω B
+  pr1 pointed-equiv-pointed-map-Ω-is-emb = equiv-map-Ω-is-emb
+  pr2 pointed-equiv-pointed-map-Ω-is-emb = preserves-refl-map-Ω f
 ```
 
 ### The operator `pointed-map-Ω` preserves equivalences
@@ -136,7 +135,7 @@ module _
   equiv-map-Ω-pointed-equiv :
     type-Ω A ≃ type-Ω B
   equiv-map-Ω-pointed-equiv =
-    equiv-map-Ω-emb
+    equiv-map-Ω-is-emb
       ( pointed-map-pointed-equiv e)
       ( is-emb-is-equiv (is-equiv-map-equiv-pointed-equiv e))
 ```
diff --git a/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md
index eba651d64c..a385455cd2 100644
--- a/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md
+++ b/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md
@@ -9,24 +9,20 @@ module synthetic-homotopy-theory.iterated-suspensions-of-pointed-types where
 ```agda
 open import elementary-number-theory.natural-numbers
 
-open import foundation.constant-maps
-open import foundation.dependent-pair-types
-open import foundation.identity-types
 open import foundation.universe-levels
 
 open import structured-types.pointed-types
 
-open import synthetic-homotopy-theory.loop-spaces
-open import synthetic-homotopy-theory.suspension-structures
 open import synthetic-homotopy-theory.suspensions-of-pointed-types
-open import synthetic-homotopy-theory.suspensions-of-types
 ```
 
 </details>
 
 ## Idea
 
-Given a [pointed type](structured-types.pointed-types.md) `X`
+Given a [pointed type](structured-types.pointed-types.md) `X` and a
+[natural number](elementary-number-theory.natural-numbers.md), we can form the
+`n`-**iterated suspension** of `X`.
 
 ### The iterated suspension of a pointed type
 
@@ -37,33 +33,3 @@ iterated-suspension-Pointed-Type 0 X = X
 iterated-suspension-Pointed-Type (succ-ℕ n) X =
   suspension-Pointed-Type (iterated-suspension-Pointed-Type n X)
 ```
-
-#### Suspension structure induced by a pointed type
-
-```agda
--- constant-suspension-structure-Pointed-Type :
---   {l1 l2 : Level} (X : UU l1) (Y : Pointed-Type l2) →
---   suspension-structure X (type-Pointed-Type Y)
--- pr1 (constant-suspension-structure-Pointed-Type X Y) =
---   point-Pointed-Type Y
--- pr1 (pr2 (constant-suspension-structure-Pointed-Type X Y)) =
---   point-Pointed-Type Y
--- pr2 (pr2 (constant-suspension-structure-Pointed-Type X Y)) =
---   const X (point-Pointed-Type Y ＝ point-Pointed-Type Y) refl
-```
-
-#### Suspension structure induced by a map into a loop space
-
-The following function takes a map `X → Ω Y` and returns a suspension structure
-on `Y`.
-
-```agda
--- module _
---   {l1 l2 : Level} (X : UU l1) (Y : Pointed-Type l2)
---   where
---   suspension-structure-map-into-Ω :
---     (X → type-Ω Y) → suspension-structure X (type-Pointed-Type Y)
---   pr1 (suspension-structure-map-into-Ω f) = point-Pointed-Type Y
---   pr1 (pr2 (suspension-structure-map-into-Ω f)) = point-Pointed-Type Y
---   pr2 (pr2 (suspension-structure-map-into-Ω f)) = f
-```
diff --git a/src/synthetic-homotopy-theory/loop-spaces.lagda.md b/src/synthetic-homotopy-theory/loop-spaces.lagda.md
index ecd1e66c32..2800b53e61 100644
--- a/src/synthetic-homotopy-theory/loop-spaces.lagda.md
+++ b/src/synthetic-homotopy-theory/loop-spaces.lagda.md
@@ -7,7 +7,6 @@ module synthetic-homotopy-theory.loop-spaces where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
@@ -16,8 +15,6 @@ open import foundation.universe-levels
 open import structured-types.h-spaces
 open import structured-types.magmas
 open import structured-types.pointed-equivalences
-open import structured-types.pointed-families-of-types
-open import structured-types.pointed-maps
 open import structured-types.pointed-types
 open import structured-types.wild-quasigroups
 ```
@@ -172,30 +169,6 @@ module _
   eq-tr-type-Ω refl q = inv right-unit
 ```
 
-### The functorial action of `Ω`
-
-```agda
-module _
-  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
-  where
-
-  map-pointed-map-Ω : (A →∗ B) → type-Ω A → type-Ω B
-  map-pointed-map-Ω f p =
-    ( inv (preserves-point-pointed-map f)) ∙
-    ( ( ap (map-pointed-map f) p) ∙
-      ( preserves-point-pointed-map f))
-
-  pointed-map-Ω : (A →∗ B) → Ω A →∗ Ω B
-  pr1 (pointed-map-Ω f) = map-pointed-map-Ω f
-  pr2 (pointed-map-Ω f) =
-      ( ap
-        ( λ p →
-          ( inv (preserves-point-pointed-map f)) ∙
-          ( p ∙ (preserves-point-pointed-map f)))
-        ( ap-refl (map-pointed-map f) (point-Pointed-Type A))) ∙
-      ( left-inv (preserves-point-pointed-map f))
-```
-
 ## Properties
 
 ### Every pointed identity type is equivalent to a loop space
diff --git a/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md b/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
new file mode 100644
index 0000000000..8d22ec868e
--- /dev/null
+++ b/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
@@ -0,0 +1,45 @@
+# The sphere spectrum
+
+```agda
+module synthetic-homotopy-theory.sphere-spectrum where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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
+```
+
+</details>
+
+## Idea
+
+The [spheres](synthetic-homotopy-theory.spheres.md) `Sⁿ` define a
+[spectrum](synthetic-homotopy-theory.spectra.md)
+
+```text
+  Sⁿ ≃∗ ΩSⁿ⁺¹.
+```
+
+We call this spectrum the the **sphere spectrum**.
+
+## Definition
+
+### The sphere presecptrum
+
+```agda
+sphere-Prespectrum : Prespectrum lzero
+sphere-Prespectrum = suspension-Prespectrum (Fin 2 , zero-Fin 1)
+```
+
+### The sphere spectrum
+
+This remains to be defined. To define this, it would be practical to first have
+the lemma that the transposing map of the loop-suspension adjunction preserves
+and reflects equivalences.
diff --git a/src/synthetic-homotopy-theory/spheres.lagda.md b/src/synthetic-homotopy-theory/spheres.lagda.md
index ff3be84437..f307865988 100644
--- a/src/synthetic-homotopy-theory/spheres.lagda.md
+++ b/src/synthetic-homotopy-theory/spheres.lagda.md
@@ -9,9 +9,14 @@ module synthetic-homotopy-theory.spheres where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.dependent-pair-types
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.universe-levels
 
+open import structured-types.pointed-types
+
+open import synthetic-homotopy-theory.iterated-suspensions-of-pointed-types
 open import synthetic-homotopy-theory.suspensions-of-types
 
 open import univalent-combinatorics.standard-finite-types
@@ -21,14 +26,19 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-The spheres are defined as iterated suspensions of `Fin 2`.
+The **spheres** are defined as
+[iterated suspensions](synthetic-homotopy-theory.iterated-suspensions-pointed-types.md)
+of the
+[standard two-element type `Fin 2`](univalent-combinatorics.standard-finite-types.md).
 
 ## Definition
 
 ```agda
+sphere-Pointed-Type : ℕ → Pointed-Type lzero
+sphere-Pointed-Type n = iterated-suspension-Pointed-Type n (Fin 2 , zero-Fin 1)
+
 sphere : ℕ → UU lzero
-sphere zero-ℕ = Fin 2
-sphere (succ-ℕ n) = suspension (sphere n)
+sphere = type-Pointed-Type ∘ sphere-Pointed-Type
 
 north-sphere : (n : ℕ) → sphere n
 north-sphere zero-ℕ = zero-Fin 1
@@ -39,7 +49,6 @@ south-sphere zero-ℕ = one-Fin 1
 south-sphere (succ-ℕ n) = south-suspension
 
 meridian-sphere :
-  (n : ℕ) → sphere n →
-  north-sphere (succ-ℕ n) ＝ south-sphere (succ-ℕ n)
+  (n : ℕ) → sphere n → north-sphere (succ-ℕ n) ＝ south-sphere (succ-ℕ n)
 meridian-sphere n = meridian-suspension
 ```
diff --git a/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md b/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
index 60a99071c9..7aa6b83358 100644
--- a/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
@@ -18,7 +18,6 @@ open import structured-types.pointed-types
 open import synthetic-homotopy-theory.iterated-suspensions-of-pointed-types
 open import synthetic-homotopy-theory.loop-spaces
 open import synthetic-homotopy-theory.prespectra
-open import synthetic-homotopy-theory.spectra
 open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types
 ```
 
@@ -34,14 +33,20 @@ Given a [pointed type](structured-types.pointed-types.md) `A`, the
   A   Σ¹A   Σ² A   Σ³ A   ...
 ```
 
-defines a [prespectrum](synthetic-homotopy-theory.prespectra.md) that we call
-the **suspension spectrum** of `A`.
+defines a [prespectrum](synthetic-homotopy-theory.prespectra.md) `Σ^∞A` that we
+call the **suspension spectrum** of `A`.
 
 ## Definition
 
 ```agda
+structure-map-suspension-Prespectrum :
+  {l : Level} (A : Pointed-Type l) (n : ℕ) →
+  iterated-suspension-Pointed-Type n A →∗
+  Ω (iterated-suspension-Pointed-Type (succ-ℕ n) A)
+structure-map-suspension-Prespectrum A n =
+  pointed-map-unit-suspension-loop-adjunction (iterated-suspension-Pointed-Type n A)
+
 suspension-Prespectrum : {l : Level} → Pointed-Type l → Prespectrum l
 pr1 (suspension-Prespectrum A) n = iterated-suspension-Pointed-Type n A
-pr2 (suspension-Prespectrum A) n =
-  pointed-map-unit-susp-loop-adj (iterated-suspension-Pointed-Type n A)
+pr2 (suspension-Prespectrum A) = structure-map-suspension-Prespectrum A
 ```
diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md
index 96a9963aaa..fee3903f99 100644
--- a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md
+++ b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md
@@ -71,58 +71,58 @@ module _
   pr1 pointed-map-concat-meridian-suspension = meridian-suspension
   pr2 pointed-map-concat-meridian-suspension = refl
 
-  pointed-map-unit-susp-loop-adj : X →∗ Ω (suspension-Pointed-Type X)
-  pointed-map-unit-susp-loop-adj =
+  pointed-map-unit-suspension-loop-adjunction :
+    X →∗ Ω (suspension-Pointed-Type X)
+  pointed-map-unit-suspension-loop-adjunction =
     pointed-map-loop-pointed-identity-suspension ∘∗
     pointed-map-concat-meridian-suspension
 
-  map-unit-susp-loop-adj : type-Pointed-Type X →
-    type-Ω (suspension-Pointed-Type X)
-  map-unit-susp-loop-adj = map-pointed-map pointed-map-unit-susp-loop-adj
+  map-unit-suspension-loop-adjunction :
+    type-Pointed-Type X → type-Ω (suspension-Pointed-Type X)
+  map-unit-suspension-loop-adjunction =
+    map-pointed-map pointed-map-unit-suspension-loop-adjunction
 
-  map-counit-susp-loop-adj : (suspension (type-Ω X)) → type-Pointed-Type X
-  map-counit-susp-loop-adj =
+  map-counit-suspension-loop-adjunction :
+    suspension (type-Ω X) → type-Pointed-Type X
+  map-counit-suspension-loop-adjunction =
     map-inv-is-equiv
       ( up-suspension (type-Ω X) (type-Pointed-Type X))
-      ( ( point-Pointed-Type X) ,
-        ( point-Pointed-Type X) ,
-        ( id))
-
-  pointed-map-counit-susp-loop-adj :
-    ( pair (suspension (type-Ω X)) north-suspension) →∗ X
-  pr1 pointed-map-counit-susp-loop-adj = map-counit-susp-loop-adj
-  pr2 pointed-map-counit-susp-loop-adj =
+      ( point-Pointed-Type X , point-Pointed-Type X , id)
+
+  pointed-map-counit-suspension-loop-adjunction :
+    pair (suspension (type-Ω X)) (north-suspension) →∗ X
+  pr1 pointed-map-counit-suspension-loop-adjunction =
+    map-counit-suspension-loop-adjunction
+  pr2 pointed-map-counit-suspension-loop-adjunction =
     up-suspension-north-suspension
       ( type-Ω X)
       ( type-Pointed-Type X)
-      ( ( point-Pointed-Type X) ,
-        ( point-Pointed-Type X) ,
-        ( id))
+      ( point-Pointed-Type X , point-Pointed-Type X , id)
 ```
 
-#### The underlying map of the equivalence
+#### The transposing map of the adjunction
 
 ```agda
 module _
   {l1 l2 : Level} (X : Pointed-Type l1) (Y : Pointed-Type l2)
   where
 
-  map-equiv-susp-loop-adj :
+  transpose-suspension-loop-adjunction :
     (suspension-Pointed-Type X →∗ Y) → (X →∗ Ω Y)
-  map-equiv-susp-loop-adj f∗ =
-    ((pointed-map-Ω f∗) ∘∗ (pointed-map-unit-susp-loop-adj X))
+  transpose-suspension-loop-adjunction f∗ =
+    pointed-map-Ω f∗ ∘∗ pointed-map-unit-suspension-loop-adjunction X
 ```
 
-#### The underlying map of the inverse equivalence
+#### The inverse transposing map of the adjunction
 
 ```agda
 module _
   {l1 l2 : Level} (X : Pointed-Type l1) (Y : Pointed-Type l2)
   where
 
-  map-inv-equiv-susp-loop-adj :
+  inv-transpose-suspension-loop-adjunction :
     (X →∗ Ω Y) → (suspension-Pointed-Type X →∗ Y)
-  pr1 (map-inv-equiv-susp-loop-adj f∗) =
+  pr1 (inv-transpose-suspension-loop-adjunction f∗) =
     map-inv-up-suspension
       ( type-Pointed-Type X)
       ( type-Pointed-Type Y)
@@ -130,7 +130,7 @@ module _
         ( type-Pointed-Type X)
         ( Y)
         ( map-pointed-map f∗))
-  pr2 (map-inv-equiv-susp-loop-adj f∗) =
+  pr2 (inv-transpose-suspension-loop-adjunction f∗) =
     up-suspension-north-suspension
       ( type-Pointed-Type X)
       ( type-Pointed-Type Y)
@@ -142,51 +142,41 @@ module _
 
 We now show these maps are inverses of each other.
 
-#### The equivalence between pointed maps out of the suspension of X and pointed maps into the loop space of Y
+#### The transposing equivalence between pointed maps out of the suspension of `X` and pointed maps into the loop space of `Y`
 
 ```agda
 module _
   {l1 l2 : Level} (X : Pointed-Type l1) (Y : Pointed-Type l2)
   where
 
-  equiv-susp-loop-adj : (suspension-Pointed-Type X →∗ Y) ≃ (X →∗ Ω Y)
-  equiv-susp-loop-adj =
+  equiv-transpose-suspension-loop-adjunction :
+    (suspension-Pointed-Type X →∗ Y) ≃ (X →∗ Ω Y)
+  equiv-transpose-suspension-loop-adjunction =
     ( left-unit-law-Σ-is-contr
       ( is-contr-total-path (point-Pointed-Type Y))
-      ( (point-Pointed-Type Y) , refl)) ∘e
-    ( ( inv-equiv
-        ( associative-Σ
-          ( type-Pointed-Type Y)
-          ( λ z → (point-Pointed-Type Y) ＝ z)
-          ( λ t →
-            Σ ( type-Pointed-Type X →
-                ( point-Pointed-Type Y) ＝ (pr1 t))
-              ( λ f → f (point-Pointed-Type X) ＝ (pr2 t))))) ∘e
-      ( ( equiv-tot (λ y1 → equiv-left-swap-Σ)) ∘e
-        ( ( associative-Σ
-            ( type-Pointed-Type Y)
-            ( λ y1 →
-              type-Pointed-Type X → point-Pointed-Type Y ＝ y1)
-            ( λ z →
-              Σ ( Id (point-Pointed-Type Y) (pr1 z))
-                ( λ x → pr2 z (point-Pointed-Type X) ＝ x))) ∘e
-          ( ( inv-equiv
-              ( right-unit-law-Σ-is-contr
-                ( λ ( z : Σ ( type-Pointed-Type Y)
-                  ( λ y1 →
-                    type-Pointed-Type X →
-                    point-Pointed-Type Y ＝ y1)) →
-                      ( is-contr-total-path
-                        ( pr2 z (point-Pointed-Type X)))))) ∘e
-            ( ( left-unit-law-Σ-is-contr
-                ( is-contr-total-path' (point-Pointed-Type Y))
-                ( (point-Pointed-Type Y) , refl)) ∘e
-              ( ( equiv-right-swap-Σ) ∘e
-                ( equiv-Σ-equiv-base
-                  ( λ c → pr1 c ＝ point-Pointed-Type Y)
-                  ( equiv-up-suspension
-                    ( type-Pointed-Type X)
-                    ( type-Pointed-Type Y)))))))))
+      ( point-Pointed-Type Y , refl)) ∘e
+    ( inv-associative-Σ
+      ( type-Pointed-Type Y)
+      ( λ z → point-Pointed-Type Y ＝ z)
+      ( λ t →
+        Σ ( type-Pointed-Type X → point-Pointed-Type Y ＝ pr1 t)
+          ( λ f → f (point-Pointed-Type X) ＝ pr2 t))) ∘e
+    ( equiv-tot (λ y1 → equiv-left-swap-Σ)) ∘e
+    ( associative-Σ
+      ( type-Pointed-Type Y)
+      ( λ y1 → type-Pointed-Type X → point-Pointed-Type Y ＝ y1)
+      ( λ z →
+        Σ ( point-Pointed-Type Y ＝ pr1 z)
+          ( λ x → pr2 z (point-Pointed-Type X) ＝ x))) ∘e
+    ( inv-right-unit-law-Σ-is-contr
+      ( λ z → is-contr-total-path (pr2 z (point-Pointed-Type X)))) ∘e
+    ( left-unit-law-Σ-is-contr
+      ( is-contr-total-path' (point-Pointed-Type Y))
+      ( point-Pointed-Type Y , refl)) ∘e
+    ( equiv-right-swap-Σ) ∘e
+    ( equiv-Σ-equiv-base
+      ( λ c → pr1 c ＝ point-Pointed-Type Y)
+      ( equiv-up-suspension (type-Pointed-Type X) (type-Pointed-Type Y)))
 ```
 
 #### The equivalence in the suspension-loop space adjunction is pointed

From 5951e6a0d2aa6b98864348fbe26424f649174d4b Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 18:24:13 +0200
Subject: [PATCH 09/17] remove shift in `maps-of-prespectra`

---
 src/synthetic-homotopy-theory.lagda.md        |  2 +-
 .../maps-of-prespectra.lagda.md               | 81 ++++++++++++++++++
 .../prespectra.lagda.md                       | 18 +++-
 .../spectra.lagda.md                          |  5 ++
 .../sphere-spectrum.lagda.md                  |  6 +-
 .../strict-maps-of-prespectra.lagda.md        | 82 -------------------
 .../suspension-prespectra.lagda.md            |  3 +-
 7 files changed, 109 insertions(+), 88 deletions(-)
 create mode 100644 src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
 delete mode 100644 src/synthetic-homotopy-theory/strict-maps-of-prespectra.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 7095fc2aab..7c7b8f00ec 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -52,6 +52,7 @@ open import synthetic-homotopy-theory.iterated-suspensions-of-pointed-types publ
 open import synthetic-homotopy-theory.join-powers-of-types public
 open import synthetic-homotopy-theory.joins-of-types public
 open import synthetic-homotopy-theory.loop-spaces public
+open import synthetic-homotopy-theory.maps-of-prespectra public
 open import synthetic-homotopy-theory.morphisms-descent-data-circle public
 open import synthetic-homotopy-theory.multiplication-circle public
 open import synthetic-homotopy-theory.plus-principle public
@@ -65,7 +66,6 @@ open import synthetic-homotopy-theory.smash-products-of-pointed-types public
 open import synthetic-homotopy-theory.spectra public
 open import synthetic-homotopy-theory.sphere-spectrum public
 open import synthetic-homotopy-theory.spheres public
-open import synthetic-homotopy-theory.strict-maps-of-prespectra public
 open import synthetic-homotopy-theory.suspension-prespectra public
 open import synthetic-homotopy-theory.suspension-structures public
 open import synthetic-homotopy-theory.suspensions-of-pointed-types public
diff --git a/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
new file mode 100644
index 0000000000..244961cc46
--- /dev/null
+++ b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
@@ -0,0 +1,81 @@
+# Maps of prespectra
+
+```agda
+module synthetic-homotopy-theory.maps-of-prespectra where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import structured-types.commuting-squares-of-pointed-maps
+open import structured-types.pointed-maps
+open import structured-types.pointed-types
+
+open import synthetic-homotopy-theory.functoriality-loop-spaces
+open import synthetic-homotopy-theory.loop-spaces
+open import synthetic-homotopy-theory.prespectra
+```
+
+</details>
+
+## Idea
+
+A **map of presectra** `f : A → B` is a [sequence](foundation.sequences.md) of
+[pointed maps](structured-types.pointed-maps.md)
+
+```text
+  fₙ : Aₙ →∗ Bₙ
+```
+
+such that the squares
+
+```text
+        fₙ
+  Aₙ --------> Bₙ
+  |            |
+  |            |
+  |            |
+  v            v
+  ΩAₙ₊₁ -----> ΩBₙ₊₁
+        Ωfₙ₊₁
+```
+
+commute in the category of [pointed types](structured-types.pointed-types.md).
+
+## Definition
+
+```agda
+coherence-map-Prespectrum :
+  {l1 l2 : Level} (n : ℕ) (A : Prespectrum l1) (B : Prespectrum l2) →
+  ( (n : ℕ) →
+    pointed-type-Prespectrum A n →∗ pointed-type-Prespectrum B n) →
+  UU (l1 ⊔ l2)
+coherence-map-Prespectrum n A B f =
+  coherence-square-pointed-maps
+    ( f n)
+    ( pointed-structure-map-Prespectrum A n)
+    ( pointed-structure-map-Prespectrum B 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 → (n : ℕ) → coherence-map-Prespectrum n A B f)
+```
+
+## References
+
+- J. P. May, _A Concise Course in Algebraic Topology_, 1999
+  ([pdf](https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf))
diff --git a/src/synthetic-homotopy-theory/prespectra.lagda.md b/src/synthetic-homotopy-theory/prespectra.lagda.md
index cc34adb452..44e0575834 100644
--- a/src/synthetic-homotopy-theory/prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/prespectra.lagda.md
@@ -30,7 +30,18 @@ A **prespectrum** is a [sequence](foundation.sequences.md) of
 [pointed maps](structured-types.pointed-maps.md)
 
 ```text
-  ε : Aₙ →∗ Ω Aₙ₊₁.
+  ε : Aₙ →∗ ΩAₙ₊₁
+```
+
+called the **structure maps** of the prespectrum.
+
+By the
+[loop-suspension adjunction](synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types.md),
+specifying structure maps `Aₙ →∗ Ω Aₙ₊₁` is
+[equivalent](foundation-core.equivalences.md) to specifying their adjoint maps
+
+```text
+  ΣAₙ → Aₙ₊₁.
 ```
 
 ## Definition
@@ -71,3 +82,8 @@ module _
   preserves-point-structure-map-Prespectrum =
     preserves-point-pointed-map pointed-structure-map-Prespectrum
 ```
+
+## References
+
+- J. P. May, _A Concise Course in Algebraic Topology_, 1999
+  ([pdf](https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf))
diff --git a/src/synthetic-homotopy-theory/spectra.lagda.md b/src/synthetic-homotopy-theory/spectra.lagda.md
index 42ae7fb376..6687a1283b 100644
--- a/src/synthetic-homotopy-theory/spectra.lagda.md
+++ b/src/synthetic-homotopy-theory/spectra.lagda.md
@@ -107,3 +107,8 @@ module _
   pr2 (pointed-structure-equiv-Spectrum n) =
     preserves-point-structure-map-Spectrum n
 ```
+
+## References
+
+- J. P. May, _A Concise Course in Algebraic Topology_, 1999
+  ([pdf](https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf))
diff --git a/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md b/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
index 8d22ec868e..fd391cd86f 100644
--- a/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
+++ b/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
@@ -24,14 +24,14 @@ The [spheres](synthetic-homotopy-theory.spheres.md) `Sⁿ` define a
 [spectrum](synthetic-homotopy-theory.spectra.md)
 
 ```text
-  Sⁿ ≃∗ ΩSⁿ⁺¹.
+  Sⁿ ≃∗ ΩSⁿ⁺¹
 ```
 
-We call this spectrum the the **sphere spectrum**.
+which we call the **sphere spectrum**.
 
 ## Definition
 
-### The sphere presecptrum
+### The sphere prespectrum
 
 ```agda
 sphere-Prespectrum : Prespectrum lzero
diff --git a/src/synthetic-homotopy-theory/strict-maps-of-prespectra.lagda.md b/src/synthetic-homotopy-theory/strict-maps-of-prespectra.lagda.md
deleted file mode 100644
index 17269c8c0f..0000000000
--- a/src/synthetic-homotopy-theory/strict-maps-of-prespectra.lagda.md
+++ /dev/null
@@ -1,82 +0,0 @@
-# Strict maps of prespectra
-
-```agda
-module synthetic-homotopy-theory.strict-maps-of-prespectra where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import elementary-number-theory.addition-natural-numbers
-open import elementary-number-theory.natural-numbers
-
-open import foundation.commuting-squares-of-maps
-open import foundation.dependent-pair-types
-open import foundation.identity-types
-open import foundation.transport-along-identifications
-open import foundation.universe-levels
-
-open import structured-types.commuting-squares-of-pointed-maps
-open import structured-types.pointed-maps
-open import structured-types.pointed-types
-
-open import synthetic-homotopy-theory.loop-spaces
-open import synthetic-homotopy-theory.prespectra
-```
-
-</details>
-
-## Idea
-
-A **strict-map of presectra** `f : A → B` of degree `r` is a
-[sequence](foundation.sequences.md) of maps
-
-```text
-  fₙ : Eₙ₊ᵣ → Fₙ
-```
-
-such that
-
-```text
-        fₙ
-  Aₙ₊ᵣ ------> Bₙ
-  |            |
-  |            |
-  |            |
-  v            v
-  ΩAₙ₊ᵣ₊₁ ---> ΩBₙ₊₁
-          Ωfₙ₊₁
-```
-
-commute.
-
-## Definition
-
-```agda
-coherence-strict-map-Prespectrum :
-  {l1 l2 : Level} (n : ℕ) (r : ℕ) (A : Prespectrum l1) (B : Prespectrum l2) →
-  ( (n : ℕ) →
-    pointed-type-Prespectrum A (n +ℕ r) →∗ pointed-type-Prespectrum B n) →
-  UU (l1 ⊔ l2)
-coherence-strict-map-Prespectrum n r A B f =
-  coherence-square-pointed-maps
-    ( f n)
-    ( pointed-structure-map-Prespectrum A (n +ℕ r))
-    ( pointed-structure-map-Prespectrum B n)
-    ( pointed-map-Ω
-      ( tr
-        ( λ m →
-          pointed-map
-            ( pointed-type-Prespectrum A m)
-            ( pointed-type-Prespectrum B (succ-ℕ n)))
-        ( left-successor-law-add-ℕ n r)
-        ( f (succ-ℕ n))))
-
-strict-map-Prespectrum :
-  {l1 l2 : Level} (r : ℕ) (A : Prespectrum l1) (B : Prespectrum l2) →
-  UU (l1 ⊔ l2)
-strict-map-Prespectrum r A B =
-  Σ ( (n : ℕ) →
-      pointed-type-Prespectrum A (n +ℕ r) →∗ pointed-type-Prespectrum B n)
-    ( λ f → (n : ℕ) → coherence-strict-map-Prespectrum n r A B f)
-```
diff --git a/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md b/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
index 7aa6b83358..8a2675f0d4 100644
--- a/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
@@ -44,7 +44,8 @@ structure-map-suspension-Prespectrum :
   iterated-suspension-Pointed-Type n A →∗
   Ω (iterated-suspension-Pointed-Type (succ-ℕ n) A)
 structure-map-suspension-Prespectrum A n =
-  pointed-map-unit-suspension-loop-adjunction (iterated-suspension-Pointed-Type n A)
+  pointed-map-unit-suspension-loop-adjunction
+    ( iterated-suspension-Pointed-Type n A)
 
 suspension-Prespectrum : {l : Level} → Pointed-Type l → Prespectrum l
 pr1 (suspension-Prespectrum A) n = iterated-suspension-Pointed-Type n A

From b99369315f685d48d6151981121fbcade0dd43fe Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 18:36:20 +0200
Subject: [PATCH 10/17] self-review

---
 .../iterated-suspensions-of-pointed-types.lagda.md       | 6 ++++--
 src/synthetic-homotopy-theory/prespectra.lagda.md        | 4 ++--
 src/synthetic-homotopy-theory/spectra.lagda.md           | 2 +-
 src/synthetic-homotopy-theory/sphere-spectrum.lagda.md   | 3 ++-
 .../suspension-prespectra.lagda.md                       | 9 +++++----
 ...versal-property-suspensions-of-pointed-types.lagda.md | 6 +-----
 6 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md
index a385455cd2..dd19074436 100644
--- a/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md
+++ b/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md
@@ -21,8 +21,10 @@ open import synthetic-homotopy-theory.suspensions-of-pointed-types
 ## Idea
 
 Given a [pointed type](structured-types.pointed-types.md) `X` and a
-[natural number](elementary-number-theory.natural-numbers.md), we can form the
-`n`-**iterated suspension** of `X`.
+[natural number](elementary-number-theory.natural-numbers.md) `n`, we can form
+the `n`-**iterated suspension** of `X`.
+
+## Definitions
 
 ### The iterated suspension of a pointed type
 
diff --git a/src/synthetic-homotopy-theory/prespectra.lagda.md b/src/synthetic-homotopy-theory/prespectra.lagda.md
index 44e0575834..7e3bb3a276 100644
--- a/src/synthetic-homotopy-theory/prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/prespectra.lagda.md
@@ -25,7 +25,7 @@ open import synthetic-homotopy-theory.loop-spaces
 ## Idea
 
 A **prespectrum** is a [sequence](foundation.sequences.md) of
-[pointed types](structured-types.pointed-types.md) `A n`
+[pointed types](structured-types.pointed-types.md) `Aₙ`
 [equipped](foundation.structure.md) with
 [pointed maps](structured-types.pointed-maps.md)
 
@@ -33,7 +33,7 @@ A **prespectrum** is a [sequence](foundation.sequences.md) of
   ε : Aₙ →∗ ΩAₙ₊₁
 ```
 
-called the **structure maps** of the prespectrum.
+for each `n : ℕ`, called the **structure maps** of the prespectrum.
 
 By the
 [loop-suspension adjunction](synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types.md),
diff --git a/src/synthetic-homotopy-theory/spectra.lagda.md b/src/synthetic-homotopy-theory/spectra.lagda.md
index 6687a1283b..f1498b4f05 100644
--- a/src/synthetic-homotopy-theory/spectra.lagda.md
+++ b/src/synthetic-homotopy-theory/spectra.lagda.md
@@ -32,7 +32,7 @@ A **spectrum** is a [sequence](foundation.sequences.md) of
 [pointed types](structured-types.pointed-types.md) `A` such that
 
 ```text
-  Aₙ ≃∗ Ω Aₙ₊₁
+  Aₙ ≃∗ ΩAₙ₊₁
 ```
 
 for each `n : ℕ`.
diff --git a/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md b/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
index fd391cd86f..cfa365c59e 100644
--- a/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
+++ b/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
@@ -42,4 +42,5 @@ sphere-Prespectrum = suspension-Prespectrum (Fin 2 , zero-Fin 1)
 
 This remains to be defined. To define this, it would be practical to first have
 the lemma that the transposing map of the loop-suspension adjunction preserves
-and reflects equivalences.
+and reflects equivalences. Then we can simply use the transpose of the identity
+function as our structure map.
diff --git a/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md b/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
index 8a2675f0d4..5a88897015 100644
--- a/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
@@ -26,15 +26,16 @@ open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-
 ## Idea
 
 Given a [pointed type](structured-types.pointed-types.md) `A`, the
-[sequence](foundation.sequences.md) of iterated
-[suspensions](synthetic-homotopy-theory.suspensions-of-pointed-types.md) of `A`
+[sequence](foundation.sequences.md) of
+[iterated suspensions](synthetic-homotopy-theory.iterated-suspensions-of-pointed-types.md)
+of `A`
 
 ```text
-  A   Σ¹A   Σ² A   Σ³ A   ...
+  A   Σ¹A   Σ²A   Σ³A   ...
 ```
 
 defines a [prespectrum](synthetic-homotopy-theory.prespectra.md) `Σ^∞A` that we
-call the **suspension spectrum** of `A`.
+call the **suspension prespectrum** of `A`.
 
 ## Definition
 
diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md
index fee3903f99..15720ae895 100644
--- a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md
+++ b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md
@@ -100,7 +100,7 @@ module _
       ( point-Pointed-Type X , point-Pointed-Type X , id)
 ```
 
-#### The transposing map of the adjunction
+#### The transposing maps of the adjunction
 
 ```agda
 module _
@@ -111,11 +111,7 @@ module _
     (suspension-Pointed-Type X →∗ Y) → (X →∗ Ω Y)
   transpose-suspension-loop-adjunction f∗ =
     pointed-map-Ω f∗ ∘∗ pointed-map-unit-suspension-loop-adjunction X
-```
-
-#### The inverse transposing map of the adjunction
 
-```agda
 module _
   {l1 l2 : Level} (X : Pointed-Type l1) (Y : Pointed-Type l2)
   where

From dfc9fc2d7c27c62cc1a9b245e3846ba9724245f9 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 18:37:55 +0200
Subject: [PATCH 11/17] a typo

---
 src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
index 244961cc46..36b6977ff1 100644
--- a/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
@@ -29,7 +29,7 @@ open import synthetic-homotopy-theory.prespectra
 
 ## Idea
 
-A **map of presectra** `f : A → B` is a [sequence](foundation.sequences.md) of
+A **map of prespectra** `f : A → B` is a [sequence](foundation.sequences.md) of
 [pointed maps](structured-types.pointed-maps.md)
 
 ```text

From 1525f151cd5ba074a83843ddcb49095faa35a054 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 19:25:59 +0200
Subject: [PATCH 12/17] review

---
 src/foundation.lagda.md                       |  1 +
 src/foundation/dependent-sequences.lagda.md   | 40 +++++++++++++++++++
 src/foundation/sequences.lagda.md             |  3 +-
 .../functoriality-loop-spaces.lagda.md        |  2 +-
 ...ated-suspensions-of-pointed-types.lagda.md |  7 ++--
 .../loop-spaces.lagda.md                      |  5 +--
 .../maps-of-prespectra.lagda.md               |  3 +-
 .../spectra.lagda.md                          |  3 +-
 .../sphere-spectrum.lagda.md                  |  8 ++--
 .../spheres.lagda.md                          |  2 +-
 10 files changed, 58 insertions(+), 16 deletions(-)
 create mode 100644 src/foundation/dependent-sequences.lagda.md

diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index cb4a973fb7..d8ed51df47 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -83,6 +83,7 @@ open import foundation.dependent-binomial-theorem public
 open import foundation.dependent-epimorphisms public
 open import foundation.dependent-identifications public
 open import foundation.dependent-pair-types public
+open import foundation.dependent-sequences public
 open import foundation.descent-coproduct-types public
 open import foundation.descent-dependent-pair-types public
 open import foundation.descent-empty-types public
diff --git a/src/foundation/dependent-sequences.lagda.md b/src/foundation/dependent-sequences.lagda.md
new file mode 100644
index 0000000000..7590315c29
--- /dev/null
+++ b/src/foundation/dependent-sequences.lagda.md
@@ -0,0 +1,40 @@
+# Dependent sequences
+
+```agda
+module foundation.dependent-sequences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+A **dependent sequence** of elements in a family of types `A : ℕ → UU` is a
+dependent map `(n : ℕ) → A n`.
+
+## Definition
+
+### Dependent sequences of elements in a family of types
+
+```agda
+dependent-sequence : {l : Level} → (ℕ → UU l) → UU l
+dependent-sequence B = (n : ℕ) → B n
+```
+
+### Functorial action on maps of dependent sequences
+
+```agda
+map-dependent-sequence :
+  {l1 l2 : Level} {A : ℕ → UU l1} {B : ℕ → UU l2} →
+  ((n : ℕ) → A n → B n) → dependent-sequence A → dependent-sequence B
+map-dependent-sequence f a = map-Π f a
+```
diff --git a/src/foundation/sequences.lagda.md b/src/foundation/sequences.lagda.md
index 636fff2f05..57f3c52be2 100644
--- a/src/foundation/sequences.lagda.md
+++ b/src/foundation/sequences.lagda.md
@@ -9,6 +9,7 @@ module foundation.sequences where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.dependent-sequences
 open import foundation.universe-levels
 
 open import foundation-core.function-types
@@ -26,7 +27,7 @@ A **sequence** of elements in a type `A` is a map `ℕ → A`.
 
 ```agda
 sequence : {l : Level} → UU l → UU l
-sequence A = ℕ → A
+sequence A = dependent-sequence (λ _ → A)
 ```
 
 ### Functoriality of sequences
diff --git a/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md
index 0207535d46..d489f066fd 100644
--- a/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md
+++ b/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md
@@ -30,7 +30,7 @@ open import synthetic-homotopy-theory.loop-spaces
 Any [pointed map](structured-types.pointed-maps.md) `f : A →∗ B` induces a
 pointed map `pointed-map-Ω f : Ω A →∗ Ω B`. Furthermore, this operation respects
 the groupoidal operations on
-[loop spaces](sytnhetic-homotopy-theory.loop-spaces.md).
+[loop spaces](synthetic-homotopy-theory.loop-spaces.md).
 
 ## Definition
 
diff --git a/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md
index dd19074436..831ae41a13 100644
--- a/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md
+++ b/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md
@@ -9,6 +9,7 @@ module synthetic-homotopy-theory.iterated-suspensions-of-pointed-types where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.iterating-functions
 open import foundation.universe-levels
 
 open import structured-types.pointed-types
@@ -22,7 +23,7 @@ open import synthetic-homotopy-theory.suspensions-of-pointed-types
 
 Given a [pointed type](structured-types.pointed-types.md) `X` and a
 [natural number](elementary-number-theory.natural-numbers.md) `n`, we can form
-the `n`-**iterated suspension** of `X`.
+the **`n`-iterated suspension** of `X`.
 
 ## Definitions
 
@@ -31,7 +32,5 @@ the `n`-**iterated suspension** of `X`.
 ```agda
 iterated-suspension-Pointed-Type :
   {l : Level} (n : ℕ) → Pointed-Type l → Pointed-Type l
-iterated-suspension-Pointed-Type 0 X = X
-iterated-suspension-Pointed-Type (succ-ℕ n) X =
-  suspension-Pointed-Type (iterated-suspension-Pointed-Type n X)
+iterated-suspension-Pointed-Type n = iterate n suspension-Pointed-Type
 ```
diff --git a/src/synthetic-homotopy-theory/loop-spaces.lagda.md b/src/synthetic-homotopy-theory/loop-spaces.lagda.md
index 2800b53e61..588e0065da 100644
--- a/src/synthetic-homotopy-theory/loop-spaces.lagda.md
+++ b/src/synthetic-homotopy-theory/loop-spaces.lagda.md
@@ -25,9 +25,8 @@ open import structured-types.wild-quasigroups
 
 The **loop space** of a [pointed type](structured-types.pointed-types.md) `A` is
 the pointed type of self-[identifications](foundation-core.identity-types.md) of
-the base point of `A`. The loop space comes equipped with a
-[group](group-theory.groups.md) structure induced by the
-[groupoidal](category-theory.groupoids.md) structure on identifications.
+the base point of `A`. The loop space comes equipped with a group-like structure
+induced by the groupoidal-like structure on identifications.
 
 ## Table of files directly related to loop spaces
 
diff --git a/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
index 36b6977ff1..c5f6ef1bd0 100644
--- a/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
@@ -29,7 +29,8 @@ open import synthetic-homotopy-theory.prespectra
 
 ## Idea
 
-A **map of prespectra** `f : A → B` is a [sequence](foundation.sequences.md) of
+A **map of prespectra** `f : A → B` is a
+[sequence](foundation.dependent-sequences.md) of
 [pointed maps](structured-types.pointed-maps.md)
 
 ```text
diff --git a/src/synthetic-homotopy-theory/spectra.lagda.md b/src/synthetic-homotopy-theory/spectra.lagda.md
index f1498b4f05..601e93f242 100644
--- a/src/synthetic-homotopy-theory/spectra.lagda.md
+++ b/src/synthetic-homotopy-theory/spectra.lagda.md
@@ -29,7 +29,8 @@ open import synthetic-homotopy-theory.prespectra
 ## Idea
 
 A **spectrum** is a [sequence](foundation.sequences.md) of
-[pointed types](structured-types.pointed-types.md) `A` such that
+[pointed types](structured-types.pointed-types.md) `A` equipped with an
+equivalence
 
 ```text
   Aₙ ≃∗ ΩAₙ₊₁
diff --git a/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md b/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
index cfa365c59e..0380c848d0 100644
--- a/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
+++ b/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
@@ -40,7 +40,7 @@ sphere-Prespectrum = suspension-Prespectrum (Fin 2 , zero-Fin 1)
 
 ### The sphere spectrum
 
-This remains to be defined. To define this, it would be practical to first have
-the lemma that the transposing map of the loop-suspension adjunction preserves
-and reflects equivalences. Then we can simply use the transpose of the identity
-function as our structure map.
+This definition remains to be formalized. To define this, it would be practical
+to first have the lemma that the transposing map of the loop-suspension
+adjunction preserves and reflects equivalences. Then we can simply use the
+transpose of the identity function as our structure map.
diff --git a/src/synthetic-homotopy-theory/spheres.lagda.md b/src/synthetic-homotopy-theory/spheres.lagda.md
index f307865988..85490fc5db 100644
--- a/src/synthetic-homotopy-theory/spheres.lagda.md
+++ b/src/synthetic-homotopy-theory/spheres.lagda.md
@@ -27,7 +27,7 @@ open import univalent-combinatorics.standard-finite-types
 ## Idea
 
 The **spheres** are defined as
-[iterated suspensions](synthetic-homotopy-theory.iterated-suspensions-pointed-types.md)
+[iterated suspensions](synthetic-homotopy-theory.iterated-suspensions-of-pointed-types.md)
 of the
 [standard two-element type `Fin 2`](univalent-combinatorics.standard-finite-types.md).
 

From 1078629c0cd1834c4d8b95ee96679e7e8f4682d3 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 20:00:08 +0200
Subject: [PATCH 13/17] delete `sphere-spectrum`

---
 src/synthetic-homotopy-theory.lagda.md        |  1 -
 .../prespectra.lagda.md                       |  4 +-
 .../sphere-spectrum.lagda.md                  | 46 -------------------
 3 files changed, 2 insertions(+), 49 deletions(-)
 delete mode 100644 src/synthetic-homotopy-theory/sphere-spectrum.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 7c7b8f00ec..30159972c7 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -64,7 +64,6 @@ open import synthetic-homotopy-theory.pushouts-of-pointed-types public
 open import synthetic-homotopy-theory.sections-descent-circle public
 open import synthetic-homotopy-theory.smash-products-of-pointed-types public
 open import synthetic-homotopy-theory.spectra public
-open import synthetic-homotopy-theory.sphere-spectrum public
 open import synthetic-homotopy-theory.spheres public
 open import synthetic-homotopy-theory.suspension-prespectra public
 open import synthetic-homotopy-theory.suspension-structures public
diff --git a/src/synthetic-homotopy-theory/prespectra.lagda.md b/src/synthetic-homotopy-theory/prespectra.lagda.md
index 7e3bb3a276..05e0684d9d 100644
--- a/src/synthetic-homotopy-theory/prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/prespectra.lagda.md
@@ -37,11 +37,11 @@ for each `n : ℕ`, called the **structure maps** of the prespectrum.
 
 By the
 [loop-suspension adjunction](synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types.md),
-specifying structure maps `Aₙ →∗ Ω Aₙ₊₁` is
+specifying structure maps `Aₙ →∗ ΩAₙ₊₁` is
 [equivalent](foundation-core.equivalences.md) to specifying their adjoint maps
 
 ```text
-  ΣAₙ → Aₙ₊₁.
+  ΣAₙ →∗ Aₙ₊₁.
 ```
 
 ## Definition
diff --git a/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md b/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
deleted file mode 100644
index 0380c848d0..0000000000
--- a/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
+++ /dev/null
@@ -1,46 +0,0 @@
-# The sphere spectrum
-
-```agda
-module synthetic-homotopy-theory.sphere-spectrum where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-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
-```
-
-</details>
-
-## Idea
-
-The [spheres](synthetic-homotopy-theory.spheres.md) `Sⁿ` define a
-[spectrum](synthetic-homotopy-theory.spectra.md)
-
-```text
-  Sⁿ ≃∗ ΩSⁿ⁺¹
-```
-
-which we call the **sphere spectrum**.
-
-## Definition
-
-### The sphere prespectrum
-
-```agda
-sphere-Prespectrum : Prespectrum lzero
-sphere-Prespectrum = suspension-Prespectrum (Fin 2 , zero-Fin 1)
-```
-
-### The sphere spectrum
-
-This definition remains to be formalized. To define this, it would be practical
-to first have the lemma that the transposing map of the loop-suspension
-adjunction preserves and reflects equivalences. Then we can simply use the
-transpose of the identity function as our structure map.

From 5ff4854bd21b5ea5be97050de385dd2a208f3d4e Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 20:56:17 +0200
Subject: [PATCH 14/17] Revert "delete `sphere-spectrum`"

This reverts commit 1078629c0cd1834c4d8b95ee96679e7e8f4682d3.
---
 src/synthetic-homotopy-theory.lagda.md        |  1 +
 .../prespectra.lagda.md                       |  4 +-
 .../sphere-spectrum.lagda.md                  | 46 +++++++++++++++++++
 3 files changed, 49 insertions(+), 2 deletions(-)
 create mode 100644 src/synthetic-homotopy-theory/sphere-spectrum.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 30159972c7..7c7b8f00ec 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -64,6 +64,7 @@ open import synthetic-homotopy-theory.pushouts-of-pointed-types public
 open import synthetic-homotopy-theory.sections-descent-circle public
 open import synthetic-homotopy-theory.smash-products-of-pointed-types public
 open import synthetic-homotopy-theory.spectra public
+open import synthetic-homotopy-theory.sphere-spectrum public
 open import synthetic-homotopy-theory.spheres public
 open import synthetic-homotopy-theory.suspension-prespectra public
 open import synthetic-homotopy-theory.suspension-structures public
diff --git a/src/synthetic-homotopy-theory/prespectra.lagda.md b/src/synthetic-homotopy-theory/prespectra.lagda.md
index 05e0684d9d..7e3bb3a276 100644
--- a/src/synthetic-homotopy-theory/prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/prespectra.lagda.md
@@ -37,11 +37,11 @@ for each `n : ℕ`, called the **structure maps** of the prespectrum.
 
 By the
 [loop-suspension adjunction](synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types.md),
-specifying structure maps `Aₙ →∗ ΩAₙ₊₁` is
+specifying structure maps `Aₙ →∗ Ω Aₙ₊₁` is
 [equivalent](foundation-core.equivalences.md) to specifying their adjoint maps
 
 ```text
-  ΣAₙ →∗ Aₙ₊₁.
+  ΣAₙ → Aₙ₊₁.
 ```
 
 ## Definition
diff --git a/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md b/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
new file mode 100644
index 0000000000..0380c848d0
--- /dev/null
+++ b/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
@@ -0,0 +1,46 @@
+# The sphere spectrum
+
+```agda
+module synthetic-homotopy-theory.sphere-spectrum where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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
+```
+
+</details>
+
+## Idea
+
+The [spheres](synthetic-homotopy-theory.spheres.md) `Sⁿ` define a
+[spectrum](synthetic-homotopy-theory.spectra.md)
+
+```text
+  Sⁿ ≃∗ ΩSⁿ⁺¹
+```
+
+which we call the **sphere spectrum**.
+
+## Definition
+
+### The sphere prespectrum
+
+```agda
+sphere-Prespectrum : Prespectrum lzero
+sphere-Prespectrum = suspension-Prespectrum (Fin 2 , zero-Fin 1)
+```
+
+### The sphere spectrum
+
+This definition remains to be formalized. To define this, it would be practical
+to first have the lemma that the transposing map of the loop-suspension
+adjunction preserves and reflects equivalences. Then we can simply use the
+transpose of the identity function as our structure map.

From cb5e152503355553e23ee439b9bc719b475fb573 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 22:45:36 +0200
Subject: [PATCH 15/17] sphere **pre**spectrum and explanation

---
 src/synthetic-homotopy-theory.lagda.md        |  2 +-
 .../maps-of-prespectra.lagda.md               |  4 +-
 .../prespectra.lagda.md                       | 42 +++++++++++--
 .../spectra.lagda.md                          | 61 ++++++++++++++-----
 .../sphere-prespectrum.lagda.md               | 46 ++++++++++++++
 .../sphere-spectrum.lagda.md                  | 46 --------------
 .../suspension-prespectra.lagda.md            | 32 ++++++++--
 7 files changed, 157 insertions(+), 76 deletions(-)
 create mode 100644 src/synthetic-homotopy-theory/sphere-prespectrum.lagda.md
 delete mode 100644 src/synthetic-homotopy-theory/sphere-spectrum.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 7c7b8f00ec..03be0502f7 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -64,7 +64,7 @@ open import synthetic-homotopy-theory.pushouts-of-pointed-types public
 open import synthetic-homotopy-theory.sections-descent-circle public
 open import synthetic-homotopy-theory.smash-products-of-pointed-types public
 open import synthetic-homotopy-theory.spectra public
-open import synthetic-homotopy-theory.sphere-spectrum public
+open import synthetic-homotopy-theory.sphere-prespectrum public
 open import synthetic-homotopy-theory.spheres public
 open import synthetic-homotopy-theory.suspension-prespectra public
 open import synthetic-homotopy-theory.suspension-structures public
diff --git a/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
index c5f6ef1bd0..d58d854463 100644
--- a/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
@@ -63,8 +63,8 @@ coherence-map-Prespectrum :
 coherence-map-Prespectrum n A B f =
   coherence-square-pointed-maps
     ( f n)
-    ( pointed-structure-map-Prespectrum A n)
-    ( pointed-structure-map-Prespectrum B n)
+    ( pointed-adjoint-structure-map-Prespectrum A n)
+    ( pointed-adjoint-structure-map-Prespectrum B n)
     ( pointed-map-Ω (f (succ-ℕ n)))
 
 map-Prespectrum :
diff --git a/src/synthetic-homotopy-theory/prespectra.lagda.md b/src/synthetic-homotopy-theory/prespectra.lagda.md
index 7e3bb3a276..3d4733d122 100644
--- a/src/synthetic-homotopy-theory/prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/prespectra.lagda.md
@@ -18,6 +18,9 @@ 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
 ```
 
 </details>
@@ -33,7 +36,7 @@ A **prespectrum** is a [sequence](foundation.sequences.md) of
   ε : Aₙ →∗ ΩAₙ₊₁
 ```
 
-for each `n : ℕ`, called the **structure maps** of the prespectrum.
+for each `n : ℕ`, called the **adjoint structure maps** of the prespectrum.
 
 By the
 [loop-suspension adjunction](synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types.md),
@@ -68,17 +71,44 @@ module _
   {l : Level} (A : Prespectrum l) (n : ℕ)
   where
 
-  pointed-structure-map-Prespectrum :
+  pointed-adjoint-structure-map-Prespectrum :
     pointed-type-Prespectrum A n →∗ Ω (pointed-type-Prespectrum A (succ-ℕ n))
-  pointed-structure-map-Prespectrum = pr2 A n
+  pointed-adjoint-structure-map-Prespectrum = pr2 A n
 
-  structure-map-Prespectrum :
+  adjoint-structure-map-Prespectrum :
     type-Prespectrum A n → type-Ω (pointed-type-Prespectrum A (succ-ℕ n))
+  adjoint-structure-map-Prespectrum =
+    map-pointed-map pointed-adjoint-structure-map-Prespectrum
+
+  preserves-point-adjoint-structure-map-Prespectrum :
+    adjoint-structure-map-Prespectrum (point-Prespectrum A n) ＝
+    refl-Ω (pointed-type-Prespectrum A (succ-ℕ n))
+  preserves-point-adjoint-structure-map-Prespectrum =
+    preserves-point-pointed-map pointed-adjoint-structure-map-Prespectrum
+```
+
+### The structure maps of a prespectrum
+
+```agda
+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 =
+    inv-transpose-suspension-loop-adjunction
+      ( pointed-type-Prespectrum A n)
+      ( pointed-type-Prespectrum A (succ-ℕ n))
+      ( pointed-adjoint-structure-map-Prespectrum A 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 (point-Prespectrum A n) ＝
-    refl-Ω (pointed-type-Prespectrum A (succ-ℕ n))
+    structure-map-Prespectrum north-suspension ＝ point-Prespectrum A (succ-ℕ n)
   preserves-point-structure-map-Prespectrum =
     preserves-point-pointed-map pointed-structure-map-Prespectrum
 ```
diff --git a/src/synthetic-homotopy-theory/spectra.lagda.md b/src/synthetic-homotopy-theory/spectra.lagda.md
index 601e93f242..f719099060 100644
--- a/src/synthetic-homotopy-theory/spectra.lagda.md
+++ b/src/synthetic-homotopy-theory/spectra.lagda.md
@@ -22,6 +22,9 @@ open import structured-types.pointed-types
 
 open import synthetic-homotopy-theory.loop-spaces
 open import synthetic-homotopy-theory.prespectra
+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
 ```
 
 </details>
@@ -46,7 +49,8 @@ for each `n : ℕ`.
 is-spectrum-Prop : {l : Level} → Prespectrum l → Prop l
 is-spectrum-Prop A =
   Π-Prop ℕ
-    ( λ n → is-equiv-pointed-map-Prop (pointed-structure-map-Prespectrum A n))
+    ( λ n →
+      is-equiv-pointed-map-Prop (pointed-adjoint-structure-map-Prespectrum A n))
 
 is-spectrum : {l : Level} → Prespectrum l → UU l
 is-spectrum = type-Prop ∘ is-spectrum-Prop
@@ -77,36 +81,61 @@ module _
   point-Spectrum : (n : ℕ) → type-Spectrum n
   point-Spectrum = point-Prespectrum prespectrum-Spectrum
 
-  pointed-structure-map-Spectrum :
+  pointed-adjoint-structure-map-Spectrum :
     (n : ℕ) → pointed-type-Spectrum n →∗ Ω (pointed-type-Spectrum (succ-ℕ n))
-  pointed-structure-map-Spectrum =
-    pointed-structure-map-Prespectrum prespectrum-Spectrum
+  pointed-adjoint-structure-map-Spectrum =
+    pointed-adjoint-structure-map-Prespectrum prespectrum-Spectrum
 
-  structure-map-Spectrum :
+  adjoint-structure-map-Spectrum :
     (n : ℕ) → type-Spectrum n → type-Ω (pointed-type-Spectrum (succ-ℕ n))
-  structure-map-Spectrum = structure-map-Prespectrum prespectrum-Spectrum
+  adjoint-structure-map-Spectrum =
+    adjoint-structure-map-Prespectrum prespectrum-Spectrum
 
-  preserves-point-structure-map-Spectrum :
+  preserves-point-adjoint-structure-map-Spectrum :
     (n : ℕ) →
-    structure-map-Prespectrum (pr1 A) n (point-Prespectrum (pr1 A) n) ＝
+    adjoint-structure-map-Prespectrum (pr1 A) n (point-Prespectrum (pr1 A) n) ＝
     refl-Ω (pointed-type-Prespectrum (pr1 A) (succ-ℕ n))
-  preserves-point-structure-map-Spectrum =
-    preserves-point-structure-map-Prespectrum prespectrum-Spectrum
+  preserves-point-adjoint-structure-map-Spectrum =
+    preserves-point-adjoint-structure-map-Prespectrum prespectrum-Spectrum
 
-  is-equiv-pointed-structure-map-Spectrum :
-    (n : ℕ) → is-equiv-pointed-map (pointed-structure-map-Spectrum n)
-  is-equiv-pointed-structure-map-Spectrum = pr2 A
+  is-equiv-pointed-adjoint-structure-map-Spectrum :
+    (n : ℕ) → is-equiv-pointed-map (pointed-adjoint-structure-map-Spectrum n)
+  is-equiv-pointed-adjoint-structure-map-Spectrum = pr2 A
 
   structure-equiv-Spectrum :
     (n : ℕ) → type-Spectrum n ≃ type-Ω (pointed-type-Spectrum (succ-ℕ n))
-  pr1 (structure-equiv-Spectrum n) = structure-map-Spectrum n
-  pr2 (structure-equiv-Spectrum n) = is-equiv-pointed-structure-map-Spectrum n
+  pr1 (structure-equiv-Spectrum n) = adjoint-structure-map-Spectrum n
+  pr2 (structure-equiv-Spectrum n) =
+    is-equiv-pointed-adjoint-structure-map-Spectrum n
 
   pointed-structure-equiv-Spectrum :
     (n : ℕ) → pointed-type-Spectrum n ≃∗ Ω (pointed-type-Spectrum (succ-ℕ n))
   pr1 (pointed-structure-equiv-Spectrum n) = structure-equiv-Spectrum n
   pr2 (pointed-structure-equiv-Spectrum n) =
-    preserves-point-structure-map-Spectrum n
+    preserves-point-adjoint-structure-map-Spectrum n
+```
+
+### The structure maps of a spectrum
+
+```agda
+module _
+  {l : Level} (A : Spectrum l) (n : ℕ)
+  where
+
+  pointed-structure-map-Spectrum :
+    suspension-Pointed-Type (pointed-type-Spectrum A n) →∗
+    pointed-type-Spectrum A (succ-ℕ n)
+  pointed-structure-map-Spectrum =
+    pointed-structure-map-Prespectrum (prespectrum-Spectrum A) n
+
+  structure-map-Spectrum :
+    suspension (type-Spectrum A n) → type-Spectrum A (succ-ℕ n)
+  structure-map-Spectrum = map-pointed-map pointed-structure-map-Spectrum
+
+  preserves-point-structure-map-Spectrum :
+    structure-map-Spectrum north-suspension ＝ point-Spectrum A (succ-ℕ n)
+  preserves-point-structure-map-Spectrum =
+    preserves-point-pointed-map pointed-structure-map-Spectrum
 ```
 
 ## References
diff --git a/src/synthetic-homotopy-theory/sphere-prespectrum.lagda.md b/src/synthetic-homotopy-theory/sphere-prespectrum.lagda.md
new file mode 100644
index 0000000000..c35bf1483a
--- /dev/null
+++ b/src/synthetic-homotopy-theory/sphere-prespectrum.lagda.md
@@ -0,0 +1,46 @@
+# The sphere prespectrum
+
+```agda
+module synthetic-homotopy-theory.sphere-prespectrum where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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
+```
+
+</details>
+
+## Idea
+
+The [spheres](synthetic-homotopy-theory.spheres.md) `Sⁿ` define a
+[prespectrum](synthetic-homotopy-theory.prespectra.md)
+
+```text
+  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](synthetic-homotopy-theory.spectra.md), as the transposing map of the
+[loop-suspension adjunction](synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types.md)
+does not in general send [equivalences](foundation-core.equivalences.md) to
+equivalences.
+
+## Definition
+
+### The sphere prespectrum
+
+```agda
+sphere-Prespectrum : Prespectrum lzero
+sphere-Prespectrum = suspension-Prespectrum (Fin 2 , zero-Fin 1)
+```
diff --git a/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md b/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
deleted file mode 100644
index 0380c848d0..0000000000
--- a/src/synthetic-homotopy-theory/sphere-spectrum.lagda.md
+++ /dev/null
@@ -1,46 +0,0 @@
-# The sphere spectrum
-
-```agda
-module synthetic-homotopy-theory.sphere-spectrum where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-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
-```
-
-</details>
-
-## Idea
-
-The [spheres](synthetic-homotopy-theory.spheres.md) `Sⁿ` define a
-[spectrum](synthetic-homotopy-theory.spectra.md)
-
-```text
-  Sⁿ ≃∗ ΩSⁿ⁺¹
-```
-
-which we call the **sphere spectrum**.
-
-## Definition
-
-### The sphere prespectrum
-
-```agda
-sphere-Prespectrum : Prespectrum lzero
-sphere-Prespectrum = suspension-Prespectrum (Fin 2 , zero-Fin 1)
-```
-
-### The sphere spectrum
-
-This definition remains to be formalized. To define this, it would be practical
-to first have the lemma that the transposing map of the loop-suspension
-adjunction preserves and reflects equivalences. Then we can simply use the
-transpose of the identity function as our structure map.
diff --git a/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md b/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
index 5a88897015..54a0453fb9 100644
--- a/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
@@ -18,6 +18,7 @@ open import structured-types.pointed-types
 open import synthetic-homotopy-theory.iterated-suspensions-of-pointed-types
 open import synthetic-homotopy-theory.loop-spaces
 open import synthetic-homotopy-theory.prespectra
+open import synthetic-homotopy-theory.suspensions-of-pointed-types
 open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types
 ```
 
@@ -35,20 +36,41 @@ of `A`
 ```
 
 defines a [prespectrum](synthetic-homotopy-theory.prespectra.md) `Σ^∞A` that we
-call the **suspension prespectrum** of `A`.
+call the **suspension prespectrum** of `A`. Its structure map is defined
+degreewise by the identity
+
+```text
+  Σⁿ⁺¹A = Σⁿ⁺¹A   ↝   ΣⁿA →∗ ΩΣⁿ⁺¹A
+```
+
+**Note:** Even though the suspension prespectrum is defined degreewise by the
+adjoint to the identity map, it is not in general a
+[spectrum](synthetic-homotopy-theory.spectra.md), as the transposing map of the
+[loop-suspension adjunction](synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types.md)
+does not generally send [equivalences](foundation-core.equivalences.md) to
+equivalences.
 
 ## Definition
 
 ```agda
-structure-map-suspension-Prespectrum :
+pointed-structure-map-suspension-Prespectrum :
+  {l : Level} (A : Pointed-Type l) (n : ℕ) →
+  suspension-Pointed-Type (iterated-suspension-Pointed-Type n A) →∗
+  iterated-suspension-Pointed-Type (succ-ℕ n) A
+pointed-structure-map-suspension-Prespectrum A n = id-pointed-map
+
+pointed-adjoint-structure-map-suspension-Prespectrum :
   {l : Level} (A : Pointed-Type l) (n : ℕ) →
   iterated-suspension-Pointed-Type n A →∗
   Ω (iterated-suspension-Pointed-Type (succ-ℕ n) A)
-structure-map-suspension-Prespectrum A n =
-  pointed-map-unit-suspension-loop-adjunction
+pointed-adjoint-structure-map-suspension-Prespectrum A n =
+  transpose-suspension-loop-adjunction
     ( iterated-suspension-Pointed-Type n A)
+    ( iterated-suspension-Pointed-Type (succ-ℕ n) A)
+    ( pointed-structure-map-suspension-Prespectrum A n)
 
 suspension-Prespectrum : {l : Level} → Pointed-Type l → Prespectrum l
 pr1 (suspension-Prespectrum A) n = iterated-suspension-Pointed-Type n A
-pr2 (suspension-Prespectrum A) = structure-map-suspension-Prespectrum A
+pr2 (suspension-Prespectrum A) =
+  pointed-adjoint-structure-map-suspension-Prespectrum A
 ```

From f1c83c35f7fe56286317f7ea9c7b0f00c7b555e9 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 22:48:13 +0200
Subject: [PATCH 16/17] a word

---
 src/synthetic-homotopy-theory/sphere-prespectrum.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/synthetic-homotopy-theory/sphere-prespectrum.lagda.md b/src/synthetic-homotopy-theory/sphere-prespectrum.lagda.md
index c35bf1483a..2a8ad9eab1 100644
--- a/src/synthetic-homotopy-theory/sphere-prespectrum.lagda.md
+++ b/src/synthetic-homotopy-theory/sphere-prespectrum.lagda.md
@@ -33,7 +33,7 @@ which we call the **sphere prespectrum**.
 adjoint to the identity map, it is not in general a
 [spectrum](synthetic-homotopy-theory.spectra.md), as the transposing map of the
 [loop-suspension adjunction](synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types.md)
-does not in general send [equivalences](foundation-core.equivalences.md) to
+does not generally send [equivalences](foundation-core.equivalences.md) to
 equivalences.
 
 ## Definition

From a650bd0a1be49b9f99c7995e59a0332b34222975 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 12 Oct 2023 22:52:56 +0200
Subject: [PATCH 17/17] another wording `sequences`

---
 src/foundation/sequences.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/sequences.lagda.md b/src/foundation/sequences.lagda.md
index 57f3c52be2..53f07d5c44 100644
--- a/src/foundation/sequences.lagda.md
+++ b/src/foundation/sequences.lagda.md
@@ -30,7 +30,7 @@ sequence : {l : Level} → UU l → UU l
 sequence A = dependent-sequence (λ _ → A)
 ```
 
-### Functoriality of sequences
+### Functorial action on maps of sequences
 
 ```agda
 map-sequence :