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.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 e2fa18053f..53f07d5c44 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
@@ -18,7 +19,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
 
@@ -26,10 +27,10 @@ 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
+### Functorial action on maps of sequences
 
 ```agda
 map-sequence :
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 d0ae361439..a32857b0e5 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 =
@@ -64,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
@@ -199,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))))
@@ -221,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)
@@ -307,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
@@ -431,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 bfae224a76..03be0502f7 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -48,9 +48,11 @@ 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
+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
@@ -62,7 +64,9 @@ 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-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
 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/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/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..d489f066fd 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](synthetic-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
new file mode 100644
index 0000000000..831ae41a13
--- /dev/null
+++ b/src/synthetic-homotopy-theory/iterated-suspensions-of-pointed-types.lagda.md
@@ -0,0 +1,36 @@
+# 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.iterating-functions
+open import foundation.universe-levels
+
+open import structured-types.pointed-types
+
+open import synthetic-homotopy-theory.suspensions-of-pointed-types
+```
+
+</details>
+
+## Idea
+
+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`.
+
+## Definitions
+
+### 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 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 b61195a3b2..588e0065da 100644
--- a/src/synthetic-homotopy-theory/loop-spaces.lagda.md
+++ b/src/synthetic-homotopy-theory/loop-spaces.lagda.md
@@ -23,9 +23,10 @@ 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-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
new file mode 100644
index 0000000000..d58d854463
--- /dev/null
+++ b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
@@ -0,0 +1,82 @@
+# 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 prespectra** `f : A → B` is a
+[sequence](foundation.dependent-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-adjoint-structure-map-Prespectrum A n)
+    ( pointed-adjoint-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 6b8827e384..3d4733d122 100644
--- a/src/synthetic-homotopy-theory/prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/prespectra.lagda.md
@@ -10,20 +10,42 @@ 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
 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>
 
 ## 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ₙ`
+[equipped](foundation.structure.md) with
+[pointed maps](structured-types.pointed-maps.md)
+
+```text
+  ε : Aₙ →∗ ΩAₙ₊₁
+```
+
+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),
+specifying structure maps `Aₙ →∗ Ω Aₙ₊₁` is
+[equivalent](foundation-core.equivalences.md) to specifying their adjoint maps
+
+```text
+  ΣAₙ → Aₙ₊₁.
+```
 
 ## Definition
 
@@ -31,4 +53,67 @@ 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-adjoint-structure-map-Prespectrum :
+    pointed-type-Prespectrum A n →∗ Ω (pointed-type-Prespectrum A (succ-ℕ n))
+  pointed-adjoint-structure-map-Prespectrum = pr2 A n
+
+  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 north-suspension ＝ point-Prespectrum A (succ-ℕ n)
+  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 b59eb28164..f719099060 100644
--- a/src/synthetic-homotopy-theory/spectra.lagda.md
+++ b/src/synthetic-homotopy-theory/spectra.lagda.md
@@ -10,25 +10,135 @@ 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
+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
+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>
 
 ## 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` equipped with an
+equivalence
+
+```text
+  Aₙ ≃∗ ΩAₙ₊₁
+```
+
+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-adjoint-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 = pointed-type-Prespectrum prespectrum-Spectrum
+
+  type-Spectrum : ℕ → UU l
+  type-Spectrum = type-Prespectrum prespectrum-Spectrum
+
+  point-Spectrum : (n : ℕ) → type-Spectrum n
+  point-Spectrum = point-Prespectrum prespectrum-Spectrum
+
+  pointed-adjoint-structure-map-Spectrum :
+    (n : ℕ) → pointed-type-Spectrum n →∗ Ω (pointed-type-Spectrum (succ-ℕ n))
+  pointed-adjoint-structure-map-Spectrum =
+    pointed-adjoint-structure-map-Prespectrum prespectrum-Spectrum
+
+  adjoint-structure-map-Spectrum :
+    (n : ℕ) → type-Spectrum n → type-Ω (pointed-type-Spectrum (succ-ℕ n))
+  adjoint-structure-map-Spectrum =
+    adjoint-structure-map-Prespectrum prespectrum-Spectrum
+
+  preserves-point-adjoint-structure-map-Spectrum :
+    (n : ℕ) →
+    adjoint-structure-map-Prespectrum (pr1 A) n (point-Prespectrum (pr1 A) n) ＝
+    refl-Ω (pointed-type-Prespectrum (pr1 A) (succ-ℕ n))
+  preserves-point-adjoint-structure-map-Spectrum =
+    preserves-point-adjoint-structure-map-Prespectrum prespectrum-Spectrum
+
+  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) = 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-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
+
+- 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-prespectrum.lagda.md b/src/synthetic-homotopy-theory/sphere-prespectrum.lagda.md
new file mode 100644
index 0000000000..2a8ad9eab1
--- /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 generally 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/spheres.lagda.md b/src/synthetic-homotopy-theory/spheres.lagda.md
index ff3be84437..85490fc5db 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-of-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
new file mode 100644
index 0000000000..54a0453fb9
--- /dev/null
+++ b/src/synthetic-homotopy-theory/suspension-prespectra.lagda.md
@@ -0,0 +1,76 @@
+# 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.suspensions-of-pointed-types
+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.iterated-suspensions-of-pointed-types.md)
+of `A`
+
+```text
+  A   Σ¹A   Σ²A   Σ³A   ...
+```
+
+defines a [prespectrum](synthetic-homotopy-theory.prespectra.md) `Σ^∞A` that we
+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
+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)
+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) =
+  pointed-adjoint-structure-map-suspension-Prespectrum A
+```
diff --git a/src/synthetic-homotopy-theory/suspension-structures.lagda.md b/src/synthetic-homotopy-theory/suspension-structures.lagda.md
index 28e806f73d..68e5ca611b 100644
--- a/src/synthetic-homotopy-theory/suspension-structures.lagda.md
+++ b/src/synthetic-homotopy-theory/suspension-structures.lagda.md
@@ -109,12 +109,9 @@ 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 +218,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 +237,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..b69dfaa20f 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -23,6 +23,7 @@ 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
@@ -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..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
@@ -71,58 +71,54 @@ 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 maps of the adjunction
 
 ```agda
 module _
   {l1 l2 : Level} (X : Pointed-Type l1) (Y : Pointed-Type l2)
   where
 
-  map-equiv-susp-loop-adj :
-    ((suspension-Pointed-Type X) →∗ Y) → (X →∗ Ω Y)
-  map-equiv-susp-loop-adj f∗ =
-    ((pointed-map-Ω f∗) ∘∗ (pointed-map-unit-susp-loop-adj X))
-```
-
-#### The underlying map of the inverse equivalence
+  transpose-suspension-loop-adjunction :
+    (suspension-Pointed-Type X →∗ Y) → (X →∗ Ω Y)
+  transpose-suspension-loop-adjunction f∗ =
+    pointed-map-Ω f∗ ∘∗ pointed-map-unit-suspension-loop-adjunction X
 
-```agda
 module _
   {l1 l2 : Level} (X : Pointed-Type l1) (Y : Pointed-Type l2)
   where
 
-  map-inv-equiv-susp-loop-adj :
-    (X →∗ Ω Y) → ((suspension-Pointed-Type X) →∗ Y)
-  pr1 (map-inv-equiv-susp-loop-adj f∗) =
+  inv-transpose-suspension-loop-adjunction :
+    (X →∗ Ω Y) → (suspension-Pointed-Type X →∗ Y)
+  pr1 (inv-transpose-suspension-loop-adjunction f∗) =
     map-inv-up-suspension
       ( type-Pointed-Type X)
       ( type-Pointed-Type Y)
@@ -130,63 +126,53 @@ 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)
       ( 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.
 
-#### 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