From 6969b19d5acd95bcb3303eef61482cef305da5cc Mon Sep 17 00:00:00 2001
From: Raymond Baker <raymondgarethbaker@gmail.com>
Date: Wed, 2 Aug 2023 13:14:56 -0600
Subject: [PATCH 01/14] add syntax

---
 .../pointed-equivalences.lagda.md             | 36 +++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/src/structured-types/pointed-equivalences.lagda.md b/src/structured-types/pointed-equivalences.lagda.md
index 48d4747ea3..478b3cd212 100644
--- a/src/structured-types/pointed-equivalences.lagda.md
+++ b/src/structured-types/pointed-equivalences.lagda.md
@@ -116,6 +116,42 @@ module _
     preserves-point-comp-pointed-map
       ( pointed-map-pointed-equiv f)
       ( pointed-map-pointed-equiv e)
+
+  _∘e∗_ : (B ≃∗ C) → (A ≃∗ B) → (A ≃∗ C)
+  _∘e∗_ = comp-pointed-equiv
+```
+
+#### Pointed Equivalence Reasoning
+
+The above allows use to use equaltional reasoning to construct pointed
+equivalences
+
+Equivalences can be constructed by equational reasoning in the following way:
+
+```text
+equivalence-reasoning
+  X ≃∗ Y by pointed-equiv-1
+    ≃∗ Z by pointed-equiv-2
+    ≃∗ V by pointed-equiv-3
+```
+
+The equivalence constructed in this way is `equiv-1 ∘e (equiv-2 ∘e equiv-3)`,
+i.e., the equivivalence is associated fully to the right.
+
+```agda
+infixl 1 pointed-equivalence-reasoning_
+infixl 0 step-pointed-equivalence-reasoning
+
+pointed-equivalence-reasoning_ :
+  {l1 : Level} (X : Pointed-Type l1) → X ≃∗ X
+pointed-equivalence-reasoning X = id-pointed-equiv
+
+step-pointed-equivalence-reasoning :
+  {l1 l2 l3 : Level} {X : Pointed-Type l1} {Y : Pointed-Type l2} →
+  (X ≃∗ Y) → (Z : Pointed-Type l3) → (Y ≃∗ Z) → (X ≃∗ Z)
+step-pointed-equivalence-reasoning e Z f = f ∘e∗ e
+
+syntax step-pointed-equivalence-reasoning e Z f = e ≃∗ Z by f
 ```
 
 ### Pointed isomorphisms

From 44870c7711e38ae932c3982d37cf62f6fc2c199b Mon Sep 17 00:00:00 2001
From: Raymond Baker <raymondgarethbaker@gmail.com>
Date: Wed, 2 Aug 2023 13:23:48 -0600
Subject: [PATCH 02/14] Revert "add syntax"

This reverts commit 6969b19d5acd95bcb3303eef61482cef305da5cc.
---
 .../pointed-equivalences.lagda.md             | 36 -------------------
 1 file changed, 36 deletions(-)

diff --git a/src/structured-types/pointed-equivalences.lagda.md b/src/structured-types/pointed-equivalences.lagda.md
index 478b3cd212..48d4747ea3 100644
--- a/src/structured-types/pointed-equivalences.lagda.md
+++ b/src/structured-types/pointed-equivalences.lagda.md
@@ -116,42 +116,6 @@ module _
     preserves-point-comp-pointed-map
       ( pointed-map-pointed-equiv f)
       ( pointed-map-pointed-equiv e)
-
-  _∘e∗_ : (B ≃∗ C) → (A ≃∗ B) → (A ≃∗ C)
-  _∘e∗_ = comp-pointed-equiv
-```
-
-#### Pointed Equivalence Reasoning
-
-The above allows use to use equaltional reasoning to construct pointed
-equivalences
-
-Equivalences can be constructed by equational reasoning in the following way:
-
-```text
-equivalence-reasoning
-  X ≃∗ Y by pointed-equiv-1
-    ≃∗ Z by pointed-equiv-2
-    ≃∗ V by pointed-equiv-3
-```
-
-The equivalence constructed in this way is `equiv-1 ∘e (equiv-2 ∘e equiv-3)`,
-i.e., the equivivalence is associated fully to the right.
-
-```agda
-infixl 1 pointed-equivalence-reasoning_
-infixl 0 step-pointed-equivalence-reasoning
-
-pointed-equivalence-reasoning_ :
-  {l1 : Level} (X : Pointed-Type l1) → X ≃∗ X
-pointed-equivalence-reasoning X = id-pointed-equiv
-
-step-pointed-equivalence-reasoning :
-  {l1 l2 l3 : Level} {X : Pointed-Type l1} {Y : Pointed-Type l2} →
-  (X ≃∗ Y) → (Z : Pointed-Type l3) → (Y ≃∗ Z) → (X ≃∗ Z)
-step-pointed-equivalence-reasoning e Z f = f ∘e∗ e
-
-syntax step-pointed-equivalence-reasoning e Z f = e ≃∗ Z by f
 ```
 
 ### Pointed isomorphisms

From 8e5d6f3b83eee9f88c7fa9fb7283836a05369559 Mon Sep 17 00:00:00 2001
From: Raymond Baker <raymondgarethbaker@gmail.com>
Date: Sun, 6 Aug 2023 16:57:39 -0600
Subject: [PATCH 03/14] definition of dependent suspension structures

---
 .../suspensions-of-types.lagda.md             | 62 +++++++++++++++++++
 1 file changed, 62 insertions(+)

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index a59d2c3c6f..a84e5f4ae6 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -10,6 +10,7 @@ module synthetic-homotopy-theory.suspensions-of-types where
 open import foundation.action-on-identifications-functions
 open import foundation.constant-maps
 open import foundation.contractible-types
+open import foundation.dependent-identifications
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.function-extensionality
@@ -29,6 +30,7 @@ open import structured-types.pointed-maps
 open import structured-types.pointed-types
 
 open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.dependent-universal-property-pushouts
 open import synthetic-homotopy-theory.loop-spaces
 open import synthetic-homotopy-theory.pushouts
 open import synthetic-homotopy-theory.universal-property-pushouts
@@ -411,6 +413,66 @@ module _
           ( up-suspension-merid-susp Z c)))
 ```
 
+### The dependent universal property of suspensions
+
+#### Dependent Suspension Structures
+
+```agda
+module _
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
+  (susp-str : suspension-structure X Y)
+  where
+
+  dependent-suspension-structure : UU (l1 ⊔ l3)
+  dependent-suspension-structure =
+    Σ
+      (B (N-suspension-structure susp-str))
+      (λ N →
+        Σ
+          (B (S-suspension-structure susp-str))
+          (λ S →
+            (x : X) →
+              dependent-identification
+                ( B)
+                ( merid-suspension-structure susp-str x)
+                ( N)
+                ( S)))
+
+module _
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (susp-str : suspension-structure X Y)
+  (B : Y → UU l3) (d-susp-str : dependent-suspension-structure B susp-str)
+  where
+
+
+  N-dependent-suspension-structure : B (N-suspension-structure susp-str)
+  N-dependent-suspension-structure = pr1 (d-susp-str)
+
+  S-dependent-suspension-structure : B (S-suspension-structure susp-str)
+  S-dependent-suspension-structure = (pr1 ∘ pr2) (d-susp-str)
+
+  merid-dependent-suspension-structure :
+    (x : X) →
+      dependent-identification
+      ( B)
+      ( merid-suspension-structure susp-str x)
+      ( N-dependent-suspension-structure)
+      ( S-dependent-suspension-structure)
+  merid-dependent-suspension-structure = (pr2 ∘ pr2) (d-susp-str)
+
+module _
+  {l1 l2 : Level} (X : UU l1) (B : suspension X → UU l1)
+  where
+  
+  dependent-ev-suspension :
+      {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
+      (susp-str-Y : suspension-structure X Y) →
+      (B : Y → UU l3) → ((y : Y) → B y) →
+      {!dependent-suspension-structure
+          ( X)
+          ( {!!})!}
+  dependent-ev-suspension = {!!}
+```
+
 ### The suspension-loop space adjunction
 
 Here we prove the universal property of the suspension of a pointed type: the

From a3d645d6d9f47afa4c403b0dc42d9c8543d51788 Mon Sep 17 00:00:00 2001
From: Raymond Baker <raymondgarethbaker@gmail.com>
Date: Sun, 6 Aug 2023 19:03:35 -0600
Subject: [PATCH 04/14] definition of the dependent universal property

---
 .../suspensions-of-types.lagda.md             | 43 +++++++++++++------
 1 file changed, 31 insertions(+), 12 deletions(-)

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index a84e5f4ae6..4acd4a7858 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -7,6 +7,7 @@ module synthetic-homotopy-theory.suspensions-of-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.constant-maps
 open import foundation.contractible-types
@@ -439,8 +440,9 @@ module _
                 ( S)))
 
 module _
-  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (susp-str : suspension-structure X Y)
-  (B : Y → UU l3) (d-susp-str : dependent-suspension-structure B susp-str)
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
+  (susp-str : suspension-structure X Y)
+  (d-susp-str : dependent-suspension-structure B susp-str)
   where
 
 
@@ -458,21 +460,38 @@ module _
       ( N-dependent-suspension-structure)
       ( S-dependent-suspension-structure)
   merid-dependent-suspension-structure = (pr2 ∘ pr2) (d-susp-str)
+  
+dependent-ev-suspension :
+    {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
+    (susp-str-Y : suspension-structure X Y) (B : Y → UU l3) 
+     → ((y : Y) → B y) →
+    dependent-suspension-structure B susp-str-Y
+pr1 (dependent-ev-suspension susp-str-Y B s) =
+  s (N-suspension-structure susp-str-Y)
+pr1 (pr2 (dependent-ev-suspension susp-str-Y B s)) =
+  s (S-suspension-structure susp-str-Y)
+pr2 (pr2 (dependent-ev-suspension susp-str-Y B s)) =
+  (apd s) ∘ (merid-suspension-structure susp-str-Y)
+```
+
+We can now state the dependent universal property
 
+```agda
 module _
-  {l1 l2 : Level} (X : UU l1) (B : suspension X → UU l1)
+  (l : Level) {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
+  (susp-str-Y : suspension-structure X Y)
   where
-  
-  dependent-ev-suspension :
-      {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
-      (susp-str-Y : suspension-structure X Y) →
-      (B : Y → UU l3) → ((y : Y) → B y) →
-      {!dependent-suspension-structure
-          ( X)
-          ( {!!})!}
-  dependent-ev-suspension = {!!}
+
+  dependent-universal-property-suspension : UU (l1 ⊔ l2 ⊔ lsuc l3)
+  dependent-universal-property-suspension =
+    (B : Y → UU l3) → is-equiv (dependent-ev-suspension susp-str-Y B)
 ```
 
+We now show that the suspension of a type `X` has the dependent universal
+property of suspensions
+
+[To Do]
+
 ### The suspension-loop space adjunction
 
 Here we prove the universal property of the suspension of a pointed type: the

From 8fa65b76a72ab5ae327c64bdf9356c754d41bbb6 Mon Sep 17 00:00:00 2001
From: Raymond Baker <raymondgarethbaker@gmail.com>
Date: Sun, 6 Aug 2023 19:06:53 -0600
Subject: [PATCH 05/14] pre-commit

---
 .../suspensions-of-types.lagda.md                        | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index 4acd4a7858..a2273a6337 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -445,7 +445,6 @@ module _
   (d-susp-str : dependent-suspension-structure B susp-str)
   where
 
-
   N-dependent-suspension-structure : B (N-suspension-structure susp-str)
   N-dependent-suspension-structure = pr1 (d-susp-str)
 
@@ -460,11 +459,11 @@ module _
       ( N-dependent-suspension-structure)
       ( S-dependent-suspension-structure)
   merid-dependent-suspension-structure = (pr2 ∘ pr2) (d-susp-str)
-  
+
 dependent-ev-suspension :
-    {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
-    (susp-str-Y : suspension-structure X Y) (B : Y → UU l3) 
-     → ((y : Y) → B y) →
+    {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
+    (susp-str-Y : suspension-structure X Y) (B : Y → UU l3) →
+    ((y : Y) → B y) →
     dependent-suspension-structure B susp-str-Y
 pr1 (dependent-ev-suspension susp-str-Y B s) =
   s (N-suspension-structure susp-str-Y)

From 78565625b73c875a873f8421fcfc27252fd1b317 Mon Sep 17 00:00:00 2001
From: Raymond Baker <raymondgarethbaker@gmail.com>
Date: Sun, 6 Aug 2023 20:31:34 -0600
Subject: [PATCH 06/14] make explict variable implicit

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

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index a2273a6337..8c14370403 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -441,7 +441,7 @@ module _
 
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
-  (susp-str : suspension-structure X Y)
+  {susp-str : suspension-structure X Y}
   (d-susp-str : dependent-suspension-structure B susp-str)
   where
 

From 3187965b07e79e8711c65a8b1946aa9becd50f93 Mon Sep 17 00:00:00 2001
From: Raymond Baker <raymondgarethbaker@gmail.com>
Date: Sun, 6 Aug 2023 20:37:08 -0600
Subject: [PATCH 07/14] formatting

---
 .../suspensions-of-types.lagda.md                         | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index 8c14370403..96ec143e5a 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -454,10 +454,10 @@ module _
   merid-dependent-suspension-structure :
     (x : X) →
       dependent-identification
-      ( B)
-      ( merid-suspension-structure susp-str x)
-      ( N-dependent-suspension-structure)
-      ( S-dependent-suspension-structure)
+        ( B)
+        ( merid-suspension-structure susp-str x)
+        ( N-dependent-suspension-structure)
+        ( S-dependent-suspension-structure)
   merid-dependent-suspension-structure = (pr2 ∘ pr2) (d-susp-str)
 
 dependent-ev-suspension :

From 3a0670d5a2be8573ac5722d84fc34e53eaeeda5a Mon Sep 17 00:00:00 2001
From: Raymond Baker <raymondgarethbaker@gmail.com>
Date: Mon, 7 Aug 2023 07:01:25 -0600
Subject: [PATCH 08/14] pre-commit

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

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index 638d29662d..73bbb328f0 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -32,8 +32,8 @@ open import structured-types.pointed-maps
 open import structured-types.pointed-types
 
 open import synthetic-homotopy-theory.cocones-under-spans
-open import synthetic-homotopy-theory.dependent-universal-property-pushouts
 open import synthetic-homotopy-theory.conjugation-loops
+open import synthetic-homotopy-theory.dependent-universal-property-pushouts
 open import synthetic-homotopy-theory.functoriality-loop-spaces
 open import synthetic-homotopy-theory.loop-spaces
 open import synthetic-homotopy-theory.pushouts

From 64857c0907e5bcdf873e03bc54b6990b1dcfa413 Mon Sep 17 00:00:00 2001
From: Raymond Baker <96847663+morphismz@users.noreply.github.com>
Date: Mon, 7 Aug 2023 08:06:09 -0600
Subject: [PATCH 09/14] Apply suggestions from code review

agda-unimath styling

Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
---
 .../suspensions-of-types.lagda.md                     | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index 73bbb328f0..ecdffbd99c 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -443,7 +443,16 @@ module _
 
   dependent-suspension-structure : UU (l1 ⊔ l3)
   dependent-suspension-structure =
-    Σ
+    Σ ( B (N-suspension-structure susp-str))
+      ( λ N →
+        Σ ( B (S-suspension-structure susp-str))
+          ( λ S →
+            (x : X) →
+            dependent-identification
+              ( B)
+              ( merid-suspension-structure susp-str x)
+              ( N)
+              ( S)))
       (B (N-suspension-structure susp-str))
       (λ N →
         Σ

From 6b19b0dabe41fbb85ac7f5381ffd484b31d2d605 Mon Sep 17 00:00:00 2001
From: Raymond Baker <raymondgarethbaker@gmail.com>
Date: Mon, 7 Aug 2023 10:42:18 -0600
Subject: [PATCH 10/14] fix typo

---
 .../suspensions-of-types.lagda.md                  | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index ecdffbd99c..89ab298438 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -443,7 +443,8 @@ module _
 
   dependent-suspension-structure : UU (l1 ⊔ l3)
   dependent-suspension-structure =
-    Σ ( B (N-suspension-structure susp-str))
+    Σ
+      ( B (N-suspension-structure susp-str))
       ( λ N →
         Σ ( B (S-suspension-structure susp-str))
           ( λ S →
@@ -453,17 +454,6 @@ module _
               ( merid-suspension-structure susp-str x)
               ( N)
               ( S)))
-      (B (N-suspension-structure susp-str))
-      (λ N →
-        Σ
-          (B (S-suspension-structure susp-str))
-          (λ S →
-            (x : X) →
-              dependent-identification
-                ( B)
-                ( merid-suspension-structure susp-str x)
-                ( N)
-                ( S)))
 
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)

From 44c49e98dfe57ef93c4cdaeb39b0c3d5d0534dec Mon Sep 17 00:00:00 2001
From: Raymond Baker <raymondgarethbaker@gmail.com>
Date: Tue, 8 Aug 2023 17:01:04 -0600
Subject: [PATCH 11/14] characterization of equalities

---
 .../suspensions-of-types.lagda.md             | 156 +++++++++++++++---
 1 file changed, 132 insertions(+), 24 deletions(-)

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index 89ab298438..8e30a2e53f 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -9,6 +9,8 @@ module synthetic-homotopy-theory.suspensions-of-types where
 ```agda
 open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-identifications
+open import foundation.commuting-squares-of-maps
 open import foundation.constant-maps
 open import foundation.contractible-types
 open import foundation.dependent-identifications
@@ -33,6 +35,7 @@ open import structured-types.pointed-types
 
 open import synthetic-homotopy-theory.cocones-under-spans
 open import synthetic-homotopy-theory.conjugation-loops
+open import synthetic-homotopy-theory.dependent-cocones-under-spans
 open import synthetic-homotopy-theory.dependent-universal-property-pushouts
 open import synthetic-homotopy-theory.functoriality-loop-spaces
 open import synthetic-homotopy-theory.loop-spaces
@@ -431,14 +434,25 @@ module _
           ( up-suspension-merid-susp Z c)))
 ```
 
-### The dependent universal property of suspensions
-
-#### Dependent Suspension Structures
+### Dependent Suspension Structures
 
 ```agda
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
-  (susp-str : suspension-structure X Y)
+  (c : suspension-cocone X Y)
+  where
+
+  dependent-suspension-cocone : UU (l1 ⊔ l3)
+  dependent-suspension-cocone =
+    dependent-cocone
+      (const X unit star)
+      (const X unit star)
+      ( c)
+      ( B)
+
+module _
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (susp-str : suspension-structure X Y)
+  (B : Y → UU l3)
   where
 
   dependent-suspension-structure : UU (l1 ⊔ l3)
@@ -454,11 +468,11 @@ module _
               ( merid-suspension-structure susp-str x)
               ( N)
               ( S)))
-
+              
 module _
-  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {B : Y → UU l3}
   {susp-str : suspension-structure X Y}
-  (d-susp-str : dependent-suspension-structure B susp-str)
+  (d-susp-str : dependent-suspension-structure susp-str B)
   where
 
   N-dependent-suspension-structure : B (N-suspension-structure susp-str)
@@ -475,35 +489,129 @@ module _
         ( N-dependent-suspension-structure)
         ( S-dependent-suspension-structure)
   merid-dependent-suspension-structure = (pr2 ∘ pr2) (d-susp-str)
+```
 
-dependent-ev-suspension :
-    {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
-    (susp-str-Y : suspension-structure X Y) (B : Y → UU l3) →
-    ((y : Y) → B y) →
-    dependent-suspension-structure B susp-str-Y
-pr1 (dependent-ev-suspension susp-str-Y B s) =
-  s (N-suspension-structure susp-str-Y)
-pr1 (pr2 (dependent-ev-suspension susp-str-Y B s)) =
-  s (S-suspension-structure susp-str-Y)
-pr2 (pr2 (dependent-ev-suspension susp-str-Y B s)) =
-  (apd s) ∘ (merid-suspension-structure susp-str-Y)
+We characterize equalities in the type of dependent suspension structures:
+
+```agda
+module _
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
+  {susp-str : suspension-structure X Y}
+  (d-susp-str0 d-susp-str1 : dependent-suspension-structure susp-str B)
+  where
+
+  htpy-dependent-suspension-structure : UU (l1 ⊔ l3)
+  htpy-dependent-suspension-structure =
+    Σ (N-dependent-suspension-structure d-susp-str0 ＝ N-dependent-suspension-structure d-susp-str1)
+      λ N-htpy  →
+        Σ (S-dependent-suspension-structure d-susp-str0 ＝ S-dependent-suspension-structure d-susp-str1)
+          λ S-htpy →
+            (x : X) →
+              coherence-square-identifications
+                ( merid-dependent-suspension-structure d-susp-str0 x)
+                ( S-htpy)
+                ( ap (tr B (merid-suspension-structure susp-str x)) N-htpy)
+                ( merid-dependent-suspension-structure d-susp-str1 x)
+                
+module _
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
+  {susp-str : suspension-structure X Y}
+  (d-susp-str0 : dependent-suspension-structure susp-str B)
+  where
+
+  extensionality-dependent-suspension-structure :
+    (d-susp-str1 : dependent-suspension-structure susp-str B) →
+    (d-susp-str0 ＝ d-susp-str1) ≃ htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1
+  extensionality-dependent-suspension-structure =
+    extensionality-Σ
+      ( λ (S1 , m1) (N-htpy) →
+        Σ (S-dependent-suspension-structure d-susp-str0 ＝ S1)
+          (λ S-htpy →
+            (x : X) →
+              coherence-square-identifications
+                ( merid-dependent-suspension-structure d-susp-str0 x)
+                ( S-htpy)
+                ( ap (tr B (merid-suspension-structure susp-str x)) N-htpy)
+                ( m1 x)))
+      ( refl)
+      ( refl , λ x₁ → right-unit)
+      ( λ N → id-equiv)
+      ( extensionality-Σ
+         (λ m1 S-htpy →
+           (x : X) →
+           (merid-dependent-suspension-structure d-susp-str0 x ∙ S-htpy) ＝ m1 x)
+        ( refl)
+        ( λ x₁ → right-unit)
+        ( λ S → id-equiv)
+        ( λ m1 →
+          equiv-concat-htpy right-unit-htpy m1 ∘e inv-equiv equiv-eq-htpy))
+
+module _
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
+  {susp-str : suspension-structure X Y}
+  {d-susp-str0 d-susp-str1 : dependent-suspension-structure susp-str B}
+  where
+  
+  htpy-eq-dependent-suspension-structure :
+    (d-susp-str0 ＝ d-susp-str1) →
+      htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1
+  htpy-eq-dependent-suspension-structure =
+    map-equiv
+      (extensionality-dependent-suspension-structure B d-susp-str0 d-susp-str1)
+
+  eq-htpy-dependent-suspension-structure :
+    htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1 →
+    d-susp-str0 ＝ d-susp-str1
+  eq-htpy-dependent-suspension-structure =
+    map-inv-equiv
+      (extensionality-dependent-suspension-structure B d-susp-str0 d-susp-str1)
+
+module _
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
+  {susp-str : suspension-structure X Y}
+  (d-susp-str : dependent-suspension-structure susp-str B)
+  where
+
+  refl-htpy-dependent-suspension-structure :
+    htpy-dependent-suspension-structure B d-susp-str d-susp-str
+  pr1 refl-htpy-dependent-suspension-structure = refl
+  pr1 (pr2 refl-htpy-dependent-suspension-structure) = refl
+  pr2 (pr2 refl-htpy-dependent-suspension-structure) x = right-unit
+
+  is-refl-refl-htpy-dependent-suspension-structure :
+      refl-htpy-dependent-suspension-structure
+    ＝
+      htpy-eq-dependent-suspension-structure B refl
+  is-refl-refl-htpy-dependent-suspension-structure = refl
 ```
 
-We can now state the dependent universal property
+### The dependent universal property of suspensions
 
 ```agda
+dependent-ev-suspension :
+    {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
+    (susp-str : suspension-structure X Y) (B : Y → UU l3) →
+    ((y : Y) → B y) →
+    dependent-suspension-structure susp-str B
+pr1 (dependent-ev-suspension susp-str B s) =
+  s (N-suspension-structure susp-str)
+pr1 (pr2 (dependent-ev-suspension susp-str B s)) =
+  s (S-suspension-structure susp-str)
+pr2 (pr2 (dependent-ev-suspension susp-str B s)) =
+  (apd s) ∘ (merid-suspension-structure susp-str)
+
 module _
-  (l : Level) {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
-  (susp-str-Y : suspension-structure X Y)
+  (l : Level) {l1 l2 : Level} {X : UU l1} {Y : UU l2}
+  (susp-str : suspension-structure X Y)
   where
 
-  dependent-universal-property-suspension : UU (l1 ⊔ l2 ⊔ lsuc l3)
+  dependent-universal-property-suspension : UU (l1 ⊔ l2 ⊔ lsuc l)
   dependent-universal-property-suspension =
-    (B : Y → UU l3) → is-equiv (dependent-ev-suspension susp-str-Y B)
+    (B : Y → UU l) → is-equiv (dependent-ev-suspension susp-str B)
 ```
 
 We now show that the suspension of a type `X` has the dependent universal
-property of suspensions
+property of suspensions. This requires a few preliminaries.
 
 [To Do]
 

From d6ac98d4221b94c365ccd1550a893114f704cf39 Mon Sep 17 00:00:00 2001
From: Raymond Baker <raymondgarethbaker@gmail.com>
Date: Tue, 8 Aug 2023 17:10:56 -0600
Subject: [PATCH 12/14] pre-commit

---
 .../suspensions-of-types.lagda.md             | 37 +++++++++++++------
 1 file changed, 26 insertions(+), 11 deletions(-)

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index 8e30a2e53f..5f1a67ba18 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -449,9 +449,12 @@ module _
       (const X unit star)
       ( c)
       ( B)
+```
 
+```agda
 module _
-  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (susp-str : suspension-structure X Y)
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
+  (susp-str : suspension-structure X Y)
   (B : Y → UU l3)
   where
 
@@ -468,7 +471,9 @@ module _
               ( merid-suspension-structure susp-str x)
               ( N)
               ( S)))
-              
+```
+
+```agda
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {B : Y → UU l3}
   {susp-str : suspension-structure X Y}
@@ -502,9 +507,15 @@ module _
 
   htpy-dependent-suspension-structure : UU (l1 ⊔ l3)
   htpy-dependent-suspension-structure =
-    Σ (N-dependent-suspension-structure d-susp-str0 ＝ N-dependent-suspension-structure d-susp-str1)
-      λ N-htpy  →
-        Σ (S-dependent-suspension-structure d-susp-str0 ＝ S-dependent-suspension-structure d-susp-str1)
+    Σ
+      ( N-dependent-suspension-structure d-susp-str0
+    ＝
+      N-dependent-suspension-structure d-susp-str1)
+      λ N-htpy →
+        Σ
+          ( S-dependent-suspension-structure d-susp-str0
+        ＝
+          S-dependent-suspension-structure d-susp-str1)
           λ S-htpy →
             (x : X) →
               coherence-square-identifications
@@ -512,7 +523,7 @@ module _
                 ( S-htpy)
                 ( ap (tr B (merid-suspension-structure susp-str x)) N-htpy)
                 ( merid-dependent-suspension-structure d-susp-str1 x)
-                
+
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
   {susp-str : suspension-structure X Y}
@@ -521,7 +532,9 @@ module _
 
   extensionality-dependent-suspension-structure :
     (d-susp-str1 : dependent-suspension-structure susp-str B) →
-    (d-susp-str0 ＝ d-susp-str1) ≃ htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1
+      (d-susp-str0 ＝ d-susp-str1)
+    ≃
+      htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1
   extensionality-dependent-suspension-structure =
     extensionality-Σ
       ( λ (S1 , m1) (N-htpy) →
@@ -537,9 +550,11 @@ module _
       ( refl , λ x₁ → right-unit)
       ( λ N → id-equiv)
       ( extensionality-Σ
-         (λ m1 S-htpy →
-           (x : X) →
-           (merid-dependent-suspension-structure d-susp-str0 x ∙ S-htpy) ＝ m1 x)
+        (λ m1 S-htpy →
+          (x : X) →
+              (merid-dependent-suspension-structure d-susp-str0 x ∙ S-htpy)
+            ＝
+              ( m1 x))
         ( refl)
         ( λ x₁ → right-unit)
         ( λ S → id-equiv)
@@ -551,7 +566,7 @@ module _
   {susp-str : suspension-structure X Y}
   {d-susp-str0 d-susp-str1 : dependent-suspension-structure susp-str B}
   where
-  
+
   htpy-eq-dependent-suspension-structure :
     (d-susp-str0 ＝ d-susp-str1) →
       htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1

From bd8cdfd79e31f7ba53873f2bd6b3f4605ca8ae7f Mon Sep 17 00:00:00 2001
From: Raymond Baker <raymondgarethbaker@gmail.com>
Date: Thu, 10 Aug 2023 11:43:11 -0600
Subject: [PATCH 13/14] formatting

---
 .../suspensions-of-types.lagda.md             | 75 ++++++++-----------
 1 file changed, 31 insertions(+), 44 deletions(-)

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index 5f1a67ba18..7b8c5d1999 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -445,8 +445,8 @@ module _
   dependent-suspension-cocone : UU (l1 ⊔ l3)
   dependent-suspension-cocone =
     dependent-cocone
-      (const X unit star)
-      (const X unit star)
+      ( const X unit star)
+      ( const X unit star)
       ( c)
       ( B)
 ```
@@ -460,8 +460,7 @@ module _
 
   dependent-suspension-structure : UU (l1 ⊔ l3)
   dependent-suspension-structure =
-    Σ
-      ( B (N-suspension-structure susp-str))
+    Σ ( B (N-suspension-structure susp-str))
       ( λ N →
         Σ ( B (S-suspension-structure susp-str))
           ( λ S →
@@ -471,9 +470,7 @@ module _
               ( merid-suspension-structure susp-str x)
               ( N)
               ( S)))
-```
 
-```agda
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {B : Y → UU l3}
   {susp-str : suspension-structure X Y}
@@ -507,22 +504,20 @@ module _
 
   htpy-dependent-suspension-structure : UU (l1 ⊔ l3)
   htpy-dependent-suspension-structure =
-    Σ
-      ( N-dependent-suspension-structure d-susp-str0
-    ＝
-      N-dependent-suspension-structure d-susp-str1)
-      λ N-htpy →
-        Σ
-          ( S-dependent-suspension-structure d-susp-str0
-        ＝
-          S-dependent-suspension-structure d-susp-str1)
-          λ S-htpy →
-            (x : X) →
-              coherence-square-identifications
-                ( merid-dependent-suspension-structure d-susp-str0 x)
-                ( S-htpy)
-                ( ap (tr B (merid-suspension-structure susp-str x)) N-htpy)
-                ( merid-dependent-suspension-structure d-susp-str1 x)
+    Σ (N-dependent-suspension-structure d-susp-str0 ＝
+        N-dependent-suspension-structure d-susp-str1)
+          ( λ N-htpy →
+            Σ ( S-dependent-suspension-structure d-susp-str0 ＝
+                    S-dependent-suspension-structure d-susp-str1)
+                  ( λ S-htpy →
+                    (x : X) →
+                      coherence-square-identifications
+                        ( merid-dependent-suspension-structure d-susp-str0 x)
+                        ( S-htpy)
+                        ( ap
+                          ( tr B (merid-suspension-structure susp-str x))
+                          ( N-htpy))
+                        ( merid-dependent-suspension-structure d-susp-str1 x)))
 
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
@@ -532,14 +527,13 @@ module _
 
   extensionality-dependent-suspension-structure :
     (d-susp-str1 : dependent-suspension-structure susp-str B) →
-      (d-susp-str0 ＝ d-susp-str1)
-    ≃
-      htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1
+      (d-susp-str0 ＝ d-susp-str1) ≃
+      (htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1)
   extensionality-dependent-suspension-structure =
     extensionality-Σ
       ( λ (S1 , m1) (N-htpy) →
         Σ (S-dependent-suspension-structure d-susp-str0 ＝ S1)
-          (λ S-htpy →
+          ( λ S-htpy →
             (x : X) →
               coherence-square-identifications
                 ( merid-dependent-suspension-structure d-susp-str0 x)
@@ -550,11 +544,10 @@ module _
       ( refl , λ x₁ → right-unit)
       ( λ N → id-equiv)
       ( extensionality-Σ
-        (λ m1 S-htpy →
+        ( λ m1 S-htpy →
           (x : X) →
-              (merid-dependent-suspension-structure d-susp-str0 x ∙ S-htpy)
-            ＝
-              ( m1 x))
+            ( merid-dependent-suspension-structure d-susp-str0 x ∙ S-htpy) ＝
+            ( m1 x))
         ( refl)
         ( λ x₁ → right-unit)
         ( λ S → id-equiv)
@@ -572,14 +565,14 @@ module _
       htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1
   htpy-eq-dependent-suspension-structure =
     map-equiv
-      (extensionality-dependent-suspension-structure B d-susp-str0 d-susp-str1)
+      ( extensionality-dependent-suspension-structure B d-susp-str0 d-susp-str1)
 
   eq-htpy-dependent-suspension-structure :
     htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1 →
     d-susp-str0 ＝ d-susp-str1
   eq-htpy-dependent-suspension-structure =
     map-inv-equiv
-      (extensionality-dependent-suspension-structure B d-susp-str0 d-susp-str1)
+      ( extensionality-dependent-suspension-structure B d-susp-str0 d-susp-str1)
 
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
@@ -594,9 +587,8 @@ module _
   pr2 (pr2 refl-htpy-dependent-suspension-structure) x = right-unit
 
   is-refl-refl-htpy-dependent-suspension-structure :
-      refl-htpy-dependent-suspension-structure
-    ＝
-      htpy-eq-dependent-suspension-structure B refl
+    refl-htpy-dependent-suspension-structure ＝
+    htpy-eq-dependent-suspension-structure B refl
   is-refl-refl-htpy-dependent-suspension-structure = refl
 ```
 
@@ -604,10 +596,10 @@ module _
 
 ```agda
 dependent-ev-suspension :
-    {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
-    (susp-str : suspension-structure X Y) (B : Y → UU l3) →
-    ((y : Y) → B y) →
-    dependent-suspension-structure susp-str B
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
+  (susp-str : suspension-structure X Y) (B : Y → UU l3) →
+  ((y : Y) → B y) →
+  dependent-suspension-structure susp-str B
 pr1 (dependent-ev-suspension susp-str B s) =
   s (N-suspension-structure susp-str)
 pr1 (pr2 (dependent-ev-suspension susp-str B s)) =
@@ -625,11 +617,6 @@ module _
     (B : Y → UU l) → is-equiv (dependent-ev-suspension susp-str B)
 ```
 
-We now show that the suspension of a type `X` has the dependent universal
-property of suspensions. This requires a few preliminaries.
-
-[To Do]
-
 ### The suspension-loop space adjunction
 
 Here we prove the universal property of the suspension of a pointed type: the

From d601b03cb2e2e2ba0c8b683025cc9e756ba9f7c7 Mon Sep 17 00:00:00 2001
From: Raymond Baker <96847663+morphismz@users.noreply.github.com>
Date: Fri, 18 Aug 2023 15:27:55 -0600
Subject: [PATCH 14/14] Apply suggestions from code review

implement suggestions

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 .../suspensions-of-types.lagda.md             | 74 +++++++++----------
 1 file changed, 37 insertions(+), 37 deletions(-)

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index 7b8c5d1999..18bfcc64bb 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -485,15 +485,15 @@ module _
 
   merid-dependent-suspension-structure :
     (x : X) →
-      dependent-identification
-        ( B)
-        ( merid-suspension-structure susp-str x)
-        ( N-dependent-suspension-structure)
-        ( S-dependent-suspension-structure)
+    dependent-identification
+      ( B)
+      ( merid-suspension-structure susp-str x)
+      ( N-dependent-suspension-structure)
+      ( S-dependent-suspension-structure)
   merid-dependent-suspension-structure = (pr2 ∘ pr2) (d-susp-str)
 ```
 
-We characterize equalities in the type of dependent suspension structures:
+#### Characterizing equality of dependent suspension structures
 
 ```agda
 module _
@@ -504,20 +504,20 @@ module _
 
   htpy-dependent-suspension-structure : UU (l1 ⊔ l3)
   htpy-dependent-suspension-structure =
-    Σ (N-dependent-suspension-structure d-susp-str0 ＝
+    Σ ( N-dependent-suspension-structure d-susp-str0 ＝
         N-dependent-suspension-structure d-susp-str1)
-          ( λ N-htpy →
-            Σ ( S-dependent-suspension-structure d-susp-str0 ＝
-                    S-dependent-suspension-structure d-susp-str1)
-                  ( λ S-htpy →
-                    (x : X) →
-                      coherence-square-identifications
-                        ( merid-dependent-suspension-structure d-susp-str0 x)
-                        ( S-htpy)
-                        ( ap
-                          ( tr B (merid-suspension-structure susp-str x))
-                          ( N-htpy))
-                        ( merid-dependent-suspension-structure d-susp-str1 x)))
+      ( λ N-htpy →
+        Σ ( S-dependent-suspension-structure d-susp-str0 ＝
+            S-dependent-suspension-structure d-susp-str1)
+          ( λ S-htpy →
+            (x : X) →
+            coherence-square-identifications
+              ( merid-dependent-suspension-structure d-susp-str0 x)
+              ( S-htpy)
+              ( ap
+                ( tr B (merid-suspension-structure susp-str x))
+                ( N-htpy))
+              ( merid-dependent-suspension-structure d-susp-str1 x)))
 
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
@@ -526,33 +526,33 @@ module _
   where
 
   extensionality-dependent-suspension-structure :
-    (d-susp-str1 : dependent-suspension-structure susp-str B) →
-      (d-susp-str0 ＝ d-susp-str1) ≃
-      (htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1)
+    ( d-susp-str1 : dependent-suspension-structure susp-str B) →
+    ( d-susp-str0 ＝ d-susp-str1) ≃
+    ( htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1)
   extensionality-dependent-suspension-structure =
     extensionality-Σ
-      ( λ (S1 , m1) (N-htpy) →
-        Σ (S-dependent-suspension-structure d-susp-str0 ＝ S1)
+      ( λ (S , m) (N-htpy) →
+        Σ (S-dependent-suspension-structure d-susp-str0 ＝ S)
           ( λ S-htpy →
             (x : X) →
-              coherence-square-identifications
-                ( merid-dependent-suspension-structure d-susp-str0 x)
-                ( S-htpy)
-                ( ap (tr B (merid-suspension-structure susp-str x)) N-htpy)
-                ( m1 x)))
+            coherence-square-identifications
+              ( merid-dependent-suspension-structure d-susp-str0 x)
+              ( S-htpy)
+              ( ap (tr B (merid-suspension-structure susp-str x)) N-htpy)
+              ( m x)))
       ( refl)
-      ( refl , λ x₁ → right-unit)
+      ( refl , λ x → right-unit)
       ( λ N → id-equiv)
       ( extensionality-Σ
-        ( λ m1 S-htpy →
+        ( λ m S-htpy →
           (x : X) →
-            ( merid-dependent-suspension-structure d-susp-str0 x ∙ S-htpy) ＝
-            ( m1 x))
+          ( merid-dependent-suspension-structure d-susp-str0 x ∙ S-htpy) ＝
+          ( m x))
         ( refl)
-        ( λ x₁ → right-unit)
+        ( λ x → right-unit)
         ( λ S → id-equiv)
-        ( λ m1 →
-          equiv-concat-htpy right-unit-htpy m1 ∘e inv-equiv equiv-eq-htpy))
+        ( λ m →
+          equiv-concat-htpy right-unit-htpy m ∘e inv-equiv equiv-eq-htpy))
 
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
@@ -562,7 +562,7 @@ module _
 
   htpy-eq-dependent-suspension-structure :
     (d-susp-str0 ＝ d-susp-str1) →
-      htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1
+    htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1
   htpy-eq-dependent-suspension-structure =
     map-equiv
       ( extensionality-dependent-suspension-structure B d-susp-str0 d-susp-str1)