From a8ad651f49db105e8119675cc77e369b94061154 Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Thu, 16 Jan 2025 11:28:57 -0500
Subject: [PATCH 01/18] Pushout draft

---
 source/UF/Pushouts.lagda | 133 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 133 insertions(+)
 create mode 100644 source/UF/Pushouts.lagda

diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
new file mode 100644
index 000000000..a3066e882
--- /dev/null
+++ b/source/UF/Pushouts.lagda
@@ -0,0 +1,133 @@
+Ian Ray, 15th January 2025
+
+Pushouts defined as higher inductive type (in the form of records).
+We postulate point and path constructors, an induction principle and
+computation rules for each constructor.
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+open import UF.FunExt
+
+module UF.Pushouts (fe : Fun-Ext) where
+
+open import MLTT.Spartan
+open import UF.Base
+open import UF.Equiv
+open import UF.EquivalenceExamples
+
+cocone : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+         (f : C → A) (g : C → B)
+         (X : 𝓣  ̇)
+       → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
+cocone {𝓤} {𝓥} {𝓦} {𝓣} {A} {B} {C} f g X =
+ Σ k ꞉ (A → X) , Σ l ꞉ (B → X) , (k ∘ f ∼ l ∘ g)
+
+record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A) (g : C → B) : 𝓤ω
+ where
+ field
+  pushout : 𝓤 ⊔ 𝓥 ⊔ 𝓦  ̇
+  inll : A → pushout 
+  inrr : B → pushout 
+  glue : (c : C) → inll (f c) ＝ inrr (g c)
+  pushout-induction : {P : pushout → 𝓣  ̇}
+                    → (l : (a : A) → P (inll a))
+                    → (r : (b : B) → P (inrr b))
+                    → ((c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+                    → (x : pushout) → P x
+  pushout-ind-comp-l
+   : {P : pushout → 𝓣  ̇}
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → (a : A)
+   → pushout-induction l r G (inll a) ＝ l a 
+  pushout-ind-comp-r
+   : {P : pushout → 𝓣  ̇}
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → (b : B)
+   → pushout-induction l r G (inrr b) ＝ r b
+  pushout-ind-comp-G
+   : {P : pushout → 𝓣  ̇}
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → (c : C)
+   → apd (pushout-induction l r G) (glue c) ∙ pushout-ind-comp-r l r G (g c)
+   ＝ ap (transport P (glue c)) (pushout-ind-comp-l l r G (f c)) ∙ G c
+   
+ pushout-recursion : {D : 𝓣  ̇}
+                   → (l : A → D)
+                   → (r : B → D)
+                   → ((c : C) → l (f c) ＝ r (g c))
+                   → pushout → D
+ pushout-recursion l r G =
+  pushout-induction l r (λ c → (transport-const (glue c) ∙ G c))
+
+ pushout-rec-comp-l : {D : 𝓣  ̇}
+                    → (l : A → D)
+                    → (r : B → D)
+                    → (G : (c : C) → l (f c) ＝ r (g c))
+                    → (a : A)
+                    → pushout-recursion l r G (inll a) ＝ l a
+ pushout-rec-comp-l l r G =
+  pushout-ind-comp-l l r (λ c → (transport-const (glue c) ∙ G c))
+
+ pushout-rec-comp-r : {D : 𝓣  ̇}
+                    → (l : A → D)
+                    → (r : B → D)
+                    → (G : (c : C) → l (f c) ＝ r (g c))
+                    → (b : B)
+                    → pushout-recursion l r G (inrr b) ＝ r b
+ pushout-rec-comp-r l r G =
+  pushout-ind-comp-r l r (λ c → (transport-const (glue c) ∙ G c))
+
+ pushout-rec-comp-G
+  : {D : 𝓣  ̇}
+  → (l : A → D)
+  → (r : B → D)
+  → (G : (c : C) → l (f c) ＝ r (g c))
+  → (c : C)
+  → ap (pushout-recursion l r G) (glue c) ∙ pushout-rec-comp-r l r G (g c) 
+  ＝ pushout-rec-comp-l l r G (f c) ∙ G c
+ pushout-rec-comp-G {𝓣} {D} l r G c = {!!}
+
+ pushout-cocone : cocone f g pushout
+ pushout-cocone = (inll , inrr , glue)
+
+ pushout-universal-property : (X : 𝓣 ̇)
+                            → (pushout → X) ≃ cocone f g X
+ pushout-universal-property X = qinveq ϕ (ψ , ψ-ϕ , ϕ-ψ)
+  where
+   ϕ : (pushout → X) → cocone f g X
+   ϕ u = (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue)
+   ψ : cocone f g X → (pushout → X)
+   ψ (l , r , G) = pushout-recursion l r G
+   ψ-ϕ : ψ ∘ ϕ ∼ id
+   ψ-ϕ u =
+    dfunext fe (pushout-induction
+     (pushout-rec-comp-l (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
+     (pushout-rec-comp-r (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
+     {!!})
+   ϕ-ψ : ϕ ∘ ψ ∼ id
+   ϕ-ψ (l , r , G) =
+    ap ⌜ Σ-assoc ⌝ (to-Σ-＝ (to-×-＝ I II , dfunext fe {!!}))
+    where
+     I = dfunext fe (pushout-rec-comp-l l r G)
+     II = dfunext fe (pushout-rec-comp-r l r G)
+     III : (c : C) → transport {!!} (to-×-＝ I II)
+                               (∼-ap-∘ (ψ (l , r , G)) glue c)
+                   ＝ G c
+     III = {!!}
+      where
+       
+
+
+\end{code}
+
+I : apd (pushout-induction l r ?) (glue c)
+     ＝ ap (pushout-recursion l r G) (glue c)
+   I = ? 

From 18382e336ca7edd7e54bcff74cebf83195fdabaf Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Mon, 20 Jan 2025 01:12:40 -0500
Subject: [PATCH 02/18] Update

---
 source/UF/Base.lagda     | 58 +++++++++++++++++++++++++++++
 source/UF/Pushouts.lagda | 79 ++++++++++++++++++++++++++++++++++------
 2 files changed, 126 insertions(+), 11 deletions(-)

diff --git a/source/UF/Base.lagda b/source/UF/Base.lagda
index a34640844..98098a156 100644
--- a/source/UF/Base.lagda
+++ b/source/UF/Base.lagda
@@ -502,3 +502,61 @@ ap-refl : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) {x : X}
         → ap f (𝓻𝓮𝒻𝓵 x) ＝ 𝓻𝓮𝒻𝓵 (f x)
 ap-refl f = refl
 \end{code}
+
+Added by Ian Ray 18th Jan 2025
+
+\begin{code}
+
+apd-to-ap : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) {x x' : X} (p : x ＝ x')
+          → apd f p ＝ transport-const p ∙ ap f p
+apd-to-ap f refl = refl
+
+apd-from-ap : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) {x x' : X} (p : x ＝ x')
+            → ap f p ＝ transport-const p ⁻¹ ∙ apd f p
+apd-from-ap f refl = refl
+
+\end{code}
+
+We will also add some helpful path lemmas paths. Note that pattern matching
+is not helpful here since association l ∙ q ∙ s is by definition (l ∙ q) ∙ s.
+
+\begin{code}
+
+ap-on-left-is-assoc : {X : 𝓤 ̇ } {x y z z' : X} (l : x ＝ y)
+                      {p q : y ＝ z} {r s : z ＝ z'}
+                    → p ∙ r ＝ q ∙ s
+                    → (l ∙ p) ∙ r ＝ (l ∙ q) ∙ s
+ap-on-left-is-assoc l {p} {q} {r} {s} α = l ∙ p ∙ r   ＝⟨ ∙assoc l p r ⟩
+                                          l ∙ (p ∙ r) ＝⟨ ap (l ∙_) α ⟩
+                                          l ∙ (q ∙ s) ＝⟨ ∙assoc l q s ⁻¹ ⟩
+                                          l ∙ q ∙ s   ∎
+
+ap-on-left-is-assoc' : {X : 𝓤 ̇ } {x y z z' : X} (l : x ＝ y)
+                       (p : y ＝ z') (q : y ＝ z) (s : z ＝ z')
+                     → p ＝ q ∙ s
+                     → l ∙ p ＝ (l ∙ q) ∙ s
+ap-on-left-is-assoc' l p q s α = l ∙ p        ＝⟨ ap (l ∙_) α ⟩
+                                 l ∙ (q ∙ s)  ＝⟨ ∙assoc l q s ⁻¹ ⟩
+                                 l ∙ q ∙ s    ∎
+
+ap-left-inverse : {X : 𝓤 ̇ } {x y z : X} (l : x ＝ y)
+                  {p : x ＝ z} {q : y ＝ z}
+                → p ＝ l ∙ q
+                → l ⁻¹ ∙ p ＝ q
+ap-left-inverse l {p} {q} α =
+ l ⁻¹ ∙ p     ＝⟨ ap-on-left-is-assoc' (l ⁻¹) p l q α ⟩
+ l ⁻¹ ∙ l ∙ q ＝⟨ ap (_∙ q) (left-inverse l) ⟩
+ refl ∙ q     ＝⟨ refl-left-neutral ⟩
+ q            ∎
+
+ap-right-inverse : {X : 𝓤 ̇ } {x y z : X} (r : y ＝ z)
+                   {p : x ＝ z} {q : x ＝ y}
+                 → p ＝ q ∙ r
+                 → p ∙ r ⁻¹ ＝ q
+ap-right-inverse r {p} {q} α =
+ p ∙ r ⁻¹       ＝⟨ ap (_∙ r ⁻¹) α ⟩
+ q ∙ r ∙ r ⁻¹   ＝⟨ ∙assoc q r (r ⁻¹) ⟩
+ q ∙ (r ∙ r ⁻¹) ＝⟨ ap (q ∙_) (sym-is-inverse' r ⁻¹) ⟩
+ q              ∎  
+
+\end{code}
diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index a3066e882..213323e60 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -58,6 +58,18 @@ record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A)
    → (c : C)
    → apd (pushout-induction l r G) (glue c) ∙ pushout-ind-comp-r l r G (g c)
    ＝ ap (transport P (glue c)) (pushout-ind-comp-l l r G (f c)) ∙ G c
+
+\end{code}
+
+We will now observe that the pushout is a cocone and begin deriving some key
+results from the induction principle:
+recursion (along with corresponding computation rules), universal properties
+and uniqueness.
+
+\begin{code}
+
+ pushout-cocone : cocone f g pushout
+ pushout-cocone = (inll , inrr , glue)
    
  pushout-recursion : {D : 𝓣  ̇}
                    → (l : A → D)
@@ -93,11 +105,52 @@ record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A)
   → (c : C)
   → ap (pushout-recursion l r G) (glue c) ∙ pushout-rec-comp-r l r G (g c) 
   ＝ pushout-rec-comp-l l r G (f c) ∙ G c
- pushout-rec-comp-G {𝓣} {D} l r G c = {!!}
-
- pushout-cocone : cocone f g pushout
- pushout-cocone = (inll , inrr , glue)
-
+ pushout-rec-comp-G {𝓣} {D} l r G c =
+  ap (pushout-recursion l r G) (glue c) ∙ pushout-rec-comp-r l r G (g c)                                                                    ＝⟨ III ⟩
+  transport-const (glue c) ⁻¹ ∙ apd (pushout-recursion l r G) (glue c)
+   ∙ pushout-rec-comp-r l r G (g c)                         ＝⟨ V ⟩
+  transport-const (glue c) ⁻¹
+    ∙ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-l l r G (f c))
+    ∙ (transport-const (glue c) ∙ G c)                      ＝⟨ VI ⟩
+  transport-const (glue c) ⁻¹
+    ∙ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-l l r G (f c))
+    ∙ transport-const (glue c) ∙ G c                        ＝⟨ IX ⟩
+  pushout-rec-comp-l l r G (f c) ∙ G c                      ∎
+  where
+   II : ap (pushout-recursion l r G) (glue c)
+      ＝ transport-const (glue c) ⁻¹
+         ∙ apd (pushout-induction l r (λ - → (transport-const (glue -) ∙ G -)))
+               (glue c)
+   II = apd-from-ap (pushout-recursion l r G) (glue c)
+   III = ap (_∙ pushout-rec-comp-r l r G (g c)) II 
+   IV : apd (pushout-recursion l r G) (glue c) ∙ pushout-rec-comp-r l r G (g c)
+      ＝ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-l l r G (f c))
+       ∙ (transport-const (glue c) ∙ G c)
+   IV = pushout-ind-comp-G l r (λ - → (transport-const (glue -) ∙ G -)) c
+   V : transport-const (glue c) ⁻¹ ∙ apd (pushout-recursion l r G) (glue c)
+        ∙ pushout-rec-comp-r l r G (g c)
+     ＝ transport-const (glue c) ⁻¹
+        ∙ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-l l r G (f c))
+        ∙ (transport-const (glue c) ∙ G c)
+   V = ap-on-left-is-assoc (transport-const (glue c) ⁻¹) IV
+   VI = ∙assoc (transport-const (glue c) ⁻¹ ∙ ap (transport (λ - → D) (glue c))
+               (pushout-rec-comp-l l r G (f c))) (transport-const (glue c))
+               (G c) ⁻¹
+   VII : ap (transport (λ - → D) (glue c)) (pushout-rec-comp-l l r G (f c))
+         ∙ transport-const (glue c)
+       ＝ transport-const (glue c) ∙ pushout-rec-comp-l l r G (f c)
+   VII = homotopies-are-natural (transport (λ - → D) (glue c)) id
+          (λ - → transport-const (glue c)) ⁻¹
+   VIII : transport-const (glue c) ⁻¹
+        ∙ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-l l r G (f c))
+        ∙ transport-const (glue c)
+     ＝ pushout-rec-comp-l l r G (f c)
+   VIII = ∙assoc (transport-const (glue c) ⁻¹)
+                 (ap (transport (λ - → D) (glue c))
+                 (pushout-rec-comp-l l r G (f c))) (transport-const (glue c))
+          ∙ ap-left-inverse (transport-const (glue c)) VII 
+   IX = ap (_∙ G c) VIII 
+   
  pushout-universal-property : (X : 𝓣 ̇)
                             → (pushout → X) ≃ cocone f g X
  pushout-universal-property X = qinveq ϕ (ψ , ψ-ϕ , ϕ-ψ)
@@ -122,12 +175,16 @@ record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A)
                                (∼-ap-∘ (ψ (l , r , G)) glue c)
                    ＝ G c
      III = {!!}
-      where
-       
-
 
 \end{code}
 
-I : apd (pushout-induction l r ?) (glue c)
-     ＝ ap (pushout-recursion l r G) (glue c)
-   I = ? 
+I ⁻¹ ∙ apd (pushout-recursion l r G) (glue c)
+            ∙ pushout-rec-comp-r l r G (g c)           ＝⟨ VI ⟩
+       I ⁻¹ ∙ (apd (pushout-recursion l r G) (glue c)
+            ∙ pushout-rec-comp-r l r G (g c))          ＝⟨ VII ⟩
+       I ⁻¹ ∙ (ap (transport (λ - → D) (glue c))
+              (pushout-rec-comp-l l r G (f c))
+            ∙ (transport-const (glue c) ∙ G c))        ＝⟨ VIII ⟩
+       I ⁻¹ ∙ ap (transport (λ - → D) (glue c))
+                 (pushout-rec-comp-l l r G (f c))
+            ∙ (transport-const (glue c) ∙ G c)         ∎

From a07a47c9393caca12f0b87e00f9298f46428c855 Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Mon, 20 Jan 2025 12:44:58 -0500
Subject: [PATCH 03/18] Update

---
 source/UF/Base.lagda     |  6 ++++--
 source/UF/Pushouts.lagda | 36 +++++++++++++++++++-----------------
 2 files changed, 23 insertions(+), 19 deletions(-)

diff --git a/source/UF/Base.lagda b/source/UF/Base.lagda
index 98098a156..19f90d9aa 100644
--- a/source/UF/Base.lagda
+++ b/source/UF/Base.lagda
@@ -517,8 +517,10 @@ apd-from-ap f refl = refl
 
 \end{code}
 
-We will also add some helpful path lemmas paths. Note that pattern matching
-is not helpful here since association l ∙ q ∙ s is by definition (l ∙ q) ∙ s.
+We will also add some helpful path algebra lemmas. Note that pattern matching
+is not helpful here since the path concatenation by definition associates to
+the left: l ∙ q ∙ s ≡ (l ∙ q) ∙ s (where ≡ is definitional). So, as you will
+see below, we have to reassociate before applying on the left.
 
 \begin{code}
 
diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index 213323e60..2e0255b69 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -164,27 +164,29 @@ and uniqueness.
     dfunext fe (pushout-induction
      (pushout-rec-comp-l (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
      (pushout-rec-comp-r (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
-     {!!})
+     I)
+    where
+     I : (c : C)
+       → transport (λ z → (ψ ∘ ϕ) u z ＝ u z) (glue c)
+          (pushout-rec-comp-l (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue) (f c))
+       ＝ pushout-rec-comp-r (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue) (g c)
+     I c = transport (λ z → (ψ ∘ ϕ) u z ＝ u z) (glue c)
+            (pushout-rec-comp-l (u ∘ inll) (u ∘ inrr)
+             (∼-ap-∘ u glue) (f c))                      ＝⟨ {!!} ⟩
+           pushout-rec-comp-r (u ∘ inll) (u ∘ inrr)
+            (∼-ap-∘ u glue) (g c)                        ＝⟨ {!!} ⟩
+           {!!}
    ϕ-ψ : ϕ ∘ ψ ∼ id
    ϕ-ψ (l , r , G) =
-    ap ⌜ Σ-assoc ⌝ (to-Σ-＝ (to-×-＝ I II , dfunext fe {!!}))
+    ap ⌜ Σ-assoc ⌝ (to-Σ-＝ (to-×-＝ I II , dfunext fe III))
     where
      I = dfunext fe (pushout-rec-comp-l l r G)
      II = dfunext fe (pushout-rec-comp-r l r G)
-     III : (c : C) → transport {!!} (to-×-＝ I II)
-                               (∼-ap-∘ (ψ (l , r , G)) glue c)
-                   ＝ G c
-     III = {!!}
+     III : (c : C)
+         → transport (λ z → (λ x → pr₁ z (f x)) ∼ (λ x → pr₂ z (g x)))
+                     (to-×-＝ I II)
+                     (∼-ap-∘ (ψ (l , r , G)) glue) c
+         ＝ G c
+     III c = {!!}
 
 \end{code}
-
-I ⁻¹ ∙ apd (pushout-recursion l r G) (glue c)
-            ∙ pushout-rec-comp-r l r G (g c)           ＝⟨ VI ⟩
-       I ⁻¹ ∙ (apd (pushout-recursion l r G) (glue c)
-            ∙ pushout-rec-comp-r l r G (g c))          ＝⟨ VII ⟩
-       I ⁻¹ ∙ (ap (transport (λ - → D) (glue c))
-              (pushout-rec-comp-l l r G (f c))
-            ∙ (transport-const (glue c) ∙ G c))        ＝⟨ VIII ⟩
-       I ⁻¹ ∙ ap (transport (λ - → D) (glue c))
-                 (pushout-rec-comp-l l r G (f c))
-            ∙ (transport-const (glue c) ∙ G c)         ∎

From 6421ee9e872f1c9f5abb9809175a3a631a7ab6a5 Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Thu, 23 Jan 2025 08:46:16 -0500
Subject: [PATCH 04/18] Update

---
 source/UF/Base.lagda     |  58 ++++++++++++++++++--
 source/UF/Pushouts.lagda | 113 +++++++++++++++++++++++++++++++--------
 2 files changed, 144 insertions(+), 27 deletions(-)

diff --git a/source/UF/Base.lagda b/source/UF/Base.lagda
index 19f90d9aa..9f0900eb2 100644
--- a/source/UF/Base.lagda
+++ b/source/UF/Base.lagda
@@ -541,6 +541,13 @@ ap-on-left-is-assoc' l p q s α = l ∙ p        ＝⟨ ap (l ∙_) α ⟩
                                  l ∙ (q ∙ s)  ＝⟨ ∙assoc l q s ⁻¹ ⟩
                                  l ∙ q ∙ s    ∎
 
+ap-on-left-is-assoc'' : {X : 𝓤 ̇ } {x y z z' : X} (l : x ＝ y)
+                        (p : y ＝ z) (q : y ＝ z') (s : z ＝ z')
+                      → p ∙ s ＝ q
+                      → (l ∙ p) ∙ s ＝ l ∙ q
+ap-on-left-is-assoc'' l p q s α =
+ ap-on-left-is-assoc' l q p s (α ⁻¹) ⁻¹
+
 ap-left-inverse : {X : 𝓤 ̇ } {x y z : X} (l : x ＝ y)
                   {p : x ＝ z} {q : y ＝ z}
                 → p ＝ l ∙ q
@@ -551,14 +558,55 @@ ap-left-inverse l {p} {q} α =
  refl ∙ q     ＝⟨ refl-left-neutral ⟩
  q            ∎
 
+ap-left-inverse' : {X : 𝓤 ̇ } {x y z : X} (l : x ＝ y)
+                   {p : x ＝ z} {q : y ＝ z}
+                 → l ⁻¹ ∙ p ＝ q
+                 → p ＝ l ∙ q
+ap-left-inverse' l {p} {q} α =
+ p            ＝⟨ refl-left-neutral ⁻¹ ⟩
+ refl ∙ p     ＝⟨ ap (_∙ p) (sym-is-inverse' l) ⟩
+ l ∙ l ⁻¹ ∙ p ＝⟨ ap-on-left-is-assoc'' l (l ⁻¹) q p α ⟩
+ l ∙ q        ∎ 
+
 ap-right-inverse : {X : 𝓤 ̇ } {x y z : X} (r : y ＝ z)
                    {p : x ＝ z} {q : x ＝ y}
                  → p ＝ q ∙ r
                  → p ∙ r ⁻¹ ＝ q
-ap-right-inverse r {p} {q} α =
- p ∙ r ⁻¹       ＝⟨ ap (_∙ r ⁻¹) α ⟩
- q ∙ r ∙ r ⁻¹   ＝⟨ ∙assoc q r (r ⁻¹) ⟩
- q ∙ (r ∙ r ⁻¹) ＝⟨ ap (q ∙_) (sym-is-inverse' r ⁻¹) ⟩
- q              ∎  
+ap-right-inverse refl α = α
+
+ap-right-inverse' : {X : 𝓤 ̇ } {x y z : X} (r : y ＝ z)
+                    {p : x ＝ z} {q : x ＝ y}
+                  → p ∙ r ⁻¹ ＝ q
+                  → p ＝ q ∙ r
+ap-right-inverse' refl α = α
+
+\end{code}
+
+We will also add another transport lemma (this may already exist!)
+
+\begin{code}
+
+transport-lemma
+ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {x x' : X}
+ → (p : x ＝ x')
+ → (s s' : X → Y)
+ → (q : s x ＝ s' x)
+ → ap s p ∙ transport (λ - → s - ＝ s' -) p q ＝ q ∙ ap s' p
+transport-lemma refl s s' q =
+ ap s refl ∙ q  ＝⟨ ap (_∙ q) (ap-refl s) ⟩
+ refl ∙ q       ＝⟨ refl-left-neutral ⟩
+ q ∙ refl       ＝⟨ ap (q ∙_) (ap-refl s') ⟩
+ q ∙ ap s' refl ∎ 
+
+transport-lemma'
+ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {x x' : X}
+ → (p : x ＝ x')
+ → (s s' : X → Y)
+ → (q : s x ＝ s' x)
+ → transport (λ - → s - ＝ s' -) p q ＝ ap s p ⁻¹ ∙ q ∙ ap s' p
+transport-lemma' refl s s' q =
+ q                             ＝⟨ refl-left-neutral ⁻¹ ⟩
+ refl ∙ q                      ＝⟨ refl ⟩
+ ap s refl ⁻¹ ∙ q ∙ ap s' refl ∎ 
 
 \end{code}
diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index 2e0255b69..4161ac8f1 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -16,14 +16,34 @@ open import MLTT.Spartan
 open import UF.Base
 open import UF.Equiv
 open import UF.EquivalenceExamples
+open import UF.Subsingletons
+
+\end{code}
+
+We start by defining cocones and characerizing the identity type.
+
+\begin{code}
 
 cocone : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
-         (f : C → A) (g : C → B)
-         (X : 𝓣  ̇)
+         (f : C → A) (g : C → B) (X : 𝓣  ̇)
        → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
 cocone {𝓤} {𝓥} {𝓦} {𝓣} {A} {B} {C} f g X =
  Σ k ꞉ (A → X) , Σ l ꞉ (B → X) , (k ∘ f ∼ l ∘ g)
 
+cocone-family : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                (f : C → A) (g : C → B) (X : 𝓣  ̇)
+              → cocone f g X → cocone f g X → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
+cocone-family f g X (i , j , H) (i' , j' , H') =
+ Σ K ꞉ i ∼ i' , Σ L ꞉ j ∼ j' ,
+  ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g)
+
+cocone-family-is-contractible
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+   (f : C → A) (g : C → B) (X : 𝓣  ̇)
+ → (x : cocone f g X)
+ → is-contr (Σ y ꞉ cocone f g X , cocone-family f g X x y)
+cocone-family-is-contractible f g X (i , j , H) = {!!}
+
 record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A) (g : C → B) : 𝓤ω
  where
  field
@@ -149,7 +169,35 @@ and uniqueness.
                  (ap (transport (λ - → D) (glue c))
                  (pushout-rec-comp-l l r G (f c))) (transport-const (glue c))
           ∙ ap-left-inverse (transport-const (glue c)) VII 
-   IX = ap (_∙ G c) VIII 
+   IX = ap (_∙ G c) VIII
+
+ pushout-uniqueness : (X : 𝓣 ̇)
+                    → (s s' : pushout → X)
+                    → (H : (a : A) → s (inll a) ＝ s' (inll a))
+                    → (H' : (b : B) → s (inrr b) ＝ s' (inrr b))
+                    → (G : (c : C)
+                         → ap s (glue c) ∙ H' (g c) ＝ H (f c) ∙ ap s' (glue c))
+                    → (x : pushout) → s x ＝ s' x
+ pushout-uniqueness X s s' H H' G =
+  pushout-induction H H' I
+  where
+   I : (c : C)
+     → transport (λ - → s - ＝ s' -) (glue c) (H (f c)) ＝ H' (g c)
+   I c = transport (λ - → s - ＝ s' -) (glue c) (H (f c)) ＝⟨ II ⟩
+         ap s (glue c) ⁻¹ ∙ H (f c) ∙ ap s' (glue c)      ＝⟨ III ⟩
+         H' (g c)                                         ∎
+    where
+     II : transport (λ - → s - ＝ s' -) (glue c) (H (f c))
+        ＝ ap s (glue c) ⁻¹ ∙ H (f c) ∙ ap s' (glue c)
+     II = transport-lemma' (glue c) s s' (H (f c))
+     III : ap s (glue c) ⁻¹ ∙ H (f c) ∙ ap s' (glue c) ＝ H' (g c)
+     III =
+      ap s (glue c) ⁻¹ ∙ H (f c) ∙ ap s' (glue c)   ＝⟨ IV ⟩
+      ap s (glue c) ⁻¹ ∙ (H (f c) ∙ ap s' (glue c)) ＝⟨ V ⟩
+      H' (g c)                                       ∎
+      where
+       IV = ∙assoc (ap s (glue c) ⁻¹) (H (f c)) (ap s' (glue c))
+       V = ap-left-inverse (ap s (glue c)) (G c ⁻¹)
    
  pushout-universal-property : (X : 𝓣 ̇)
                             → (pushout → X) ≃ cocone f g X
@@ -160,22 +208,10 @@ and uniqueness.
    ψ : cocone f g X → (pushout → X)
    ψ (l , r , G) = pushout-recursion l r G
    ψ-ϕ : ψ ∘ ϕ ∼ id
-   ψ-ϕ u =
-    dfunext fe (pushout-induction
-     (pushout-rec-comp-l (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
-     (pushout-rec-comp-r (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
-     I)
-    where
-     I : (c : C)
-       → transport (λ z → (ψ ∘ ϕ) u z ＝ u z) (glue c)
-          (pushout-rec-comp-l (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue) (f c))
-       ＝ pushout-rec-comp-r (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue) (g c)
-     I c = transport (λ z → (ψ ∘ ϕ) u z ＝ u z) (glue c)
-            (pushout-rec-comp-l (u ∘ inll) (u ∘ inrr)
-             (∼-ap-∘ u glue) (f c))                      ＝⟨ {!!} ⟩
-           pushout-rec-comp-r (u ∘ inll) (u ∘ inrr)
-            (∼-ap-∘ u glue) (g c)                        ＝⟨ {!!} ⟩
-           {!!}
+   ψ-ϕ u = dfunext fe (pushout-uniqueness X ((ψ ∘ ϕ) u) u
+                   (pushout-rec-comp-l (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
+                   (pushout-rec-comp-r (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
+                   (pushout-rec-comp-G (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue)))
    ϕ-ψ : ϕ ∘ ψ ∼ id
    ϕ-ψ (l , r , G) =
     ap ⌜ Σ-assoc ⌝ (to-Σ-＝ (to-×-＝ I II , dfunext fe III))
@@ -183,10 +219,43 @@ and uniqueness.
      I = dfunext fe (pushout-rec-comp-l l r G)
      II = dfunext fe (pushout-rec-comp-r l r G)
      III : (c : C)
-         → transport (λ z → (λ x → pr₁ z (f x)) ∼ (λ x → pr₂ z (g x)))
-                     (to-×-＝ I II)
+         → transport (λ (l' , r') → l' ∘ f ∼ r' ∘ g) (to-×-＝ I II)
                      (∼-ap-∘ (ψ (l , r , G)) glue) c
          ＝ G c
-     III c = {!!}
+     III c = transport (λ (l' , r') → l' ∘ f ∼ r' ∘ g) (to-×-＝ I II)
+                       (∼-ap-∘ (ψ (l , r , G)) glue) c            ＝⟨ V ⟩
+             pushout-rec-comp-l l r G (f c) ⁻¹
+              ∙ ap (pushout-recursion l r G) (glue c)
+               ∙ pushout-rec-comp-r l r G (g c)                   ＝⟨ VI ⟩
+             pushout-rec-comp-l l r G (f c) ⁻¹
+              ∙ (ap (pushout-recursion l r G) (glue c)
+               ∙ pushout-rec-comp-r l r G (g c))                  ＝⟨ VII ⟩
+             G c                                                  ∎ 
+      where
+       IV : ap (pushout-recursion l r G) (glue c)
+              ∙ pushout-rec-comp-r l r G (g c)
+          ＝ pushout-rec-comp-l l r G (f c)
+              ∙ transport (λ (l' , r') → l' ∘ f ∼ r' ∘ g) (to-×-＝ I II)
+                          (∼-ap-∘ (ψ (l , r , G)) glue) c
+       IV = {!!} ⁻¹
+       V : transport (λ (l' , r') → l' ∘ f ∼ r' ∘ g) (to-×-＝ I II)
+                     (∼-ap-∘ (ψ (l , r , G)) glue) c
+         ＝ pushout-rec-comp-l l r G (f c) ⁻¹
+             ∙ ap (pushout-recursion l r G) (glue c)
+              ∙ pushout-rec-comp-r l r G (g c)
+       V = ap-left-inverse (pushout-rec-comp-l l r G (f c)) IV ⁻¹
+            ∙ (∙assoc (pushout-rec-comp-l l r G (f c) ⁻¹)
+                      (ap (pushout-recursion l r G) (glue c))
+                      (pushout-rec-comp-r l r G (g c))) ⁻¹
+       VI = ∙assoc (pushout-rec-comp-l l r G (f c) ⁻¹)
+                   (ap (pushout-recursion l r G) (glue c))
+                   (pushout-rec-comp-r l r G (g c))
+       VII = ap-left-inverse (pushout-rec-comp-l l r G (f c))
+                             (pushout-rec-comp-G l r G c)
 
 \end{code}
+
+    dfunext fe (pushout-induction
+     (pushout-rec-comp-l (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
+     (pushout-rec-comp-r (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
+     I)

From 335200858e4dad24a32ab39917409b9a6f3e9ade Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Sat, 25 Jan 2025 00:16:54 -0500
Subject: [PATCH 05/18] Update

---
 source/UF/Base.lagda     |  15 ++--
 source/UF/Pushouts.lagda | 151 +++++++++++++++++++++++++--------------
 2 files changed, 108 insertions(+), 58 deletions(-)

diff --git a/source/UF/Base.lagda b/source/UF/Base.lagda
index 9f0900eb2..3d4461bad 100644
--- a/source/UF/Base.lagda
+++ b/source/UF/Base.lagda
@@ -582,29 +582,34 @@ ap-right-inverse' refl α = α
 
 \end{code}
 
-We will also add another transport lemma (this may already exist!)
+We will also add a result that says:
+given two maps, a path in the domain and a path in the codomain between the
+maps at the left endpoint then applying one map to the domain path and
+transporting along that path at the codomain path is the same as following the
+codomain path and applying the other map to the domain path.
+(this may already exist!)
 
 \begin{code}
 
-transport-lemma
+transport-after-ap
  : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {x x' : X}
  → (p : x ＝ x')
  → (s s' : X → Y)
  → (q : s x ＝ s' x)
  → ap s p ∙ transport (λ - → s - ＝ s' -) p q ＝ q ∙ ap s' p
-transport-lemma refl s s' q =
+transport-after-ap refl s s' q =
  ap s refl ∙ q  ＝⟨ ap (_∙ q) (ap-refl s) ⟩
  refl ∙ q       ＝⟨ refl-left-neutral ⟩
  q ∙ refl       ＝⟨ ap (q ∙_) (ap-refl s') ⟩
  q ∙ ap s' refl ∎ 
 
-transport-lemma'
+transport-after-ap'
  : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {x x' : X}
  → (p : x ＝ x')
  → (s s' : X → Y)
  → (q : s x ＝ s' x)
  → transport (λ - → s - ＝ s' -) p q ＝ ap s p ⁻¹ ∙ q ∙ ap s' p
-transport-lemma' refl s s' q =
+transport-after-ap' refl s s' q =
  q                             ＝⟨ refl-left-neutral ⁻¹ ⟩
  refl ∙ q                      ＝⟨ refl ⟩
  ap s refl ⁻¹ ∙ q ∙ ap s' refl ∎ 
diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index 4161ac8f1..7fa06af9a 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -16,7 +16,9 @@ open import MLTT.Spartan
 open import UF.Base
 open import UF.Equiv
 open import UF.EquivalenceExamples
+open import UF.PropIndexedPiSigma
 open import UF.Subsingletons
+open import UF.Yoneda
 
 \end{code}
 
@@ -28,7 +30,7 @@ cocone : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
          (f : C → A) (g : C → B) (X : 𝓣  ̇)
        → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
 cocone {𝓤} {𝓥} {𝓦} {𝓣} {A} {B} {C} f g X =
- Σ k ꞉ (A → X) , Σ l ꞉ (B → X) , (k ∘ f ∼ l ∘ g)
+ Σ i ꞉ (A → X) , Σ j ꞉ (B → X) , (i ∘ f ∼ j ∘ g)
 
 cocone-family : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
                 (f : C → A) (g : C → B) (X : 𝓣  ̇)
@@ -37,12 +39,98 @@ cocone-family f g X (i , j , H) (i' , j' , H') =
  Σ K ꞉ i ∼ i' , Σ L ꞉ j ∼ j' ,
   ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g)
 
-cocone-family-is-contractible
+cocone-map : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+             (f : C → A) (g : C → B) (X : 𝓣  ̇)
+           → (u u' : cocone f g X)
+           → u ＝ u'
+           → cocone-family f g X u u'
+cocone-map f g X (i , j , H) .(i , j , H) refl =
+ (∼-refl , ∼-refl , λ - → refl-left-neutral)
+
+cocone-family-is-identity-system
  : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
    (f : C → A) (g : C → B) (X : 𝓣  ̇)
  → (x : cocone f g X)
  → is-contr (Σ y ꞉ cocone f g X , cocone-family f g X x y)
-cocone-family-is-contractible f g X (i , j , H) = {!!}
+cocone-family-is-identity-system {_} {_} {_} {𝓣} {A} {B} {C} f g X (i , j , H) =
+ equiv-to-singleton e 𝟙-is-singleton
+ where
+  e : (Σ y ꞉ cocone f g X , cocone-family f g X (i , j , H) y) ≃ 𝟙 { 𝓣 }
+  e = (Σ y ꞉ cocone f g X , cocone-family f g X (i , j , H) y) ≃⟨ I ⟩
+      (Σ i' ꞉ (A → X) , Σ j' ꞉ (B → X) ,
+        Σ H' ꞉ (i' ∘ f ∼ j' ∘ g) ,
+         Σ K ꞉ i ∼ i' , Σ L ꞉ j ∼ j' ,
+          ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g))              ≃⟨ II ⟩
+      (Σ i' ꞉ (A → X) , Σ K ꞉ i ∼ i' ,
+        Σ j' ꞉ (B → X) , Σ L ꞉ j ∼ j' ,
+         Σ H' ꞉ (i' ∘ f ∼ j' ∘ g) ,
+          ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g))              ≃⟨ VII ⟩
+      (Σ H' ꞉ (i ∘ f ∼ j ∘ g) , H' ∼ H)                        ≃⟨ IXV ⟩
+      𝟙                                                        ■
+   where
+    I = ≃-comp Σ-assoc (Σ-cong (λ i' → Σ-assoc))
+    II = Σ-cong (λ _ → ≃-comp (Σ-cong
+          (λ _ → ≃-comp Σ-flip (Σ-cong (λ K → Σ-flip)))) Σ-flip)
+    III = (Σ i' ꞉ (A → X) , i ∼ i')  ≃⟨ IV ⟩
+          (Σ i' ꞉ (A → X) , i ＝ i') ≃⟨ V ⟩
+          𝟙                          ■
+     where
+      IV = Σ-cong (λ - → ≃-sym (≃-funext fe i -))
+      V = singleton-≃-𝟙 (singleton-types-are-singletons i)
+    VI = ≃-comp (Σ-cong (λ - → ≃-sym (≃-funext fe j -)))
+                (singleton-≃-𝟙 (singleton-types-are-singletons j))
+    VII = (Σ i' ꞉ (A → X) , Σ K ꞉ i ∼ i' ,
+            Σ j' ꞉ (B → X) , Σ L ꞉ j ∼ j' ,
+             Σ H' ꞉ (i' ∘ f ∼ j' ∘ g) ,
+              ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g))           ≃⟨ IIIV ⟩
+          (Σ (i' , K) ꞉ (Σ i' ꞉ (A → X) , i ∼ i') ,
+            Σ j' ꞉ (B → X) , Σ L ꞉ j ∼ j' ,
+             Σ H' ꞉ (i' ∘ f ∼ j' ∘ g) ,
+              ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g))           ≃⟨ IX ⟩
+           (Σ j' ꞉ (B → X) , Σ L ꞉ j ∼ j' ,
+             Σ H' ꞉ (i ∘ f ∼ j' ∘ g) ,
+              ∼-trans (∼-refl ∘ f) H' ∼ ∼-trans H (L ∘ g))      ≃⟨ XI ⟩
+           (Σ (j' , L) ꞉ (Σ j' ꞉ (B → X) , j ∼ j') ,
+             Σ H' ꞉ (i ∘ f ∼ j' ∘ g) ,
+              ∼-trans (∼-refl ∘ f) H' ∼ ∼-trans H (L ∘ g))      ≃⟨ XII ⟩
+           (Σ H' ꞉ (i ∘ f ∼ j ∘ g) ,
+             ∼-trans (∼-refl ∘ f) H' ∼ ∼-trans H (∼-refl ∘ g))  ≃⟨ XIII ⟩
+           (Σ H' ꞉ (i ∘ f ∼ j ∘ g) , H' ∼ H)                    ■
+     where
+      IIIV = ≃-sym Σ-assoc
+      IX = prop-indexed-sum (equiv-to-prop III 𝟙-is-prop) (i , ∼-refl)
+      XI = ≃-sym Σ-assoc
+      XII = prop-indexed-sum (equiv-to-prop VI 𝟙-is-prop) (j , ∼-refl)
+      XIII = Σ-cong (λ H' → Π-cong fe fe (λ c → ＝-cong (refl ∙ H' c)
+                    (∼-trans H (λ _ → refl) c) refl-left-neutral
+                      (refl-right-neutral (H c) ⁻¹)))
+    IXV = ≃-comp (Σ-cong (λ - → ≃-sym (≃-funext fe - H)))
+                 (singleton-≃-𝟙 (equiv-to-singleton (Σ-cong (λ - → ＝-flip))
+                 (singleton-types-are-singletons H)))
+
+cocone-identity-characterization : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                                   (f : C → A) (g : C → B) (X : 𝓣  ̇)
+                                 → (u u' : cocone f g X)
+                                 → (u ＝ u') ≃ (cocone-family f g X u u')
+cocone-identity-characterization f g X u u' =
+ (cocone-map f g X u u' ,
+   Yoneda-Theorem-forth u (cocone-map f g X u)
+                        (cocone-family-is-identity-system f g X u) u')
+
+inverse-cocone-map : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                     (f : C → A) (g : C → B) (X : 𝓣  ̇)
+                   → (u u' : cocone f g X)
+                   → cocone-family f g X u u'
+                   → u ＝ u'
+inverse-cocone-map f g X u u' =
+ ⌜ (cocone-identity-characterization f g X u u') ⌝⁻¹
+
+\end{code}
+
+Now we will use a record type to give the pushout, point and path constructors,
+and the induction principle along with propositional computation rules.
+
+\begin{code}
 
 record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A) (g : C → B) : 𝓤ω
  where
@@ -83,8 +171,8 @@ record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A)
 
 We will now observe that the pushout is a cocone and begin deriving some key
 results from the induction principle:
-recursion (along with corresponding computation rules), universal properties
-and uniqueness.
+recursion (along with corresponding computation rules), uniqueness and the
+universal property.
 
 \begin{code}
 
@@ -187,10 +275,7 @@ and uniqueness.
          ap s (glue c) ⁻¹ ∙ H (f c) ∙ ap s' (glue c)      ＝⟨ III ⟩
          H' (g c)                                         ∎
     where
-     II : transport (λ - → s - ＝ s' -) (glue c) (H (f c))
-        ＝ ap s (glue c) ⁻¹ ∙ H (f c) ∙ ap s' (glue c)
-     II = transport-lemma' (glue c) s s' (H (f c))
-     III : ap s (glue c) ⁻¹ ∙ H (f c) ∙ ap s' (glue c) ＝ H' (g c)
+     II = transport-after-ap' (glue c) s s' (H (f c))
      III =
       ap s (glue c) ⁻¹ ∙ H (f c) ∙ ap s' (glue c)   ＝⟨ IV ⟩
       ap s (glue c) ⁻¹ ∙ (H (f c) ∙ ap s' (glue c)) ＝⟨ V ⟩
@@ -214,48 +299,8 @@ and uniqueness.
                    (pushout-rec-comp-G (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue)))
    ϕ-ψ : ϕ ∘ ψ ∼ id
    ϕ-ψ (l , r , G) =
-    ap ⌜ Σ-assoc ⌝ (to-Σ-＝ (to-×-＝ I II , dfunext fe III))
-    where
-     I = dfunext fe (pushout-rec-comp-l l r G)
-     II = dfunext fe (pushout-rec-comp-r l r G)
-     III : (c : C)
-         → transport (λ (l' , r') → l' ∘ f ∼ r' ∘ g) (to-×-＝ I II)
-                     (∼-ap-∘ (ψ (l , r , G)) glue) c
-         ＝ G c
-     III c = transport (λ (l' , r') → l' ∘ f ∼ r' ∘ g) (to-×-＝ I II)
-                       (∼-ap-∘ (ψ (l , r , G)) glue) c            ＝⟨ V ⟩
-             pushout-rec-comp-l l r G (f c) ⁻¹
-              ∙ ap (pushout-recursion l r G) (glue c)
-               ∙ pushout-rec-comp-r l r G (g c)                   ＝⟨ VI ⟩
-             pushout-rec-comp-l l r G (f c) ⁻¹
-              ∙ (ap (pushout-recursion l r G) (glue c)
-               ∙ pushout-rec-comp-r l r G (g c))                  ＝⟨ VII ⟩
-             G c                                                  ∎ 
-      where
-       IV : ap (pushout-recursion l r G) (glue c)
-              ∙ pushout-rec-comp-r l r G (g c)
-          ＝ pushout-rec-comp-l l r G (f c)
-              ∙ transport (λ (l' , r') → l' ∘ f ∼ r' ∘ g) (to-×-＝ I II)
-                          (∼-ap-∘ (ψ (l , r , G)) glue) c
-       IV = {!!} ⁻¹
-       V : transport (λ (l' , r') → l' ∘ f ∼ r' ∘ g) (to-×-＝ I II)
-                     (∼-ap-∘ (ψ (l , r , G)) glue) c
-         ＝ pushout-rec-comp-l l r G (f c) ⁻¹
-             ∙ ap (pushout-recursion l r G) (glue c)
-              ∙ pushout-rec-comp-r l r G (g c)
-       V = ap-left-inverse (pushout-rec-comp-l l r G (f c)) IV ⁻¹
-            ∙ (∙assoc (pushout-rec-comp-l l r G (f c) ⁻¹)
-                      (ap (pushout-recursion l r G) (glue c))
-                      (pushout-rec-comp-r l r G (g c))) ⁻¹
-       VI = ∙assoc (pushout-rec-comp-l l r G (f c) ⁻¹)
-                   (ap (pushout-recursion l r G) (glue c))
-                   (pushout-rec-comp-r l r G (g c))
-       VII = ap-left-inverse (pushout-rec-comp-l l r G (f c))
-                             (pushout-rec-comp-G l r G c)
-
+    inverse-cocone-map f g X ((ϕ ∘ ψ) (l , r , G)) (l , r , G)
+     (pushout-rec-comp-l l r G , pushout-rec-comp-r l r G ,
+      ∼-sym (pushout-rec-comp-G l r G))
+   
 \end{code}
-
-    dfunext fe (pushout-induction
-     (pushout-rec-comp-l (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
-     (pushout-rec-comp-r (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
-     I)

From 4fe2e56870157b4adf6c484e1672f1d610a4ca95 Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Sat, 25 Jan 2025 00:21:36 -0500
Subject: [PATCH 06/18] Updating comments

---
 source/UF/Pushouts.lagda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index 7fa06af9a..92142c18a 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -1,8 +1,8 @@
 Ian Ray, 15th January 2025
 
-Pushouts defined as higher inductive type (in the form of records).
+Pushouts are defined as higher inductive type (in the form of a record type).
 We postulate point and path constructors, an induction principle and
-computation rules for each constructor.
+propositional computation rules for each constructor.
 
 \begin{code}
 
@@ -115,7 +115,7 @@ cocone-identity-characterization : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
 cocone-identity-characterization f g X u u' =
  (cocone-map f g X u u' ,
    Yoneda-Theorem-forth u (cocone-map f g X u)
-                        (cocone-family-is-identity-system f g X u) u')
+    (cocone-family-is-identity-system f g X u) u')
 
 inverse-cocone-map : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
                      (f : C → A) (g : C → B) (X : 𝓣  ̇)

From b328465a90e490cd1486a51ca57e67c00162793b Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Sun, 26 Jan 2025 11:54:51 -0500
Subject: [PATCH 07/18] Giving UP, Ind and computation rules.

---
 source/UF/Pushouts.lagda | 73 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 73 insertions(+)

diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index 92142c18a..9ebe185dc 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -127,6 +127,79 @@ inverse-cocone-map f g X u u' =
 
 \end{code}
 
+Now we will define the universal property, induction principle and propositional
+computation rules for pushouts and show they are inter-derivable.
+
+\begin{code}
+
+Pushout-Universal-Property
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (X : 𝓣  ̇)
+   (f : C → A) (g : C → B) (i : A → S) (j : B → S) (G : i ∘ f ∼ j ∘ g) 
+ → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓤' ⊔ 𝓣  ̇
+Pushout-Universal-Property S X f g i j G 
+ = (S → X) ≃ cocone f g X
+
+Pushout-Induction-Principle
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
+   (f : C → A) (g : C → B) (i : A → S) (j : B → S) (G : i ∘ f ∼ j ∘ g)
+ → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓤' ⊔ 𝓣  ̇
+Pushout-Induction-Principle {_} {_} {_} {_} {_} {A} {B} {C} S P f g i j G 
+ = (l : (a : A) → P (i a))
+ → (r : (b : B) → P (j b))
+ → ((c : C) → transport P (G c) (l (f c)) ＝ r (g c))
+ → (x : S) → P x
+
+Pushout-Propositional-Computation-Rule₁
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
+   (f : C → A) (g : C → B) (i : A → S) (j : B → S) (G : i ∘ f ∼ j ∘ g)
+   (S-ind : Pushout-Induction-Principle S P f g i j G)
+ → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
+Pushout-Propositional-Computation-Rule₁
+ {_} {_} {_} {_} {_} {A} {B} {C} S P f g i j G S-ind
+ = (l : (a : A) → P (i a))
+ → (r : (b : B) → P (j b))
+ → (H : (c : C) → transport P (G c) (l (f c)) ＝ r (g c))
+ → (a : A)
+ → S-ind l r H (i a) ＝ l a
+
+Pushout-Propositional-Computation-Rule₂
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
+   (f : C → A) (g : C → B) (i : A → S) (j : B → S) (G : i ∘ f ∼ j ∘ g)
+   (S-ind : Pushout-Induction-Principle S P f g i j G)
+ → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
+Pushout-Propositional-Computation-Rule₂
+ {_} {_} {_} {_} {_} {A} {B} {C} S P f g i j G S-ind
+ = (l : (a : A) → P (i a))
+ → (r : (b : B) → P (j b))
+ → (H : (c : C) → transport P (G c) (l (f c)) ＝ r (g c))
+ → (b : B)
+ → S-ind l r H (j b) ＝ r b
+
+Pushout-Propositional-Computation-Rule₃
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
+   (f : C → A) (g : C → B) (i : A → S) (j : B → S) (G : i ∘ f ∼ j ∘ g)
+   (S-ind : Pushout-Induction-Principle S P f g i j G)
+   (S-comp₁ : Pushout-Propositional-Computation-Rule₁ S P f g i j G S-ind)
+   (S-comp₂ : Pushout-Propositional-Computation-Rule₂ S P f g i j G S-ind)
+ → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
+Pushout-Propositional-Computation-Rule₃
+ {_} {_} {_} {_} {_}{A} {B} {C} S P f g i j G S-ind S-comp₁ S-comp₂
+ = (l : (a : A) → P (i a))
+ → (r : (b : B) → P (j b))
+ → (H : (c : C) → transport P (G c) (l (f c)) ＝ r (g c))
+ → (c : C)
+ → apd (S-ind l r H) (G c) ∙ S-comp₂ l r H (g c)
+ ＝ ap (transport P (G c)) (S-comp₁ l r H (f c)) ∙ H c
+
+Pushout-Universal-Property-implies-Induction
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (X : 𝓣  ̇) (P : S → 𝓣  ̇)
+   (f : C → A) (g : C → B) (i : A → S) (j : B → S) (G : i ∘ f ∼ j ∘ g)
+ → Pushout-Universal-Property S X f g i j G
+ → Pushout-Induction-Principle S P f g i j G
+Pushout-Universal-Property-implies-Induction = ?
+
+\end{code}
+
 Now we will use a record type to give the pushout, point and path constructors,
 and the induction principle along with propositional computation rules.
 

From 88314c2893f786a58fa6a0f5e54b4cf58da64e67 Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Mon, 27 Jan 2025 20:19:02 -0500
Subject: [PATCH 08/18] Adding dependent universal property

---
 source/UF/Pushouts.lagda | 174 +++++++++++++++++++++++++++++----------
 1 file changed, 131 insertions(+), 43 deletions(-)

diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index 9ebe185dc..a6780feac 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -22,7 +22,7 @@ open import UF.Yoneda
 
 \end{code}
 
-We start by defining cocones and characerizing the identity type.
+We start by defining cocones and characerizing their identity type.
 
 \begin{code}
 
@@ -32,6 +32,24 @@ cocone : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
 cocone {𝓤} {𝓥} {𝓦} {𝓣} {A} {B} {C} f g X =
  Σ i ꞉ (A → X) , Σ j ꞉ (B → X) , (i ∘ f ∼ j ∘ g)
 
+cocone-vertical-map : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                      (f : C → A) (g : C → B) (X : 𝓣  ̇)
+                    → cocone f g X
+                    → (A → X)
+cocone-vertical-map f g X (i , j , K) = i
+
+cocone-horizontal-map : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                        (f : C → A) (g : C → B) (X : 𝓣  ̇)
+                      → cocone f g X
+                      → (B → X)
+cocone-horizontal-map f g X (i , j , K) = j
+
+cocone-commuting-square : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                          (f : C → A) (g : C → B) (X : 𝓣  ̇)
+                        → ((i , j , K) : cocone f g X)
+                        → i ∘ f ∼ j ∘ g
+cocone-commuting-square f g X (i , j , K) = K
+
 cocone-family : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
                 (f : C → A) (g : C → B) (X : 𝓣  ̇)
               → cocone f g X → cocone f g X → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
@@ -39,12 +57,14 @@ cocone-family f g X (i , j , H) (i' , j' , H') =
  Σ K ꞉ i ∼ i' , Σ L ꞉ j ∼ j' ,
   ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g)
 
-cocone-map : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
-             (f : C → A) (g : C → B) (X : 𝓣  ̇)
-           → (u u' : cocone f g X)
-           → u ＝ u'
-           → cocone-family f g X u u'
-cocone-map f g X (i , j , H) .(i , j , H) refl =
+canonical-map-from-identity-to-cocone-family
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+   (f : C → A) (g : C → B) (X : 𝓣  ̇)
+ → (u u' : cocone f g X)
+ → u ＝ u'
+ → cocone-family f g X u u'
+canonical-map-from-identity-to-cocone-family
+ f g X (i , j , H) .(i , j , H) refl =
  (∼-refl , ∼-refl , λ - → refl-left-neutral)
 
 cocone-family-is-identity-system
@@ -113,8 +133,8 @@ cocone-identity-characterization : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
                                  → (u u' : cocone f g X)
                                  → (u ＝ u') ≃ (cocone-family f g X u u')
 cocone-identity-characterization f g X u u' =
- (cocone-map f g X u u' ,
-   Yoneda-Theorem-forth u (cocone-map f g X u)
+ (canonical-map-from-identity-to-cocone-family f g X u u' ,
+   Yoneda-Theorem-forth u (canonical-map-from-identity-to-cocone-family f g X u)
     (cocone-family-is-identity-system f g X u) u')
 
 inverse-cocone-map : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
@@ -127,63 +147,115 @@ inverse-cocone-map f g X u u' =
 
 \end{code}
 
-Now we will define the universal property, induction principle and propositional
-computation rules for pushouts and show they are inter-derivable.
+We also introduce the notion of a dependent cocone.
+
+\begin{code}
+
+dependent-cocone : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                   (f : C → A) (g : C → B) (X : 𝓣  ̇)
+                   (t : cocone f g X) (P : X → 𝓣'  ̇)
+                 → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣'  ̇
+dependent-cocone {_} {_} {_} {_} {_} {A} {B} {C} f g X (i , j , H) P =
+ Σ i' ꞉ ((a : A) → P (i a)) , Σ j' ꞉ ((b : B) → P (j b)) ,
+  ((c : C) → transport P (H c) (i' (f c)) ＝ j' (g c))
+
+\end{code}
+
+Now we will define the (dependent) universal property, induction principle and
+propositional computation rules for pushouts and show they are inter-derivable*.
+
+*In fact we will only show:
+(1)
+  The dependent universal propery implies the induction principle and
+  propositional computation rules.
+
+(2)
+  The induction principle and propositional computationrules implies the
+  (non-dependeny) universal property.
+
+We will not show
+(3)
+  The (non-dependent) universal property implies the dependent universal
+  property.
+
+(3) Is shown in the Agda Unimath library (*link*). It involves something called
+the pullback property of pushouts which we wish to avoid exploring for now.*
 
 \begin{code}
 
+canonical-map-to-cocone
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (X : 𝓣  ̇)
+   (f : C → A) (g : C → B) (s : cocone f g S)
+ → (S → X) → cocone f g X
+canonical-map-to-cocone S X f g (i , j , G) u =
+ (u ∘ i , u ∘ j , ∼-ap-∘ u G)
+
 Pushout-Universal-Property
  : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (X : 𝓣  ̇)
-   (f : C → A) (g : C → B) (i : A → S) (j : B → S) (G : i ∘ f ∼ j ∘ g) 
+   (f : C → A) (g : C → B) (s : cocone f g S) 
  → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓤' ⊔ 𝓣  ̇
-Pushout-Universal-Property S X f g i j G 
- = (S → X) ≃ cocone f g X
+Pushout-Universal-Property S X f g s 
+ = is-equiv (canonical-map-to-cocone S X f g s)
+
+dependent-canonical-map-to-cocone
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S →  𝓣  ̇)
+   (f : C → A) (g : C → B) (s : cocone f g S)
+ → ((x : S) → P x) → dependent-cocone f g S s P
+dependent-canonical-map-to-cocone S P f g (i , j , G) d =
+ (d ∘ i , d ∘ j , λ c → apd d (G c))
+
+Pushout-Dependent-Universal-Property
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S →  𝓣  ̇)
+   (f : C → A) (g : C → B) (s : cocone f g S)
+ → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓤' ⊔ 𝓣  ̇
+Pushout-Dependent-Universal-Property S P f g s =
+ is-equiv (dependent-canonical-map-to-cocone S P f g s)
 
 Pushout-Induction-Principle
  : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
-   (f : C → A) (g : C → B) (i : A → S) (j : B → S) (G : i ∘ f ∼ j ∘ g)
+   (f : C → A) (g : C → B) (s : cocone f g S)
  → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓤' ⊔ 𝓣  ̇
-Pushout-Induction-Principle {_} {_} {_} {_} {_} {A} {B} {C} S P f g i j G 
+Pushout-Induction-Principle {_} {_} {_} {_} {_} {A} {B} {C} S P f g (i , j , G) 
  = (l : (a : A) → P (i a))
  → (r : (b : B) → P (j b))
  → ((c : C) → transport P (G c) (l (f c)) ＝ r (g c))
  → (x : S) → P x
 
-Pushout-Propositional-Computation-Rule₁
+Pushout-Computation-Rule₁
  : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
-   (f : C → A) (g : C → B) (i : A → S) (j : B → S) (G : i ∘ f ∼ j ∘ g)
-   (S-ind : Pushout-Induction-Principle S P f g i j G)
+   (f : C → A) (g : C → B) (s : cocone f g S)
+ → Pushout-Induction-Principle S P f g s
  → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
-Pushout-Propositional-Computation-Rule₁
- {_} {_} {_} {_} {_} {A} {B} {C} S P f g i j G S-ind
+Pushout-Computation-Rule₁
+ {_} {_} {_} {_} {_} {A} {B} {C} S P f g (i , j , G) S-ind
  = (l : (a : A) → P (i a))
  → (r : (b : B) → P (j b))
  → (H : (c : C) → transport P (G c) (l (f c)) ＝ r (g c))
  → (a : A)
  → S-ind l r H (i a) ＝ l a
 
-Pushout-Propositional-Computation-Rule₂
+Pushout-Computation-Rule₂
  : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
-   (f : C → A) (g : C → B) (i : A → S) (j : B → S) (G : i ∘ f ∼ j ∘ g)
-   (S-ind : Pushout-Induction-Principle S P f g i j G)
+   (f : C → A) (g : C → B) (s : cocone f g S)
+ → Pushout-Induction-Principle S P f g s
  → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
-Pushout-Propositional-Computation-Rule₂
- {_} {_} {_} {_} {_} {A} {B} {C} S P f g i j G S-ind
+Pushout-Computation-Rule₂
+ {_} {_} {_} {_} {_} {A} {B} {C} S P f g (i , j , G) S-ind
  = (l : (a : A) → P (i a))
  → (r : (b : B) → P (j b))
  → (H : (c : C) → transport P (G c) (l (f c)) ＝ r (g c))
  → (b : B)
  → S-ind l r H (j b) ＝ r b
 
-Pushout-Propositional-Computation-Rule₃
+Pushout-Computation-Rule₃
  : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
-   (f : C → A) (g : C → B) (i : A → S) (j : B → S) (G : i ∘ f ∼ j ∘ g)
-   (S-ind : Pushout-Induction-Principle S P f g i j G)
-   (S-comp₁ : Pushout-Propositional-Computation-Rule₁ S P f g i j G S-ind)
-   (S-comp₂ : Pushout-Propositional-Computation-Rule₂ S P f g i j G S-ind)
+   (f : C → A) (g : C → B) (s : cocone f g S)
+   (S-ind : Pushout-Induction-Principle S P f g s)
+ → Pushout-Computation-Rule₁ S P f g s S-ind
+ → Pushout-Computation-Rule₂ S P f g s S-ind
  → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
-Pushout-Propositional-Computation-Rule₃
- {_} {_} {_} {_} {_}{A} {B} {C} S P f g i j G S-ind S-comp₁ S-comp₂
+Pushout-Computation-Rule₃
+ {_} {_} {_} {_} {_}{A} {B} {C} S P f g (i , j , G) S-ind S-comp₁ S-comp₂
  = (l : (a : A) → P (i a))
  → (r : (b : B) → P (j b))
  → (H : (c : C) → transport P (G c) (l (f c)) ＝ r (g c))
@@ -191,18 +263,36 @@ Pushout-Propositional-Computation-Rule₃
  → apd (S-ind l r H) (G c) ∙ S-comp₂ l r H (g c)
  ＝ ap (transport P (G c)) (S-comp₁ l r H (f c)) ∙ H c
 
-Pushout-Universal-Property-implies-Induction
+Pushout-Dependent-Universal-Property-implies-Induction
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
+   (f : C → A) (g : C → B) (s : cocone f g S)
+ → Pushout-Dependent-Universal-Property S P f g s
+ → Pushout-Induction-Principle S P f g s
+Pushout-Dependent-Universal-Property-implies-Induction = {!!}
+
+Pushout-Induction-and-Computation-implies-Universal-Property
  : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (X : 𝓣  ̇) (P : S → 𝓣  ̇)
-   (f : C → A) (g : C → B) (i : A → S) (j : B → S) (G : i ∘ f ∼ j ∘ g)
- → Pushout-Universal-Property S X f g i j G
- → Pushout-Induction-Principle S P f g i j G
-Pushout-Universal-Property-implies-Induction = ?
+   (f : C → A) (g : C → B) (s : cocone f g S)
+   (S-ind : Pushout-Induction-Principle S P f g s)
+   (S-comp₁ : Pushout-Computation-Rule₁ S P f g s S-ind)
+   (S-comp₂ : Pushout-Computation-Rule₂ S P f g s S-ind)
+ → Pushout-Computation-Rule₃ S P f g s S-ind S-comp₁ S-comp₂
+ → Pushout-Universal-Property S X f g s
+Pushout-Induction-and-Computation-implies-Universal-Property = {!!}
 
 \end{code}
 
 Now we will use a record type to give the pushout, point and path constructors,
 and the induction principle along with propositional computation rules.
 
+Commenting out the fleshed out induction principle to test the named version
+given above
+
+(l : (a : A) → P (inll a))
+                    → (r : (b : B) → P (inrr b))
+                    → ((c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+                    → (x : pushout) → P x
+
 \begin{code}
 
 record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A) (g : C → B) : 𝓤ω
@@ -212,11 +302,9 @@ record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A)
   inll : A → pushout 
   inrr : B → pushout 
   glue : (c : C) → inll (f c) ＝ inrr (g c)
-  pushout-induction : {P : pushout → 𝓣  ̇}
-                    → (l : (a : A) → P (inll a))
-                    → (r : (b : B) → P (inrr b))
-                    → ((c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-                    → (x : pushout) → P x
+  pushout-induction
+   : {P : pushout → 𝓣  ̇}
+   → Pushout-Induction-Principle pushout P f g (inll , inrr , glue)
   pushout-ind-comp-l
    : {P : pushout → 𝓣  ̇}
    → (l : (a : A) → P (inll a))

From dbc2be4bf3dc6d707e959d2b69d11311bfdabb4d Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Mon, 27 Jan 2025 22:18:33 -0500
Subject: [PATCH 09/18] Updating dependent universal property, etc.

---
 source/UF/Pushouts.lagda | 126 +++++++++++++++++++++------------------
 1 file changed, 68 insertions(+), 58 deletions(-)

diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index a6780feac..09dad97c5 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -184,10 +184,10 @@ the pullback property of pushouts which we wish to avoid exploring for now.*
 \begin{code}
 
 canonical-map-to-cocone
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (X : 𝓣  ̇)
-   (f : C → A) (g : C → B) (s : cocone f g S)
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) 
+   (f : C → A) (g : C → B) (s : cocone f g S) (X : 𝓣  ̇)
  → (S → X) → cocone f g X
-canonical-map-to-cocone S X f g (i , j , G) u =
+canonical-map-to-cocone S f g (i , j , G) X u =
  (u ∘ i , u ∘ j , ∼-ap-∘ u G)
 
 Pushout-Universal-Property
@@ -195,39 +195,39 @@ Pushout-Universal-Property
    (f : C → A) (g : C → B) (s : cocone f g S) 
  → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓤' ⊔ 𝓣  ̇
 Pushout-Universal-Property S X f g s 
- = is-equiv (canonical-map-to-cocone S X f g s)
+ = is-equiv (canonical-map-to-cocone S f g s X)
 
 dependent-canonical-map-to-cocone
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S →  𝓣  ̇)
-   (f : C → A) (g : C → B) (s : cocone f g S)
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇)
+   (f : C → A) (g : C → B) (s : cocone f g S) (P : S →  𝓣  ̇)
  → ((x : S) → P x) → dependent-cocone f g S s P
-dependent-canonical-map-to-cocone S P f g (i , j , G) d =
+dependent-canonical-map-to-cocone S f g (i , j , G) P d =
  (d ∘ i , d ∘ j , λ c → apd d (G c))
 
 Pushout-Dependent-Universal-Property
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S →  𝓣  ̇)
-   (f : C → A) (g : C → B) (s : cocone f g S)
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) 
+   (f : C → A) (g : C → B) (s : cocone f g S) (P : S →  𝓣  ̇)
  → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓤' ⊔ 𝓣  ̇
-Pushout-Dependent-Universal-Property S P f g s =
- is-equiv (dependent-canonical-map-to-cocone S P f g s)
+Pushout-Dependent-Universal-Property S f g s P =
+ is-equiv (dependent-canonical-map-to-cocone S f g s P)
 
 Pushout-Induction-Principle
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
-   (f : C → A) (g : C → B) (s : cocone f g S)
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇)
+   (f : C → A) (g : C → B) (s : cocone f g S) (P : S → 𝓣  ̇)
  → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓤' ⊔ 𝓣  ̇
-Pushout-Induction-Principle {_} {_} {_} {_} {_} {A} {B} {C} S P f g (i , j , G) 
+Pushout-Induction-Principle {_} {_} {_} {_} {_} {A} {B} {C} S f g (i , j , G) P 
  = (l : (a : A) → P (i a))
  → (r : (b : B) → P (j b))
  → ((c : C) → transport P (G c) (l (f c)) ＝ r (g c))
  → (x : S) → P x
 
 Pushout-Computation-Rule₁
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
-   (f : C → A) (g : C → B) (s : cocone f g S)
- → Pushout-Induction-Principle S P f g s
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) 
+   (f : C → A) (g : C → B) (s : cocone f g S) (P : S → 𝓣  ̇)
+ → Pushout-Induction-Principle S f g s P
  → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
 Pushout-Computation-Rule₁
- {_} {_} {_} {_} {_} {A} {B} {C} S P f g (i , j , G) S-ind
+ {_} {_} {_} {_} {_} {A} {B} {C} S f g (i , j , G) P S-ind
  = (l : (a : A) → P (i a))
  → (r : (b : B) → P (j b))
  → (H : (c : C) → transport P (G c) (l (f c)) ＝ r (g c))
@@ -235,12 +235,12 @@ Pushout-Computation-Rule₁
  → S-ind l r H (i a) ＝ l a
 
 Pushout-Computation-Rule₂
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
-   (f : C → A) (g : C → B) (s : cocone f g S)
- → Pushout-Induction-Principle S P f g s
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇)
+   (f : C → A) (g : C → B) (s : cocone f g S) (P : S → 𝓣  ̇)
+ → Pushout-Induction-Principle S f g s P
  → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
 Pushout-Computation-Rule₂
- {_} {_} {_} {_} {_} {A} {B} {C} S P f g (i , j , G) S-ind
+ {_} {_} {_} {_} {_} {A} {B} {C} S f g (i , j , G) P S-ind
  = (l : (a : A) → P (i a))
  → (r : (b : B) → P (j b))
  → (H : (c : C) → transport P (G c) (l (f c)) ＝ r (g c))
@@ -248,14 +248,14 @@ Pushout-Computation-Rule₂
  → S-ind l r H (j b) ＝ r b
 
 Pushout-Computation-Rule₃
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
-   (f : C → A) (g : C → B) (s : cocone f g S)
-   (S-ind : Pushout-Induction-Principle S P f g s)
- → Pushout-Computation-Rule₁ S P f g s S-ind
- → Pushout-Computation-Rule₂ S P f g s S-ind
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) 
+   (f : C → A) (g : C → B) (s : cocone f g S) (P : S → 𝓣  ̇)
+   (S-ind : Pushout-Induction-Principle S f g s P)
+ → Pushout-Computation-Rule₁ S f g s P S-ind
+ → Pushout-Computation-Rule₂ S f g s P S-ind
  → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
 Pushout-Computation-Rule₃
- {_} {_} {_} {_} {_}{A} {B} {C} S P f g (i , j , G) S-ind S-comp₁ S-comp₂
+ {_} {_} {_} {_} {_}{A} {B} {C} S f g (i , j , G) P S-ind S-comp₁ S-comp₂
  = (l : (a : A) → P (i a))
  → (r : (b : B) → P (j b))
  → (H : (c : C) → transport P (G c) (l (f c)) ＝ r (g c))
@@ -264,20 +264,21 @@ Pushout-Computation-Rule₃
  ＝ ap (transport P (G c)) (S-comp₁ l r H (f c)) ∙ H c
 
 Pushout-Dependent-Universal-Property-implies-Induction
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (P : S → 𝓣  ̇)
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) 
    (f : C → A) (g : C → B) (s : cocone f g S)
- → Pushout-Dependent-Universal-Property S P f g s
- → Pushout-Induction-Principle S P f g s
+ → ((P : S → 𝓣  ̇) → Pushout-Dependent-Universal-Property S f g s P)
+ → ((P : S → 𝓣  ̇) → Pushout-Induction-Principle S f g s P)
 Pushout-Dependent-Universal-Property-implies-Induction = {!!}
 
 Pushout-Induction-and-Computation-implies-Universal-Property
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (X : 𝓣  ̇) (P : S → 𝓣  ̇)
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇)
    (f : C → A) (g : C → B) (s : cocone f g S)
-   (S-ind : Pushout-Induction-Principle S P f g s)
-   (S-comp₁ : Pushout-Computation-Rule₁ S P f g s S-ind)
-   (S-comp₂ : Pushout-Computation-Rule₂ S P f g s S-ind)
- → Pushout-Computation-Rule₃ S P f g s S-ind S-comp₁ S-comp₂
- → Pushout-Universal-Property S X f g s
+   (S-ind : (P : S → 𝓣  ̇) → Pushout-Induction-Principle S f g s P)
+   (S-comp₁ : (P : S → 𝓣  ̇) → Pushout-Computation-Rule₁ S f g s P (S-ind P))
+   (S-comp₂ : (P : S → 𝓣  ̇) → Pushout-Computation-Rule₂ S f g s P (S-ind P))
+ → ((P : S → 𝓣  ̇)
+  → Pushout-Computation-Rule₃ S f g s P (S-ind P) (S-comp₁ P) (S-comp₂ P))
+ → ((X : 𝓣  ̇) → Pushout-Universal-Property S X f g s)
 Pushout-Induction-and-Computation-implies-Universal-Property = {!!}
 
 \end{code}
@@ -288,10 +289,29 @@ and the induction principle along with propositional computation rules.
 Commenting out the fleshed out induction principle to test the named version
 given above
 
-(l : (a : A) → P (inll a))
-                    → (r : (b : B) → P (inrr b))
-                    → ((c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-                    → (x : pushout) → P x
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → ((c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → (x : pushout) → P x
+
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → (a : A)
+   → pushout-induction l r G (inll a) ＝ l a 
+
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → (b : B)
+   → pushout-induction l r G (inrr b) ＝ r b
+
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → (c : C)
+   → apd (pushout-induction l r G) (glue c) ∙ pushout-ind-comp-r l r G (g c)
+   ＝ ap (transport P (glue c)) (pushout-ind-comp-l l r G (f c)) ∙ G c
 
 \begin{code}
 
@@ -304,29 +324,19 @@ record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A)
   glue : (c : C) → inll (f c) ＝ inrr (g c)
   pushout-induction
    : {P : pushout → 𝓣  ̇}
-   → Pushout-Induction-Principle pushout P f g (inll , inrr , glue)
+   → Pushout-Induction-Principle pushout f g (inll , inrr , glue) P
   pushout-ind-comp-l
    : {P : pushout → 𝓣  ̇}
-   → (l : (a : A) → P (inll a))
-   → (r : (b : B) → P (inrr b))
-   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-   → (a : A)
-   → pushout-induction l r G (inll a) ＝ l a 
+   → Pushout-Computation-Rule₁ pushout f g (inll , inrr , glue) P
+      pushout-induction
   pushout-ind-comp-r
    : {P : pushout → 𝓣  ̇}
-   → (l : (a : A) → P (inll a))
-   → (r : (b : B) → P (inrr b))
-   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-   → (b : B)
-   → pushout-induction l r G (inrr b) ＝ r b
+   → Pushout-Computation-Rule₂ pushout f g (inll , inrr , glue) P
+      pushout-induction
   pushout-ind-comp-G
    : {P : pushout → 𝓣  ̇}
-   → (l : (a : A) → P (inll a))
-   → (r : (b : B) → P (inrr b))
-   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-   → (c : C)
-   → apd (pushout-induction l r G) (glue c) ∙ pushout-ind-comp-r l r G (g c)
-   ＝ ap (transport P (glue c)) (pushout-ind-comp-l l r G (f c)) ∙ G c
+   → Pushout-Computation-Rule₃ pushout f g (inll , inrr , glue) P
+      pushout-induction pushout-ind-comp-l pushout-ind-comp-r
 
 \end{code}
 

From 9281a21551761d6a3b4c2f280148ec43536ceec9 Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Tue, 28 Jan 2025 12:17:19 -0500
Subject: [PATCH 10/18] Updating statement of universal property

---
 source/UF/Pushouts.lagda | 96 +++++++++++++++++++++++-----------------
 1 file changed, 56 insertions(+), 40 deletions(-)

diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index 09dad97c5..2c5def3aa 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -17,6 +17,7 @@ open import UF.Base
 open import UF.Equiv
 open import UF.EquivalenceExamples
 open import UF.PropIndexedPiSigma
+open import UF.Retracts
 open import UF.Subsingletons
 open import UF.Yoneda
 
@@ -181,6 +182,9 @@ We will not show
 (3) Is shown in the Agda Unimath library (*link*). It involves something called
 the pullback property of pushouts which we wish to avoid exploring for now.*
 
+In general, we know that the universal property of (higher) inductive types is
+equivalent to the induction principle with propositional computation rules.
+
 \begin{code}
 
 canonical-map-to-cocone
@@ -191,17 +195,17 @@ canonical-map-to-cocone S f g (i , j , G) X u =
  (u ∘ i , u ∘ j , ∼-ap-∘ u G)
 
 Pushout-Universal-Property
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) (X : 𝓣  ̇)
-   (f : C → A) (g : C → B) (s : cocone f g S) 
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) 
+   (f : C → A) (g : C → B) (s : cocone f g S) (X : 𝓣  ̇)
  → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓤' ⊔ 𝓣  ̇
-Pushout-Universal-Property S X f g s 
+Pushout-Universal-Property S f g s X
  = is-equiv (canonical-map-to-cocone S f g s X)
 
-dependent-canonical-map-to-cocone
+canonical-map-to-dependent-cocone
  : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇)
    (f : C → A) (g : C → B) (s : cocone f g S) (P : S →  𝓣  ̇)
  → ((x : S) → P x) → dependent-cocone f g S s P
-dependent-canonical-map-to-cocone S f g (i , j , G) P d =
+canonical-map-to-dependent-cocone S f g (i , j , G) P d =
  (d ∘ i , d ∘ j , λ c → apd d (G c))
 
 Pushout-Dependent-Universal-Property
@@ -209,7 +213,7 @@ Pushout-Dependent-Universal-Property
    (f : C → A) (g : C → B) (s : cocone f g S) (P : S →  𝓣  ̇)
  → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓤' ⊔ 𝓣  ̇
 Pushout-Dependent-Universal-Property S f g s P =
- is-equiv (dependent-canonical-map-to-cocone S f g s P)
+ is-equiv (canonical-map-to-dependent-cocone S f g s P)
 
 Pushout-Induction-Principle
  : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇)
@@ -268,7 +272,45 @@ Pushout-Dependent-Universal-Property-implies-Induction
    (f : C → A) (g : C → B) (s : cocone f g S)
  → ((P : S → 𝓣  ̇) → Pushout-Dependent-Universal-Property S f g s P)
  → ((P : S → 𝓣  ̇) → Pushout-Induction-Principle S f g s P)
-Pushout-Dependent-Universal-Property-implies-Induction = {!!}
+Pushout-Dependent-Universal-Property-implies-Induction
+ S f g s dep-UP P l r G = inv (l , r , G)
+ where
+  inv : dependent-cocone f g S s P
+      → ((x : S) → P x)
+  inv = ⌜ (canonical-map-to-dependent-cocone S f g s P , dep-UP P) ⌝⁻¹
+
+Pushout-Dependent-Universal-Property-implies-Computation-Rule₁
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) 
+   (f : C → A) (g : C → B) (s : cocone f g S)
+ → (S-UP : (P : S → 𝓣  ̇) → Pushout-Dependent-Universal-Property S f g s P)
+ → (P : S → 𝓣  ̇) → Pushout-Computation-Rule₁ S f g s P
+    (Pushout-Dependent-Universal-Property-implies-Induction S f g s S-UP P)
+Pushout-Dependent-Universal-Property-implies-Computation-Rule₁
+ S f g (i , j , G) S-UP P l r H a = {!!}
+ where
+  H' : is-equiv (canonical-map-to-dependent-cocone S f g (i , j , G) P)
+     → is-section (canonical-map-to-dependent-cocone S f g (i , j , G) P)
+  H' =
+   equivs-are-sections (canonical-map-to-dependent-cocone S f g (i , j , G) P)
+  H'-eq : retraction-of
+           (canonical-map-to-dependent-cocone S f g (i , j , G) P)
+            (pr₂ (S-UP P))
+             ∘ canonical-map-to-dependent-cocone S f g (i , j , G) P
+        ∼ id
+  H'-eq =
+   retraction-equation (canonical-map-to-dependent-cocone S f g (i , j , G) P)
+                       (H' (S-UP P))
+  H'' : is-equiv (canonical-map-to-dependent-cocone S f g (i , j , G) P)
+      → has-section (canonical-map-to-dependent-cocone S f g (i , j , G) P)
+  H'' =
+   equivs-have-sections (canonical-map-to-dependent-cocone S f g (i , j , G) P)
+  H''-eq : canonical-map-to-dependent-cocone S f g (i , j , G) P ∘
+            section-of (canonical-map-to-dependent-cocone S f g (i , j , G) P)
+             (pr₁ (S-UP (λ v → P v)))
+         ∼ id
+  H''-eq =
+   section-equation (canonical-map-to-dependent-cocone S f g (i , j , G) P)
+                    (H'' (S-UP P))
 
 Pushout-Induction-and-Computation-implies-Universal-Property
  : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇)
@@ -278,7 +320,7 @@ Pushout-Induction-and-Computation-implies-Universal-Property
    (S-comp₂ : (P : S → 𝓣  ̇) → Pushout-Computation-Rule₂ S f g s P (S-ind P))
  → ((P : S → 𝓣  ̇)
   → Pushout-Computation-Rule₃ S f g s P (S-ind P) (S-comp₁ P) (S-comp₂ P))
- → ((X : 𝓣  ̇) → Pushout-Universal-Property S X f g s)
+ → ((X : 𝓣  ̇) → Pushout-Universal-Property S f g s X)
 Pushout-Induction-and-Computation-implies-Universal-Property = {!!}
 
 \end{code}
@@ -286,33 +328,6 @@ Pushout-Induction-and-Computation-implies-Universal-Property = {!!}
 Now we will use a record type to give the pushout, point and path constructors,
 and the induction principle along with propositional computation rules.
 
-Commenting out the fleshed out induction principle to test the named version
-given above
-
-   → (l : (a : A) → P (inll a))
-   → (r : (b : B) → P (inrr b))
-   → ((c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-   → (x : pushout) → P x
-
-   → (l : (a : A) → P (inll a))
-   → (r : (b : B) → P (inrr b))
-   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-   → (a : A)
-   → pushout-induction l r G (inll a) ＝ l a 
-
-   → (l : (a : A) → P (inll a))
-   → (r : (b : B) → P (inrr b))
-   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-   → (b : B)
-   → pushout-induction l r G (inrr b) ＝ r b
-
-   → (l : (a : A) → P (inll a))
-   → (r : (b : B) → P (inrr b))
-   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-   → (c : C)
-   → apd (pushout-induction l r G) (glue c) ∙ pushout-ind-comp-r l r G (g c)
-   ＝ ap (transport P (glue c)) (pushout-ind-comp-l l r G (f c)) ∙ G c
-
 \begin{code}
 
 record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A) (g : C → B) : 𝓤ω
@@ -435,7 +450,7 @@ universal property.
                     → (H : (a : A) → s (inll a) ＝ s' (inll a))
                     → (H' : (b : B) → s (inrr b) ＝ s' (inrr b))
                     → (G : (c : C)
-                         → ap s (glue c) ∙ H' (g c) ＝ H (f c) ∙ ap s' (glue c))
+                      → ap s (glue c) ∙ H' (g c) ＝ H (f c) ∙ ap s' (glue c))
                     → (x : pushout) → s x ＝ s' x
  pushout-uniqueness X s s' H H' G =
   pushout-induction H H' I
@@ -455,12 +470,13 @@ universal property.
        IV = ∙assoc (ap s (glue c) ⁻¹) (H (f c)) (ap s' (glue c))
        V = ap-left-inverse (ap s (glue c)) (G c ⁻¹)
    
- pushout-universal-property : (X : 𝓣 ̇)
-                            → (pushout → X) ≃ cocone f g X
- pushout-universal-property X = qinveq ϕ (ψ , ψ-ϕ , ϕ-ψ)
+ pushout-universal-property
+  : (X : 𝓣 ̇)
+  → Pushout-Universal-Property pushout f g (inll , inrr , glue) X
+ pushout-universal-property X = ((ψ , ϕ-ψ) , (ψ , ψ-ϕ))
   where
    ϕ : (pushout → X) → cocone f g X
-   ϕ u = (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue)
+   ϕ u = canonical-map-to-cocone pushout f g (inll , inrr , glue) X u
    ψ : cocone f g X → (pushout → X)
    ψ (l , r , G) = pushout-recursion l r G
    ψ-ϕ : ψ ∘ ϕ ∼ id

From 2d39acda6b6fadd04ada41db0e7d5644a20ead82 Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Tue, 28 Jan 2025 18:10:41 -0500
Subject: [PATCH 11/18] Dependent universal property in record type

---
 source/UF/Pushouts.lagda | 233 ++++++++++++++++++---------------------
 1 file changed, 110 insertions(+), 123 deletions(-)

diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index 2c5def3aa..47ac4d46e 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -267,66 +267,10 @@ Pushout-Computation-Rule₃
  → apd (S-ind l r H) (G c) ∙ S-comp₂ l r H (g c)
  ＝ ap (transport P (G c)) (S-comp₁ l r H (f c)) ∙ H c
 
-Pushout-Dependent-Universal-Property-implies-Induction
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) 
-   (f : C → A) (g : C → B) (s : cocone f g S)
- → ((P : S → 𝓣  ̇) → Pushout-Dependent-Universal-Property S f g s P)
- → ((P : S → 𝓣  ̇) → Pushout-Induction-Principle S f g s P)
-Pushout-Dependent-Universal-Property-implies-Induction
- S f g s dep-UP P l r G = inv (l , r , G)
- where
-  inv : dependent-cocone f g S s P
-      → ((x : S) → P x)
-  inv = ⌜ (canonical-map-to-dependent-cocone S f g s P , dep-UP P) ⌝⁻¹
-
-Pushout-Dependent-Universal-Property-implies-Computation-Rule₁
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇) 
-   (f : C → A) (g : C → B) (s : cocone f g S)
- → (S-UP : (P : S → 𝓣  ̇) → Pushout-Dependent-Universal-Property S f g s P)
- → (P : S → 𝓣  ̇) → Pushout-Computation-Rule₁ S f g s P
-    (Pushout-Dependent-Universal-Property-implies-Induction S f g s S-UP P)
-Pushout-Dependent-Universal-Property-implies-Computation-Rule₁
- S f g (i , j , G) S-UP P l r H a = {!!}
- where
-  H' : is-equiv (canonical-map-to-dependent-cocone S f g (i , j , G) P)
-     → is-section (canonical-map-to-dependent-cocone S f g (i , j , G) P)
-  H' =
-   equivs-are-sections (canonical-map-to-dependent-cocone S f g (i , j , G) P)
-  H'-eq : retraction-of
-           (canonical-map-to-dependent-cocone S f g (i , j , G) P)
-            (pr₂ (S-UP P))
-             ∘ canonical-map-to-dependent-cocone S f g (i , j , G) P
-        ∼ id
-  H'-eq =
-   retraction-equation (canonical-map-to-dependent-cocone S f g (i , j , G) P)
-                       (H' (S-UP P))
-  H'' : is-equiv (canonical-map-to-dependent-cocone S f g (i , j , G) P)
-      → has-section (canonical-map-to-dependent-cocone S f g (i , j , G) P)
-  H'' =
-   equivs-have-sections (canonical-map-to-dependent-cocone S f g (i , j , G) P)
-  H''-eq : canonical-map-to-dependent-cocone S f g (i , j , G) P ∘
-            section-of (canonical-map-to-dependent-cocone S f g (i , j , G) P)
-             (pr₁ (S-UP (λ v → P v)))
-         ∼ id
-  H''-eq =
-   section-equation (canonical-map-to-dependent-cocone S f g (i , j , G) P)
-                    (H'' (S-UP P))
-
-Pushout-Induction-and-Computation-implies-Universal-Property
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (S : 𝓤'  ̇)
-   (f : C → A) (g : C → B) (s : cocone f g S)
-   (S-ind : (P : S → 𝓣  ̇) → Pushout-Induction-Principle S f g s P)
-   (S-comp₁ : (P : S → 𝓣  ̇) → Pushout-Computation-Rule₁ S f g s P (S-ind P))
-   (S-comp₂ : (P : S → 𝓣  ̇) → Pushout-Computation-Rule₂ S f g s P (S-ind P))
- → ((P : S → 𝓣  ̇)
-  → Pushout-Computation-Rule₃ S f g s P (S-ind P) (S-comp₁ P) (S-comp₂ P))
- → ((X : 𝓣  ̇) → Pushout-Universal-Property S f g s X)
-Pushout-Induction-and-Computation-implies-Universal-Property = {!!}
-
 \end{code}
 
 Now we will use a record type to give the pushout, point and path constructors,
-and the induction principle along with propositional computation rules.
+and the dependent universal property.
 
 \begin{code}
 
@@ -337,33 +281,76 @@ record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A)
   inll : A → pushout 
   inrr : B → pushout 
   glue : (c : C) → inll (f c) ＝ inrr (g c)
-  pushout-induction
+  pushout-dependent-universal-property
    : {P : pushout → 𝓣  ̇}
-   → Pushout-Induction-Principle pushout f g (inll , inrr , glue) P
-  pushout-ind-comp-l
-   : {P : pushout → 𝓣  ̇}
-   → Pushout-Computation-Rule₁ pushout f g (inll , inrr , glue) P
-      pushout-induction
-  pushout-ind-comp-r
-   : {P : pushout → 𝓣  ̇}
-   → Pushout-Computation-Rule₂ pushout f g (inll , inrr , glue) P
-      pushout-induction
-  pushout-ind-comp-G
-   : {P : pushout → 𝓣  ̇}
-   → Pushout-Computation-Rule₃ pushout f g (inll , inrr , glue) P
-      pushout-induction pushout-ind-comp-l pushout-ind-comp-r
+   → Pushout-Dependent-Universal-Property pushout f g (inll , inrr , glue) P
 
 \end{code}
 
-We will now observe that the pushout is a cocone and begin deriving some key
-results from the induction principle:
-recursion (along with corresponding computation rules), uniqueness and the
-universal property.
+We will observe that the pushout is a cocone and begin deriving some key
+results from the dependent universal property:
+induction and recursion principles (along with corresponding computation rules), the uniqueness principle and the non-dependent universal property.
+
+TODO. Show that the non-dependent universal property implies the dependent
+universal property. This will establish the logical equivalence between
+
+1) The dependent universal property
+2) The induction principle with propositional computation rules
+3) The recursion principle with propositional computation rules and the
+   uniqueness principle
+4) The non-dependent universal property.
 
 \begin{code}
 
  pushout-cocone : cocone f g pushout
  pushout-cocone = (inll , inrr , glue)
+
+ pushout-dep-UP-inverse : {P : pushout → 𝓣  ̇}
+                        → dependent-cocone f g pushout (inll , inrr , glue) P
+                        → ((x : pushout) → P x)
+ pushout-dep-UP-inverse {_} {P}
+  = inverse (canonical-map-to-dependent-cocone pushout f g (inll , inrr , glue) P)
+     pushout-dependent-universal-property
+
+ pushout-dep-UP-section
+  : {P : pushout → 𝓣  ̇}
+  → pushout-dep-UP-inverse
+   ∘ canonical-map-to-dependent-cocone pushout f g (inll , inrr , glue) P
+  ∼ id
+ pushout-dep-UP-section {_} {P}
+  = {!!}
+
+ pushout-dep-UP-retraction
+  : {P : pushout → 𝓣  ̇}
+  → canonical-map-to-dependent-cocone pushout f g (inll , inrr , glue) P
+     ∘ pushout-dep-UP-inverse
+  ∼ id
+ pushout-dep-UP-retraction {_} {P}
+  = retraction-equation pushout-dep-UP-inverse
+     (equivs-are-sections pushout-dep-UP-inverse {!!})
+
+ pushout-induction
+  : {P : pushout → 𝓣  ̇}
+  → Pushout-Induction-Principle pushout f g (inll , inrr , glue) P
+ pushout-induction {_} {P} l r G = pushout-dep-UP-inverse (l , r , G)
+
+ pushout-ind-comp-inll
+  : {P : pushout → 𝓣  ̇}
+  → Pushout-Computation-Rule₁ pushout f g (inll , inrr , glue) P
+     pushout-induction
+ pushout-ind-comp-inll l r H a = {!!}
+  
+ pushout-ind-comp-inrr
+  : {P : pushout → 𝓣  ̇}
+  → Pushout-Computation-Rule₂ pushout f g (inll , inrr , glue) P
+     pushout-induction
+ pushout-ind-comp-inrr l r H b = {!!}
+  
+ pushout-ind-comp-glue
+  : {P : pushout → 𝓣  ̇}
+  → Pushout-Computation-Rule₃ pushout f g (inll , inrr , glue) P
+     pushout-induction pushout-ind-comp-inll pushout-ind-comp-inrr
+ pushout-ind-comp-glue l r H c = {!!}
    
  pushout-recursion : {D : 𝓣  ̇}
                    → (l : A → D)
@@ -373,75 +360,76 @@ universal property.
  pushout-recursion l r G =
   pushout-induction l r (λ c → (transport-const (glue c) ∙ G c))
 
- pushout-rec-comp-l : {D : 𝓣  ̇}
-                    → (l : A → D)
-                    → (r : B → D)
-                    → (G : (c : C) → l (f c) ＝ r (g c))
-                    → (a : A)
-                    → pushout-recursion l r G (inll a) ＝ l a
- pushout-rec-comp-l l r G =
-  pushout-ind-comp-l l r (λ c → (transport-const (glue c) ∙ G c))
-
- pushout-rec-comp-r : {D : 𝓣  ̇}
-                    → (l : A → D)
-                    → (r : B → D)
-                    → (G : (c : C) → l (f c) ＝ r (g c))
-                    → (b : B)
-                    → pushout-recursion l r G (inrr b) ＝ r b
- pushout-rec-comp-r l r G =
-  pushout-ind-comp-r l r (λ c → (transport-const (glue c) ∙ G c))
-
- pushout-rec-comp-G
+ pushout-rec-comp-inll : {D : 𝓣  ̇}
+                       → (l : A → D)
+                       → (r : B → D)
+                       → (G : (c : C) → l (f c) ＝ r (g c))
+                       → (a : A)
+                       → pushout-recursion l r G (inll a) ＝ l a
+ pushout-rec-comp-inll l r G =
+  pushout-ind-comp-inll l r (λ c → (transport-const (glue c) ∙ G c))
+
+ pushout-rec-comp-inrr : {D : 𝓣  ̇}
+                       → (l : A → D)
+                       → (r : B → D)
+                       → (G : (c : C) → l (f c) ＝ r (g c))
+                       → (b : B)
+                       → pushout-recursion l r G (inrr b) ＝ r b
+ pushout-rec-comp-inrr l r G =
+  pushout-ind-comp-inrr l r (λ c → (transport-const (glue c) ∙ G c))
+
+ pushout-rec-comp-glue
   : {D : 𝓣  ̇}
   → (l : A → D)
   → (r : B → D)
   → (G : (c : C) → l (f c) ＝ r (g c))
   → (c : C)
-  → ap (pushout-recursion l r G) (glue c) ∙ pushout-rec-comp-r l r G (g c) 
-  ＝ pushout-rec-comp-l l r G (f c) ∙ G c
- pushout-rec-comp-G {𝓣} {D} l r G c =
-  ap (pushout-recursion l r G) (glue c) ∙ pushout-rec-comp-r l r G (g c)                                                                    ＝⟨ III ⟩
+  → ap (pushout-recursion l r G) (glue c) ∙ pushout-rec-comp-inrr l r G (g c) 
+  ＝ pushout-rec-comp-inll l r G (f c) ∙ G c
+ pushout-rec-comp-glue {𝓣} {D} l r G c =
+  ap (pushout-recursion l r G) (glue c) ∙ pushout-rec-comp-inrr l r G (g c)                                                                 ＝⟨ III ⟩
   transport-const (glue c) ⁻¹ ∙ apd (pushout-recursion l r G) (glue c)
-   ∙ pushout-rec-comp-r l r G (g c)                         ＝⟨ V ⟩
+   ∙ pushout-rec-comp-inrr l r G (g c)                      ＝⟨ V ⟩
   transport-const (glue c) ⁻¹
-    ∙ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-l l r G (f c))
+    ∙ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-inll l r G (f c))
     ∙ (transport-const (glue c) ∙ G c)                      ＝⟨ VI ⟩
   transport-const (glue c) ⁻¹
-    ∙ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-l l r G (f c))
+    ∙ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-inll l r G (f c))
     ∙ transport-const (glue c) ∙ G c                        ＝⟨ IX ⟩
-  pushout-rec-comp-l l r G (f c) ∙ G c                      ∎
+  pushout-rec-comp-inll l r G (f c) ∙ G c                      ∎
   where
    II : ap (pushout-recursion l r G) (glue c)
       ＝ transport-const (glue c) ⁻¹
          ∙ apd (pushout-induction l r (λ - → (transport-const (glue -) ∙ G -)))
                (glue c)
    II = apd-from-ap (pushout-recursion l r G) (glue c)
-   III = ap (_∙ pushout-rec-comp-r l r G (g c)) II 
-   IV : apd (pushout-recursion l r G) (glue c) ∙ pushout-rec-comp-r l r G (g c)
-      ＝ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-l l r G (f c))
+   III = ap (_∙ pushout-rec-comp-inrr l r G (g c)) II 
+   IV : apd (pushout-recursion l r G) (glue c)
+       ∙ pushout-rec-comp-inrr l r G (g c)
+      ＝ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-inll l r G (f c))
        ∙ (transport-const (glue c) ∙ G c)
-   IV = pushout-ind-comp-G l r (λ - → (transport-const (glue -) ∙ G -)) c
+   IV = pushout-ind-comp-glue l r (λ - → (transport-const (glue -) ∙ G -)) c
    V : transport-const (glue c) ⁻¹ ∙ apd (pushout-recursion l r G) (glue c)
-        ∙ pushout-rec-comp-r l r G (g c)
+        ∙ pushout-rec-comp-inrr l r G (g c)
      ＝ transport-const (glue c) ⁻¹
-        ∙ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-l l r G (f c))
+        ∙ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-inll l r G (f c))
         ∙ (transport-const (glue c) ∙ G c)
    V = ap-on-left-is-assoc (transport-const (glue c) ⁻¹) IV
    VI = ∙assoc (transport-const (glue c) ⁻¹ ∙ ap (transport (λ - → D) (glue c))
-               (pushout-rec-comp-l l r G (f c))) (transport-const (glue c))
+               (pushout-rec-comp-inll l r G (f c))) (transport-const (glue c))
                (G c) ⁻¹
-   VII : ap (transport (λ - → D) (glue c)) (pushout-rec-comp-l l r G (f c))
+   VII : ap (transport (λ - → D) (glue c)) (pushout-rec-comp-inll l r G (f c))
          ∙ transport-const (glue c)
-       ＝ transport-const (glue c) ∙ pushout-rec-comp-l l r G (f c)
+       ＝ transport-const (glue c) ∙ pushout-rec-comp-inll l r G (f c)
    VII = homotopies-are-natural (transport (λ - → D) (glue c)) id
           (λ - → transport-const (glue c)) ⁻¹
    VIII : transport-const (glue c) ⁻¹
-        ∙ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-l l r G (f c))
+        ∙ ap (transport (λ - → D) (glue c)) (pushout-rec-comp-inll l r G (f c))
         ∙ transport-const (glue c)
-     ＝ pushout-rec-comp-l l r G (f c)
+     ＝ pushout-rec-comp-inll l r G (f c)
    VIII = ∙assoc (transport-const (glue c) ⁻¹)
                  (ap (transport (λ - → D) (glue c))
-                 (pushout-rec-comp-l l r G (f c))) (transport-const (glue c))
+                 (pushout-rec-comp-inll l r G (f c))) (transport-const (glue c))
           ∙ ap-left-inverse (transport-const (glue c)) VII 
    IX = ap (_∙ G c) VIII
 
@@ -462,10 +450,9 @@ universal property.
          H' (g c)                                         ∎
     where
      II = transport-after-ap' (glue c) s s' (H (f c))
-     III =
-      ap s (glue c) ⁻¹ ∙ H (f c) ∙ ap s' (glue c)   ＝⟨ IV ⟩
-      ap s (glue c) ⁻¹ ∙ (H (f c) ∙ ap s' (glue c)) ＝⟨ V ⟩
-      H' (g c)                                       ∎
+     III = ap s (glue c) ⁻¹ ∙ H (f c) ∙ ap s' (glue c)   ＝⟨ IV ⟩
+           ap s (glue c) ⁻¹ ∙ (H (f c) ∙ ap s' (glue c)) ＝⟨ V ⟩
+           H' (g c)                                       ∎
       where
        IV = ∙assoc (ap s (glue c) ⁻¹) (H (f c)) (ap s' (glue c))
        V = ap-left-inverse (ap s (glue c)) (G c ⁻¹)
@@ -481,13 +468,13 @@ universal property.
    ψ (l , r , G) = pushout-recursion l r G
    ψ-ϕ : ψ ∘ ϕ ∼ id
    ψ-ϕ u = dfunext fe (pushout-uniqueness X ((ψ ∘ ϕ) u) u
-                   (pushout-rec-comp-l (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
-                   (pushout-rec-comp-r (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
-                   (pushout-rec-comp-G (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue)))
+                   (pushout-rec-comp-inll (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
+                   (pushout-rec-comp-inrr (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
+                   (pushout-rec-comp-glue (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue)))
    ϕ-ψ : ϕ ∘ ψ ∼ id
    ϕ-ψ (l , r , G) =
     inverse-cocone-map f g X ((ϕ ∘ ψ) (l , r , G)) (l , r , G)
-     (pushout-rec-comp-l l r G , pushout-rec-comp-r l r G ,
-      ∼-sym (pushout-rec-comp-G l r G))
+     (pushout-rec-comp-inll l r G , pushout-rec-comp-inrr l r G ,
+      ∼-sym (pushout-rec-comp-glue l r G))
    
 \end{code}

From af9c2fb84f5e46845c878c177f9e628d980cfae2 Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Wed, 29 Jan 2025 12:31:25 -0500
Subject: [PATCH 12/18] Deriving induction and computation rules; first steps

---
 source/UF/Pushouts.lagda | 40 +++++++++++++++++++++++-----------------
 1 file changed, 23 insertions(+), 17 deletions(-)

diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index 47ac4d46e..4fd233cf0 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -150,6 +150,8 @@ inverse-cocone-map f g X u u' =
 
 We also introduce the notion of a dependent cocone.
 
+TODO. Characterize the identity type of dependent cocones.
+
 \begin{code}
 
 dependent-cocone : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
@@ -171,19 +173,22 @@ propositional computation rules for pushouts and show they are inter-derivable*.
   propositional computation rules.
 
 (2)
-  The induction principle and propositional computationrules implies the
-  (non-dependeny) universal property.
+  The induction principle and propositional computation rules implies the
+  the recursion principle with corresponding computation rules and the uniqueness
+  principle.
 
-We will not show
 (3)
+  The recursion principle with corresponding computation rules and the uniqueness
+  principle implies the non-dependent universal property.
+
+(4)
   The (non-dependent) universal property implies the dependent universal
   property.
 
-(3) Is shown in the Agda Unimath library (*link*). It involves something called
-the pullback property of pushouts which we wish to avoid exploring for now.*
-
-In general, we know that the universal property of (higher) inductive types is
-equivalent to the induction principle with propositional computation rules.
+(4) Is shown in the Agda Unimath library (*link*). It involves something called
+the pullback property of pushouts which we wish to avoid exploring for now.
+Alternativly, we can show the converse of (3), (2) and (1) which would provide a
+proof of (4).*
 
 \begin{code}
 
@@ -318,7 +323,9 @@ universal property. This will establish the logical equivalence between
    ∘ canonical-map-to-dependent-cocone pushout f g (inll , inrr , glue) P
   ∼ id
  pushout-dep-UP-section {_} {P}
-  = {!!}
+  = inverses-are-retractions
+     (canonical-map-to-dependent-cocone pushout f g (inll , inrr , glue) P)
+      pushout-dependent-universal-property
 
  pushout-dep-UP-retraction
   : {P : pushout → 𝓣  ̇}
@@ -326,24 +333,23 @@ universal property. This will establish the logical equivalence between
      ∘ pushout-dep-UP-inverse
   ∼ id
  pushout-dep-UP-retraction {_} {P}
-  = retraction-equation pushout-dep-UP-inverse
-     (equivs-are-sections pushout-dep-UP-inverse {!!})
+  = inverses-are-sections
+     (canonical-map-to-dependent-cocone pushout f g (inll , inrr , glue) P)
+      pushout-dependent-universal-property
 
  pushout-induction
   : {P : pushout → 𝓣  ̇}
   → Pushout-Induction-Principle pushout f g (inll , inrr , glue) P
- pushout-induction {_} {P} l r G = pushout-dep-UP-inverse (l , r , G)
+ pushout-induction {_} {P} l r H = pushout-dep-UP-inverse (l , r , H)
 
  pushout-ind-comp-inll
   : {P : pushout → 𝓣  ̇}
-  → Pushout-Computation-Rule₁ pushout f g (inll , inrr , glue) P
-     pushout-induction
- pushout-ind-comp-inll l r H a = {!!}
+  → Pushout-Computation-Rule₁ pushout f g (inll , inrr , glue) P pushout-induction
+ pushout-ind-comp-inll {_} {P} l r H a = {!!}
   
  pushout-ind-comp-inrr
   : {P : pushout → 𝓣  ̇}
-  → Pushout-Computation-Rule₂ pushout f g (inll , inrr , glue) P
-     pushout-induction
+  → Pushout-Computation-Rule₂ pushout f g (inll , inrr , glue) P pushout-induction
  pushout-ind-comp-inrr l r H b = {!!}
   
  pushout-ind-comp-glue

From 16acc8e8d803b6e0880f6b41c3a1e77c39e08d30 Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Fri, 31 Jan 2025 12:26:59 -0500
Subject: [PATCH 13/18] Deriving everything from universal property

---
 source/UF/Pushouts.lagda | 267 +++++++++++++++++++++++++++------------
 1 file changed, 189 insertions(+), 78 deletions(-)

diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index 4fd233cf0..927af493b 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -164,31 +164,18 @@ dependent-cocone {_} {_} {_} {_} {_} {A} {B} {C} f g X (i , j , H) P =
 
 \end{code}
 
-Now we will define the (dependent) universal property, induction principle and
-propositional computation rules for pushouts and show they are inter-derivable*.
+Now we will define the universal property, induction principle and propositional
+computation rules for pushouts and show they are inter-derivable.
 
-*In fact we will only show:
-(1)
-  The dependent universal propery implies the induction principle and
-  propositional computation rules.
-
-(2)
-  The induction principle and propositional computation rules implies the
+In fact we will only show:
+(1) The induction principle and propositional computation rules implies the
   the recursion principle with corresponding computation rules and the uniqueness
   principle.
 
-(3)
-  The recursion principle with corresponding computation rules and the uniqueness
-  principle implies the non-dependent universal property.
-
-(4)
-  The (non-dependent) universal property implies the dependent universal
-  property.
+(2) The recursion principle with corresponding computation rules and the
+  uniqueness principle implies the non-dependent universal property.
 
-(4) Is shown in the Agda Unimath library (*link*). It involves something called
-the pullback property of pushouts which we wish to avoid exploring for now.
-Alternativly, we can show the converse of (3), (2) and (1) which would provide a
-proof of (4).*
+(3) The universal property implies the induction principle.
 
 \begin{code}
 
@@ -286,77 +273,40 @@ record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A)
   inll : A → pushout 
   inrr : B → pushout 
   glue : (c : C) → inll (f c) ＝ inrr (g c)
-  pushout-dependent-universal-property
+  pushout-induction
+   : {P : pushout → 𝓣  ̇}
+   → Pushout-Induction-Principle pushout f g (inll , inrr , glue) P
+  pushout-ind-comp-inll
    : {P : pushout → 𝓣  ̇}
-   → Pushout-Dependent-Universal-Property pushout f g (inll , inrr , glue) P
+   → Pushout-Computation-Rule₁ pushout f g (inll , inrr , glue) P
+      pushout-induction
+  pushout-ind-comp-inrr
+   : {P : pushout → 𝓣  ̇}
+   → Pushout-Computation-Rule₂ pushout f g (inll , inrr , glue) P
+      pushout-induction
+  pushout-ind-comp-glue
+   : {P : pushout → 𝓣  ̇}
+   → Pushout-Computation-Rule₃ pushout f g (inll , inrr , glue) P
+      pushout-induction pushout-ind-comp-inll pushout-ind-comp-inrr
 
 \end{code}
 
 We will observe that the pushout is a cocone and begin deriving some key
-results from the dependent universal property:
-induction and recursion principles (along with corresponding computation rules), the uniqueness principle and the non-dependent universal property.
+results from the induction principles:
+recursion principle (along with corresponding computation rules), the uniqueness
+principle and the universal property.
 
-TODO. Show that the non-dependent universal property implies the dependent
-universal property. This will establish the logical equivalence between
+The following are logically equivalent
 
-1) The dependent universal property
-2) The induction principle with propositional computation rules
-3) The recursion principle with propositional computation rules and the
+1) The induction principle with propositional computation rules
+2) The recursion principle with propositional computation rules and the
    uniqueness principle
-4) The non-dependent universal property.
+3) The universal property.
 
 \begin{code}
 
  pushout-cocone : cocone f g pushout
  pushout-cocone = (inll , inrr , glue)
-
- pushout-dep-UP-inverse : {P : pushout → 𝓣  ̇}
-                        → dependent-cocone f g pushout (inll , inrr , glue) P
-                        → ((x : pushout) → P x)
- pushout-dep-UP-inverse {_} {P}
-  = inverse (canonical-map-to-dependent-cocone pushout f g (inll , inrr , glue) P)
-     pushout-dependent-universal-property
-
- pushout-dep-UP-section
-  : {P : pushout → 𝓣  ̇}
-  → pushout-dep-UP-inverse
-   ∘ canonical-map-to-dependent-cocone pushout f g (inll , inrr , glue) P
-  ∼ id
- pushout-dep-UP-section {_} {P}
-  = inverses-are-retractions
-     (canonical-map-to-dependent-cocone pushout f g (inll , inrr , glue) P)
-      pushout-dependent-universal-property
-
- pushout-dep-UP-retraction
-  : {P : pushout → 𝓣  ̇}
-  → canonical-map-to-dependent-cocone pushout f g (inll , inrr , glue) P
-     ∘ pushout-dep-UP-inverse
-  ∼ id
- pushout-dep-UP-retraction {_} {P}
-  = inverses-are-sections
-     (canonical-map-to-dependent-cocone pushout f g (inll , inrr , glue) P)
-      pushout-dependent-universal-property
-
- pushout-induction
-  : {P : pushout → 𝓣  ̇}
-  → Pushout-Induction-Principle pushout f g (inll , inrr , glue) P
- pushout-induction {_} {P} l r H = pushout-dep-UP-inverse (l , r , H)
-
- pushout-ind-comp-inll
-  : {P : pushout → 𝓣  ̇}
-  → Pushout-Computation-Rule₁ pushout f g (inll , inrr , glue) P pushout-induction
- pushout-ind-comp-inll {_} {P} l r H a = {!!}
-  
- pushout-ind-comp-inrr
-  : {P : pushout → 𝓣  ̇}
-  → Pushout-Computation-Rule₂ pushout f g (inll , inrr , glue) P pushout-induction
- pushout-ind-comp-inrr l r H b = {!!}
-  
- pushout-ind-comp-glue
-  : {P : pushout → 𝓣  ̇}
-  → Pushout-Computation-Rule₃ pushout f g (inll , inrr , glue) P
-     pushout-induction pushout-ind-comp-inll pushout-ind-comp-inrr
- pushout-ind-comp-glue l r H c = {!!}
    
  pushout-recursion : {D : 𝓣  ̇}
                    → (l : A → D)
@@ -484,3 +434,164 @@ universal property. This will establish the logical equivalence between
       ∼-sym (pushout-rec-comp-glue l r G))
    
 \end{code}
+
+We investigate only postulating the (non-dependent) universal property.
+
+\begin{code}
+
+record pushouts-exist' {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A) (g : C → B) : 𝓤ω
+ where
+ field
+  pushout : 𝓤 ⊔ 𝓥 ⊔ 𝓦  ̇
+  inll : A → pushout 
+  inrr : B → pushout 
+  glue : (c : C) → inll (f c) ＝ inrr (g c)
+  pushout-universal-property
+   : {X : 𝓣  ̇}
+   → Pushout-Universal-Property pushout f g (inll , inrr , glue) X
+
+ pushout-cocone : cocone f g pushout
+ pushout-cocone = (inll , inrr , glue)
+
+\end{code}
+
+We will unpack the equivalence established by the universal property.
+
+\begin{code}
+
+ pushout-fiber-is-singleton
+  : {X : 𝓣  ̇}
+  → (s : cocone f g X)
+  → is-contr (fiber (canonical-map-to-cocone pushout f g pushout-cocone X) s)
+ pushout-fiber-is-singleton {_} {X} s
+  = equivs-are-vv-equivs (canonical-map-to-cocone pushout f g pushout-cocone X)
+     pushout-universal-property s
+
+ pushout-fiber-is-singleton'
+  : {X : 𝓣  ̇}
+  → (s : cocone f g X)
+  → is-contr (Σ u ꞉ (pushout → X) ,
+               cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+ pushout-fiber-is-singleton' {_} {X} s 
+  = equiv-to-singleton' (Σ-cong (λ - → cocone-identity-characterization f g X
+                         (- ∘ inll , - ∘ inrr , ∼-ap-∘ - glue) s))
+                        (pushout-fiber-is-singleton s)
+
+ pushout-fiber-center
+  : {X : 𝓣  ̇}
+  → (s : cocone f g X)
+  → Σ u ꞉ (pushout → X) ,
+     cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s
+ pushout-fiber-center s = center (pushout-fiber-is-singleton' s)
+
+ pushout-fiber-centrality
+  : {X : 𝓣  ̇}
+  → (s : cocone f g X)
+  → is-central (Σ u ꞉ (pushout → X) ,
+                cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+               (pushout-fiber-center s)
+ pushout-fiber-centrality s = centrality (pushout-fiber-is-singleton' s)
+
+ pushout-unique-map : {X : 𝓣  ̇}
+                    → (s : cocone f g X)
+                    → Σ u ꞉ (pushout → X) ,
+                       cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s
+                    → pushout → X
+ pushout-unique-map s (u , _) = u
+
+ pushout-inll-homotopy
+  : {X : 𝓣  ̇}
+  → (s : cocone f g X)
+  → (z : Σ u ꞉ (pushout → X) ,
+          cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+  → (pushout-unique-map s z) ∘ inll ∼ cocone-vertical-map f g X s
+ pushout-inll-homotopy s (u , K , L , M) = K
+
+ pushout-inrr-homotopy
+  : {X : 𝓣  ̇}
+  → (s : cocone f g X)
+  → (z : Σ u ꞉ (pushout → X) ,
+          cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+  → (pushout-unique-map s z) ∘ inrr ∼ cocone-horizontal-map f g X s
+ pushout-inrr-homotopy s (u , K , L , M) = L
+
+ pushout-glue-homotopy
+  : {X : 𝓣  ̇}
+  → (s : cocone f g X)
+  → (z : Σ u ꞉ (pushout → X) ,
+          cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+  → ∼-trans ((pushout-inll-homotopy s z) ∘ f) (cocone-commuting-square f g X s)
+  ∼ ∼-trans (∼-ap-∘ (pushout-unique-map s z) glue)
+            ((pushout-inrr-homotopy s z) ∘ g)
+ pushout-glue-homotopy s (u , K , L , M) = M
+
+\end{code}
+
+Now we can derive the recursion principle, the corresponding propositional
+computation rules and the uniqueness principles.
+
+\begin{code}
+
+ pushout-recursion : {D : 𝓣  ̇}
+                   → (l : A → D)
+                   → (r : B → D)
+                   → ((c : C) → l (f c) ＝ r (g c))
+                   → pushout → D
+ pushout-recursion l r G
+  = pushout-unique-map (l , r , G) (pushout-fiber-center (l , r , G))
+
+ pushout-rec-comp-inll : {D : 𝓣  ̇}
+                       → (l : A → D)
+                       → (r : B → D)
+                       → (G : (c : C) → l (f c) ＝ r (g c))
+                       → (a : A)
+                       → pushout-recursion l r G (inll a) ＝ l a
+ pushout-rec-comp-inll l r G 
+  = pushout-inll-homotopy (l , r , G) (pushout-fiber-center (l , r , G)) 
+
+ pushout-rec-comp-inrr : {D : 𝓣  ̇}
+                       → (l : A → D)
+                       → (r : B → D)
+                       → (G : (c : C) → l (f c) ＝ r (g c))
+                       → (b : B)
+                       → pushout-recursion l r G (inrr b) ＝ r b
+ pushout-rec-comp-inrr l r G
+  = pushout-inrr-homotopy (l , r , G) (pushout-fiber-center (l , r , G))
+ 
+ pushout-rec-comp-glue
+  : {D : 𝓣  ̇}
+  → (l : A → D)
+  → (r : B → D)
+  → (G : (c : C) → l (f c) ＝ r (g c))
+  → (c : C)
+  → ap (pushout-recursion l r G) (glue c) ∙ pushout-rec-comp-inrr l r G (g c) 
+  ＝ pushout-rec-comp-inll l r G (f c) ∙ G c
+ pushout-rec-comp-glue l r G c
+  = pushout-glue-homotopy (l , r , G) (pushout-fiber-center (l , r , G)) c ⁻¹
+
+ pushout-uniqueness : (X : 𝓣 ̇)
+                    → (u u' : pushout → X)
+                    → (H : (a : A) → u (inll a) ＝ u' (inll a))
+                    → (H' : (b : B) → u (inrr b) ＝ u' (inrr b))
+                    → (M : (c : C)
+                      → ap u (glue c) ∙ H' (g c) ＝ H (f c) ∙ ap u' (glue c))
+                    → (x : pushout) → u x ＝ u' x
+ pushout-uniqueness X u u' H H' M
+  = happly (pr₁ (from-Σ-＝ (singletons-are-props
+    (pushout-fiber-is-singleton' (u' ∘ inll , u' ∘ inrr , ∼-ap-∘ u' glue))
+     (u , H , H' , λ c → M c ⁻¹)
+      (u' , ∼-refl , ∼-refl , λ c → refl-left-neutral))))
+
+\end{code}
+
+Finally, we can derive the induction principle and the corresponding propositional
+computation rules(?).
+
+\begin{code}
+
+ pushout-induction
+  : {P : pushout → 𝓣  ̇}
+  → Pushout-Induction-Principle pushout f g (inll , inrr , glue) P
+ pushout-induction = {!!}
+
+\end{code}

From 138bff79610fc75aed90937c19fbb4bf05b4b21c Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Sat, 1 Feb 2025 18:07:22 -0500
Subject: [PATCH 14/18] Deriving induction from recursion and uniqueness

---
 source/UF/Pushouts.lagda | 138 ++++++++++++++++++++++++++++++++++++---
 1 file changed, 130 insertions(+), 8 deletions(-)

diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index 927af493b..ab32b59d3 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -264,7 +264,7 @@ Pushout-Computation-Rule₃
 Now we will use a record type to give the pushout, point and path constructors,
 and the dependent universal property.
 
-\begin{code}
+begin{code}
 
 record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A) (g : C → B) : 𝓤ω
  where
@@ -289,7 +289,7 @@ record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A)
    → Pushout-Computation-Rule₃ pushout f g (inll , inrr , glue) P
       pushout-induction pushout-ind-comp-inll pushout-ind-comp-inrr
 
-\end{code}
+end{code}
 
 We will observe that the pushout is a cocone and begin deriving some key
 results from the induction principles:
@@ -303,7 +303,7 @@ The following are logically equivalent
    uniqueness principle
 3) The universal property.
 
-\begin{code}
+begin{code}
 
  pushout-cocone : cocone f g pushout
  pushout-cocone = (inll , inrr , glue)
@@ -433,7 +433,7 @@ The following are logically equivalent
      (pushout-rec-comp-inll l r G , pushout-rec-comp-inrr l r G ,
       ∼-sym (pushout-rec-comp-glue l r G))
    
-\end{code}
+end{code}
 
 We investigate only postulating the (non-dependent) universal property.
 
@@ -569,14 +569,14 @@ computation rules and the uniqueness principles.
  pushout-rec-comp-glue l r G c
   = pushout-glue-homotopy (l , r , G) (pushout-fiber-center (l , r , G)) c ⁻¹
 
- pushout-uniqueness : (X : 𝓣 ̇)
+ pushout-uniqueness : {X : 𝓣 ̇}
                     → (u u' : pushout → X)
                     → (H : (a : A) → u (inll a) ＝ u' (inll a))
                     → (H' : (b : B) → u (inrr b) ＝ u' (inrr b))
                     → (M : (c : C)
                       → ap u (glue c) ∙ H' (g c) ＝ H (f c) ∙ ap u' (glue c))
                     → (x : pushout) → u x ＝ u' x
- pushout-uniqueness X u u' H H' M
+ pushout-uniqueness {_} {X} u u' H H' M
   = happly (pr₁ (from-Σ-＝ (singletons-are-props
     (pushout-fiber-is-singleton' (u' ∘ inll , u' ∘ inrr , ∼-ap-∘ u' glue))
      (u , H , H' , λ c → M c ⁻¹)
@@ -585,13 +585,135 @@ computation rules and the uniqueness principles.
 \end{code}
 
 Finally, we can derive the induction principle and the corresponding propositional
-computation rules(?).
+computation rules(?). First we will introduce an auxillary type which I am going
+to call pre-induction. 
 
 \begin{code}
 
+ pre-induction
+  : {P : pushout → 𝓣  ̇}
+  → (l : (a : A) → P (inll a))
+  → (r : (b : B) → P (inrr b))
+  → ((c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+  → pushout → Σ x ꞉ pushout , P x
+ pre-induction {_} {P} l r G = pushout-recursion l' r' G'
+  where
+   l' : A → Σ x ꞉ pushout , P x
+   l' a = (inll a , l a)
+   r' : B → Σ x ꞉ pushout , P x
+   r' b = (inrr b , r b)
+   G' : (c : C) → l' (f c) ＝ r' (g c)
+   G' c = to-Σ-＝ (glue c , G c)
+
+ pre-induction-comp-inll
+  : {P : pushout → 𝓣  ̇}
+  → (l : (a : A) → P (inll a))
+  → (r : (b : B) → P (inrr b))
+  → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+  → (a : A)
+  → pre-induction l r G (inll a) ＝ (inll a , l a)
+ pre-induction-comp-inll {_} {P} l r G = pushout-rec-comp-inll l' r' G'
+  where
+   l' : A → Σ x ꞉ pushout , P x
+   l' a = (inll a , l a)
+   r' : B → Σ x ꞉ pushout , P x
+   r' b = (inrr b , r b)
+   G' : (c : C) → l' (f c) ＝ r' (g c)
+   G' c = to-Σ-＝ (glue c , G c)
+
+ pre-induction-comp-inrr
+  : {P : pushout → 𝓣  ̇}
+  → (l : (a : A) → P (inll a))
+  → (r : (b : B) → P (inrr b))
+  → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+  → (b : B)
+  → pre-induction l r G (inrr b) ＝ (inrr b , r b)
+ pre-induction-comp-inrr {_} {P} l r G = pushout-rec-comp-inrr l' r' G'
+  where
+   l' : A → Σ x ꞉ pushout , P x
+   l' a = (inll a , l a)
+   r' : B → Σ x ꞉ pushout , P x
+   r' b = (inrr b , r b)
+   G' : (c : C) → l' (f c) ＝ r' (g c)
+   G' c = to-Σ-＝ (glue c , G c)
+
+ pre-induction-comp-glue
+  : {P : pushout → 𝓣  ̇}
+  → (l : (a : A) → P (inll a))
+  → (r : (b : B) → P (inrr b))
+  → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+  → (c : C)
+  → ap (pre-induction l r G) (glue c) ∙ pre-induction-comp-inrr l r G (g c) 
+  ＝ pre-induction-comp-inll l r G (f c) ∙ to-Σ-＝ (glue c , G c)
+ pre-induction-comp-glue {_} {P} l r G = pushout-rec-comp-glue l' r' G'
+  where
+   l' : A → Σ x ꞉ pushout , P x
+   l' a = (inll a , l a)
+   r' : B → Σ x ꞉ pushout , P x
+   r' b = (inrr b , r b)
+   G' : (c : C) → l' (f c) ＝ r' (g c)
+   G' c = to-Σ-＝ (glue c , G c)
+
+ pre-induction-id
+  : {P : pushout → 𝓣  ̇}
+  → (l : (a : A) → P (inll a))
+  → (r : (b : B) → P (inrr b))
+  → ((c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+  → pushout → pushout
+ pre-induction-id l r G = pr₁ ∘ pre-induction l r G
+
+ pre-induction-id-is-id
+  : {P : pushout → 𝓣  ̇}
+  → (l : (a : A) → P (inll a))
+  → (r : (b : B) → P (inrr b))
+  → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+  → (x : pushout) → pre-induction-id l r G x ＝ x
+ pre-induction-id-is-id {_} {P} l r G
+  = pushout-uniqueness (pre-induction-id l r G) id
+     (λ a → ap pr₁ (pre-induction-comp-inll l r G a))
+     (λ b → ap pr₁ (pre-induction-comp-inrr l r G b))
+     I
+  where
+   I : (c : C)
+     → ap (pre-induction-id l r G) (glue c)
+       ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))
+     ＝ ap pr₁ (pre-induction-comp-inll l r G (f c)) ∙ ap id (glue c)
+   I c = ap (pre-induction-id l r G) (glue c)
+         ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))            ＝⟨ II ⟩
+         ap pr₁ (ap (pre-induction l r G) (glue c))
+         ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))            ＝⟨ III ⟩
+         ap pr₁ (ap (pre-induction l r G) (glue c)
+         ∙ pre-induction-comp-inrr l r G (g c))                    ＝⟨ IV ⟩
+         ap pr₁ (pre-induction-comp-inll l r G (f c)
+         ∙ to-Σ-＝ (glue c , G c))                                 ＝⟨ V ⟩
+         ap pr₁ (pre-induction-comp-inll l r G (f c))
+         ∙ ap pr₁ (to-Σ-＝ (glue c , G c))                         ＝⟨ VII ⟩
+         ap pr₁ (pre-induction-comp-inll l r G (f c))
+         ∙ ap id (glue c)                                          ∎
+    where
+     II = ap (_∙ ap pr₁ (pre-induction-comp-inrr l r G (g c)))
+             (ap-ap (pre-induction l r G) pr₁ (glue c) ⁻¹)
+     III = ap-∙ pr₁ (ap (pre-induction l r G) (glue c))
+                (pre-induction-comp-inrr l r G (g c)) ⁻¹
+     IV = ap (ap pr₁) (pre-induction-comp-glue l r G c)
+     V = ap-∙ pr₁ (pre-induction-comp-inll l r G (f c)) (to-Σ-＝ (glue c , G c))
+     VI = ap pr₁ (to-Σ-＝ (glue c , G c)) ＝⟨ ap-pr₁-to-Σ-＝ (glue c , G c) ⟩
+          glue c                          ＝⟨ ap-id-is-id' (glue c) ⟩
+          ap id (glue c)                  ∎ 
+     VII = ap (ap pr₁ (pre-induction-comp-inll l r G (f c)) ∙_) VI 
+
+ pre-induction-family
+  : {P : pushout → 𝓣  ̇}
+  → (l : (a : A) → P (inll a))
+  → (r : (b : B) → P (inrr b))
+  → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+  → (x : pushout) → P (pre-induction-id l r G x)
+ pre-induction-family l r G = pr₂ ∘ pre-induction l r G
+
  pushout-induction
   : {P : pushout → 𝓣  ̇}
   → Pushout-Induction-Principle pushout f g (inll , inrr , glue) P
- pushout-induction = {!!}
+ pushout-induction {_} {P} l r G x
+  = transport P (pre-induction-id-is-id l r G x) (pre-induction-family l r G x)
 
 \end{code}

From c5e592616e1a257a1dc30bb1c5d502aac5a56096 Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Sun, 2 Feb 2025 18:16:39 -0500
Subject: [PATCH 15/18] update

---
 source/UF/Pushouts.lagda | 47 ++++++++++++++++++++++++++++++----------
 1 file changed, 35 insertions(+), 12 deletions(-)

diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index ab32b59d3..fb283e741 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -471,7 +471,7 @@ We will unpack the equivalence established by the universal property.
   : {X : 𝓣  ̇}
   → (s : cocone f g X)
   → is-contr (Σ u ꞉ (pushout → X) ,
-               cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+                cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
  pushout-fiber-is-singleton' {_} {X} s 
   = equiv-to-singleton' (Σ-cong (λ - → cocone-identity-characterization f g X
                          (- ∘ inll , - ∘ inrr , ∼-ap-∘ - glue) s))
@@ -481,21 +481,21 @@ We will unpack the equivalence established by the universal property.
   : {X : 𝓣  ̇}
   → (s : cocone f g X)
   → Σ u ꞉ (pushout → X) ,
-     cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s
+      cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s
  pushout-fiber-center s = center (pushout-fiber-is-singleton' s)
 
  pushout-fiber-centrality
   : {X : 𝓣  ̇}
   → (s : cocone f g X)
   → is-central (Σ u ꞉ (pushout → X) ,
-                cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+                  cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
                (pushout-fiber-center s)
  pushout-fiber-centrality s = centrality (pushout-fiber-is-singleton' s)
 
  pushout-unique-map : {X : 𝓣  ̇}
                     → (s : cocone f g X)
                     → Σ u ꞉ (pushout → X) ,
-                       cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s
+                      cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s
                     → pushout → X
  pushout-unique-map s (u , _) = u
 
@@ -503,7 +503,7 @@ We will unpack the equivalence established by the universal property.
   : {X : 𝓣  ̇}
   → (s : cocone f g X)
   → (z : Σ u ꞉ (pushout → X) ,
-          cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+           cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
   → (pushout-unique-map s z) ∘ inll ∼ cocone-vertical-map f g X s
  pushout-inll-homotopy s (u , K , L , M) = K
 
@@ -511,7 +511,7 @@ We will unpack the equivalence established by the universal property.
   : {X : 𝓣  ̇}
   → (s : cocone f g X)
   → (z : Σ u ꞉ (pushout → X) ,
-          cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+           cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
   → (pushout-unique-map s z) ∘ inrr ∼ cocone-horizontal-map f g X s
  pushout-inrr-homotopy s (u , K , L , M) = L
 
@@ -519,7 +519,7 @@ We will unpack the equivalence established by the universal property.
   : {X : 𝓣  ̇}
   → (s : cocone f g X)
   → (z : Σ u ꞉ (pushout → X) ,
-          cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+           cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
   → ∼-trans ((pushout-inll-homotopy s z) ∘ f) (cocone-commuting-square f g X s)
   ∼ ∼-trans (∼-ap-∘ (pushout-unique-map s z) glue)
             ((pushout-inrr-homotopy s z) ∘ g)
@@ -574,7 +574,7 @@ computation rules and the uniqueness principles.
                     → (H : (a : A) → u (inll a) ＝ u' (inll a))
                     → (H' : (b : B) → u (inrr b) ＝ u' (inrr b))
                     → (M : (c : C)
-                      → ap u (glue c) ∙ H' (g c) ＝ H (f c) ∙ ap u' (glue c))
+                     → ap u (glue c) ∙ H' (g c) ＝ H (f c) ∙ ap u' (glue c))
                     → (x : pushout) → u x ＝ u' x
  pushout-uniqueness {_} {X} u u' H H' M
   = happly (pr₁ (from-Σ-＝ (singletons-are-props
@@ -585,8 +585,8 @@ computation rules and the uniqueness principles.
 \end{code}
 
 Finally, we can derive the induction principle and the corresponding propositional
-computation rules(?). First we will introduce an auxillary type which I am going
-to call pre-induction. 
+computation rules(?). First we will introduce an auxillary type which we will
+call pre-induction. 
 
 \begin{code}
 
@@ -671,8 +671,8 @@ to call pre-induction.
  pre-induction-id-is-id {_} {P} l r G
   = pushout-uniqueness (pre-induction-id l r G) id
      (λ a → ap pr₁ (pre-induction-comp-inll l r G a))
-     (λ b → ap pr₁ (pre-induction-comp-inrr l r G b))
-     I
+      (λ b → ap pr₁ (pre-induction-comp-inrr l r G b))
+       I
   where
    I : (c : C)
      → ap (pre-induction-id l r G) (glue c)
@@ -710,10 +710,33 @@ to call pre-induction.
   → (x : pushout) → P (pre-induction-id l r G x)
  pre-induction-family l r G = pr₂ ∘ pre-induction l r G
 
+\end{code}
+
+Now we can define the induction principle and computation rules.
+
+\begin{code}
+
  pushout-induction
   : {P : pushout → 𝓣  ̇}
   → Pushout-Induction-Principle pushout f g (inll , inrr , glue) P
  pushout-induction {_} {P} l r G x
   = transport P (pre-induction-id-is-id l r G x) (pre-induction-family l r G x)
 
+ pushout-induction-comp-inll
+  : {P : pushout → 𝓣  ̇}
+  → Pushout-Computation-Rule₁ pushout f g (inll , inrr , glue) P pushout-induction 
+ pushout-induction-comp-inll l r H a
+  = {!pushout-induction l r H (inll a) ＝⟨ ? ⟩ ?!}
+
+ pushout-induction-comp-inrr
+  : {P : pushout → 𝓣  ̇}
+  → Pushout-Computation-Rule₂ pushout f g (inll , inrr , glue) P pushout-induction 
+ pushout-induction-comp-inrr l r H b = {!!}
+
+ pushout-induction-comp-glue
+  : {P : pushout → 𝓣  ̇}
+  → Pushout-Computation-Rule₃ pushout f g (inll , inrr , glue) P pushout-induction
+     pushout-induction-comp-inll pushout-induction-comp-inrr
+ pushout-induction-comp-glue = {!!}
+
 \end{code}

From 9f734620ab06a1fb4c651d952ff9e509d202aa42 Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Mon, 3 Feb 2025 11:27:58 -0500
Subject: [PATCH 16/18] update induction computation rules

---
 source/UF/Pushouts.lagda | 407 +++++++++++++++++++++------------------
 1 file changed, 224 insertions(+), 183 deletions(-)

diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index fb283e741..6677de151 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -459,71 +459,72 @@ We will unpack the equivalence established by the universal property.
 
 \begin{code}
 
- pushout-fiber-is-singleton
-  : {X : 𝓣  ̇}
-  → (s : cocone f g X)
-  → is-contr (fiber (canonical-map-to-cocone pushout f g pushout-cocone X) s)
- pushout-fiber-is-singleton {_} {X} s
-  = equivs-are-vv-equivs (canonical-map-to-cocone pushout f g pushout-cocone X)
-     pushout-universal-property s
-
- pushout-fiber-is-singleton'
-  : {X : 𝓣  ̇}
-  → (s : cocone f g X)
-  → is-contr (Σ u ꞉ (pushout → X) ,
-                cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
- pushout-fiber-is-singleton' {_} {X} s 
-  = equiv-to-singleton' (Σ-cong (λ - → cocone-identity-characterization f g X
-                         (- ∘ inll , - ∘ inrr , ∼-ap-∘ - glue) s))
-                        (pushout-fiber-is-singleton s)
-
- pushout-fiber-center
-  : {X : 𝓣  ̇}
-  → (s : cocone f g X)
-  → Σ u ꞉ (pushout → X) ,
+ opaque
+  pushout-fiber-is-singleton
+   : {X : 𝓣  ̇}
+   → (s : cocone f g X)
+   → is-contr (fiber (canonical-map-to-cocone pushout f g pushout-cocone X) s)
+  pushout-fiber-is-singleton {_} {X} s
+   = equivs-are-vv-equivs (canonical-map-to-cocone pushout f g pushout-cocone X)
+    pushout-universal-property s
+
+  pushout-fiber-is-singleton'
+   : {X : 𝓣  ̇}
+   → (s : cocone f g X)
+   → is-contr (Σ u ꞉ (pushout → X) ,
+                 cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+  pushout-fiber-is-singleton' {_} {X} s 
+   = equiv-to-singleton' (Σ-cong (λ - → cocone-identity-characterization f g X
+                          (- ∘ inll , - ∘ inrr , ∼-ap-∘ - glue) s))
+                         (pushout-fiber-is-singleton s)
+
+  pushout-fiber-center
+   : {X : 𝓣  ̇}
+   → (s : cocone f g X)
+   → Σ u ꞉ (pushout → X) ,
       cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s
- pushout-fiber-center s = center (pushout-fiber-is-singleton' s)
-
- pushout-fiber-centrality
-  : {X : 𝓣  ̇}
-  → (s : cocone f g X)
-  → is-central (Σ u ꞉ (pushout → X) ,
-                  cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
-               (pushout-fiber-center s)
- pushout-fiber-centrality s = centrality (pushout-fiber-is-singleton' s)
-
- pushout-unique-map : {X : 𝓣  ̇}
-                    → (s : cocone f g X)
-                    → Σ u ꞉ (pushout → X) ,
-                      cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s
-                    → pushout → X
- pushout-unique-map s (u , _) = u
-
- pushout-inll-homotopy
-  : {X : 𝓣  ̇}
-  → (s : cocone f g X)
-  → (z : Σ u ꞉ (pushout → X) ,
-           cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
-  → (pushout-unique-map s z) ∘ inll ∼ cocone-vertical-map f g X s
- pushout-inll-homotopy s (u , K , L , M) = K
-
- pushout-inrr-homotopy
-  : {X : 𝓣  ̇}
-  → (s : cocone f g X)
-  → (z : Σ u ꞉ (pushout → X) ,
-           cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
-  → (pushout-unique-map s z) ∘ inrr ∼ cocone-horizontal-map f g X s
- pushout-inrr-homotopy s (u , K , L , M) = L
-
- pushout-glue-homotopy
-  : {X : 𝓣  ̇}
-  → (s : cocone f g X)
-  → (z : Σ u ꞉ (pushout → X) ,
-           cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
-  → ∼-trans ((pushout-inll-homotopy s z) ∘ f) (cocone-commuting-square f g X s)
-  ∼ ∼-trans (∼-ap-∘ (pushout-unique-map s z) glue)
-            ((pushout-inrr-homotopy s z) ∘ g)
- pushout-glue-homotopy s (u , K , L , M) = M
+  pushout-fiber-center s = center (pushout-fiber-is-singleton' s)
+
+  pushout-fiber-centrality
+   : {X : 𝓣  ̇}
+   → (s : cocone f g X)
+   → is-central (Σ u ꞉ (pushout → X) ,
+                   cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+                (pushout-fiber-center s)
+  pushout-fiber-centrality s = centrality (pushout-fiber-is-singleton' s)
+
+  pushout-unique-map : {X : 𝓣  ̇}
+                     → (s : cocone f g X)
+                     → Σ u ꞉ (pushout → X) ,
+                        cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s
+                     → pushout → X
+  pushout-unique-map s (u , _) = u
+
+  pushout-inll-homotopy
+   : {X : 𝓣  ̇}
+   → (s : cocone f g X)
+   → (z : Σ u ꞉ (pushout → X) ,
+            cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+   → (pushout-unique-map s z) ∘ inll ∼ cocone-vertical-map f g X s
+  pushout-inll-homotopy s (u , K , L , M) = K
+
+  pushout-inrr-homotopy
+   : {X : 𝓣  ̇}
+   → (s : cocone f g X)
+   → (z : Σ u ꞉ (pushout → X) ,
+            cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+   → (pushout-unique-map s z) ∘ inrr ∼ cocone-horizontal-map f g X s
+  pushout-inrr-homotopy s (u , K , L , M) = L
+
+  pushout-glue-homotopy
+   : {X : 𝓣  ̇}
+   → (s : cocone f g X)
+   → (z : Σ u ꞉ (pushout → X) ,
+            cocone-family f g X (u ∘ inll , u ∘ inrr , ∼-ap-∘ u glue) s)
+   → ∼-trans ((pushout-inll-homotopy s z) ∘ f) (cocone-commuting-square f g X s)
+   ∼ ∼-trans (∼-ap-∘ (pushout-unique-map s z) glue)
+             ((pushout-inrr-homotopy s z) ∘ g)
+  pushout-glue-homotopy s (u , K , L , M) = M
 
 \end{code}
 
@@ -590,125 +591,164 @@ call pre-induction.
 
 \begin{code}
 
- pre-induction
-  : {P : pushout → 𝓣  ̇}
-  → (l : (a : A) → P (inll a))
-  → (r : (b : B) → P (inrr b))
-  → ((c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-  → pushout → Σ x ꞉ pushout , P x
- pre-induction {_} {P} l r G = pushout-recursion l' r' G'
-  where
-   l' : A → Σ x ꞉ pushout , P x
-   l' a = (inll a , l a)
-   r' : B → Σ x ꞉ pushout , P x
-   r' b = (inrr b , r b)
-   G' : (c : C) → l' (f c) ＝ r' (g c)
-   G' c = to-Σ-＝ (glue c , G c)
-
- pre-induction-comp-inll
-  : {P : pushout → 𝓣  ̇}
-  → (l : (a : A) → P (inll a))
-  → (r : (b : B) → P (inrr b))
-  → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-  → (a : A)
-  → pre-induction l r G (inll a) ＝ (inll a , l a)
- pre-induction-comp-inll {_} {P} l r G = pushout-rec-comp-inll l' r' G'
-  where
-   l' : A → Σ x ꞉ pushout , P x
-   l' a = (inll a , l a)
-   r' : B → Σ x ꞉ pushout , P x
-   r' b = (inrr b , r b)
-   G' : (c : C) → l' (f c) ＝ r' (g c)
-   G' c = to-Σ-＝ (glue c , G c)
-
- pre-induction-comp-inrr
-  : {P : pushout → 𝓣  ̇}
-  → (l : (a : A) → P (inll a))
-  → (r : (b : B) → P (inrr b))
-  → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-  → (b : B)
-  → pre-induction l r G (inrr b) ＝ (inrr b , r b)
- pre-induction-comp-inrr {_} {P} l r G = pushout-rec-comp-inrr l' r' G'
-  where
-   l' : A → Σ x ꞉ pushout , P x
-   l' a = (inll a , l a)
-   r' : B → Σ x ꞉ pushout , P x
-   r' b = (inrr b , r b)
-   G' : (c : C) → l' (f c) ＝ r' (g c)
-   G' c = to-Σ-＝ (glue c , G c)
-
- pre-induction-comp-glue
-  : {P : pushout → 𝓣  ̇}
-  → (l : (a : A) → P (inll a))
-  → (r : (b : B) → P (inrr b))
-  → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-  → (c : C)
-  → ap (pre-induction l r G) (glue c) ∙ pre-induction-comp-inrr l r G (g c) 
-  ＝ pre-induction-comp-inll l r G (f c) ∙ to-Σ-＝ (glue c , G c)
- pre-induction-comp-glue {_} {P} l r G = pushout-rec-comp-glue l' r' G'
-  where
-   l' : A → Σ x ꞉ pushout , P x
-   l' a = (inll a , l a)
-   r' : B → Σ x ꞉ pushout , P x
-   r' b = (inrr b , r b)
-   G' : (c : C) → l' (f c) ＝ r' (g c)
-   G' c = to-Σ-＝ (glue c , G c)
-
- pre-induction-id
-  : {P : pushout → 𝓣  ̇}
-  → (l : (a : A) → P (inll a))
-  → (r : (b : B) → P (inrr b))
-  → ((c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-  → pushout → pushout
- pre-induction-id l r G = pr₁ ∘ pre-induction l r G
+ opaque
+  pre-induction
+   : {P : pushout → 𝓣  ̇}
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → ((c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → pushout → Σ x ꞉ pushout , P x
+  pre-induction {_} {P} l r G = pushout-recursion l' r' G'
+   where
+    l' : A → Σ x ꞉ pushout , P x
+    l' a = (inll a , l a)
+    r' : B → Σ x ꞉ pushout , P x
+    r' b = (inrr b , r b)
+    G' : (c : C) → l' (f c) ＝ r' (g c)
+    G' c = to-Σ-＝ (glue c , G c)
+
+  pre-induction-comp-inll
+   : {P : pushout → 𝓣  ̇}
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → (a : A)
+   → pre-induction l r G (inll a) ＝ (inll a , l a)
+  pre-induction-comp-inll {_} {P} l r G = pushout-rec-comp-inll l' r' G'
+   where
+    l' : A → Σ x ꞉ pushout , P x
+    l' a = (inll a , l a)
+    r' : B → Σ x ꞉ pushout , P x
+    r' b = (inrr b , r b)
+    G' : (c : C) → l' (f c) ＝ r' (g c)
+    G' c = to-Σ-＝ (glue c , G c)
+
+  pre-induction-comp-inrr
+   : {P : pushout → 𝓣  ̇}
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → (b : B)
+   → pre-induction l r G (inrr b) ＝ (inrr b , r b)
+  pre-induction-comp-inrr {_} {P} l r G = pushout-rec-comp-inrr l' r' G'
+   where
+    l' : A → Σ x ꞉ pushout , P x
+    l' a = (inll a , l a)
+    r' : B → Σ x ꞉ pushout , P x
+    r' b = (inrr b , r b)
+    G' : (c : C) → l' (f c) ＝ r' (g c)
+    G' c = to-Σ-＝ (glue c , G c)
+
+  pre-induction-comp-glue
+   : {P : pushout → 𝓣  ̇}
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → (c : C)
+   → ap (pre-induction l r G) (glue c) ∙ pre-induction-comp-inrr l r G (g c) 
+   ＝ pre-induction-comp-inll l r G (f c) ∙ to-Σ-＝ (glue c , G c)
+  pre-induction-comp-glue {_} {P} l r G = pushout-rec-comp-glue l' r' G'
+   where
+    l' : A → Σ x ꞉ pushout , P x
+    l' a = (inll a , l a)
+    r' : B → Σ x ꞉ pushout , P x
+    r' b = (inrr b , r b)
+    G' : (c : C) → l' (f c) ＝ r' (g c)
+    G' c = to-Σ-＝ (glue c , G c)
+
+  pre-induction-id
+   : {P : pushout → 𝓣  ̇}
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → ((c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → pushout → pushout
+  pre-induction-id l r G = pr₁ ∘ pre-induction l r G
 
- pre-induction-id-is-id
-  : {P : pushout → 𝓣  ̇}
-  → (l : (a : A) → P (inll a))
-  → (r : (b : B) → P (inrr b))
-  → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-  → (x : pushout) → pre-induction-id l r G x ＝ x
- pre-induction-id-is-id {_} {P} l r G
-  = pushout-uniqueness (pre-induction-id l r G) id
-     (λ a → ap pr₁ (pre-induction-comp-inll l r G a))
-      (λ b → ap pr₁ (pre-induction-comp-inrr l r G b))
-       I
-  where
-   I : (c : C)
-     → ap (pre-induction-id l r G) (glue c)
-       ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))
-     ＝ ap pr₁ (pre-induction-comp-inll l r G (f c)) ∙ ap id (glue c)
-   I c = ap (pre-induction-id l r G) (glue c)
-         ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))            ＝⟨ II ⟩
-         ap pr₁ (ap (pre-induction l r G) (glue c))
-         ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))            ＝⟨ III ⟩
-         ap pr₁ (ap (pre-induction l r G) (glue c)
-         ∙ pre-induction-comp-inrr l r G (g c))                    ＝⟨ IV ⟩
-         ap pr₁ (pre-induction-comp-inll l r G (f c)
-         ∙ to-Σ-＝ (glue c , G c))                                 ＝⟨ V ⟩
-         ap pr₁ (pre-induction-comp-inll l r G (f c))
-         ∙ ap pr₁ (to-Σ-＝ (glue c , G c))                         ＝⟨ VII ⟩
-         ap pr₁ (pre-induction-comp-inll l r G (f c))
-         ∙ ap id (glue c)                                          ∎
-    where
-     II = ap (_∙ ap pr₁ (pre-induction-comp-inrr l r G (g c)))
-             (ap-ap (pre-induction l r G) pr₁ (glue c) ⁻¹)
-     III = ap-∙ pr₁ (ap (pre-induction l r G) (glue c))
-                (pre-induction-comp-inrr l r G (g c)) ⁻¹
-     IV = ap (ap pr₁) (pre-induction-comp-glue l r G c)
-     V = ap-∙ pr₁ (pre-induction-comp-inll l r G (f c)) (to-Σ-＝ (glue c , G c))
-     VI = ap pr₁ (to-Σ-＝ (glue c , G c)) ＝⟨ ap-pr₁-to-Σ-＝ (glue c , G c) ⟩
-          glue c                          ＝⟨ ap-id-is-id' (glue c) ⟩
-          ap id (glue c)                  ∎ 
-     VII = ap (ap pr₁ (pre-induction-comp-inll l r G (f c)) ∙_) VI 
-
- pre-induction-family
-  : {P : pushout → 𝓣  ̇}
-  → (l : (a : A) → P (inll a))
-  → (r : (b : B) → P (inrr b))
-  → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
-  → (x : pushout) → P (pre-induction-id l r G x)
- pre-induction-family l r G = pr₂ ∘ pre-induction l r G
+  pre-induction-id-is-id
+   : {P : pushout → 𝓣  ̇}
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → (x : pushout) → pre-induction-id l r G x ＝ x
+  pre-induction-id-is-id {_} {P} l r G
+   = pushout-uniqueness (pre-induction-id l r G) id
+      (λ a → ap pr₁ (pre-induction-comp-inll l r G a))
+       (λ b → ap pr₁ (pre-induction-comp-inrr l r G b))
+        I
+   where
+    I : (c : C)
+      → ap (pre-induction-id l r G) (glue c)
+        ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))
+      ＝ ap pr₁ (pre-induction-comp-inll l r G (f c)) ∙ ap id (glue c)
+    I c = ap (pre-induction-id l r G) (glue c)
+          ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))            ＝⟨ II ⟩
+          ap pr₁ (ap (pre-induction l r G) (glue c))
+          ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))            ＝⟨ III ⟩
+          ap pr₁ (ap (pre-induction l r G) (glue c)
+          ∙ pre-induction-comp-inrr l r G (g c))                    ＝⟨ IV ⟩
+          ap pr₁ (pre-induction-comp-inll l r G (f c)
+          ∙ to-Σ-＝ (glue c , G c))                                 ＝⟨ V ⟩
+          ap pr₁ (pre-induction-comp-inll l r G (f c))
+          ∙ ap pr₁ (to-Σ-＝ (glue c , G c))                         ＝⟨ VII ⟩
+          ap pr₁ (pre-induction-comp-inll l r G (f c))
+          ∙ ap id (glue c)                                          ∎
+     where
+      II : ap (pre-induction-id l r G) (glue c)
+          ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))
+        ＝ ap pr₁ (ap (pre-induction l r G) (glue c))
+          ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c)) 
+      II = ap (_∙ ap pr₁ (pre-induction-comp-inrr l r G (g c)))
+              (ap-ap (pre-induction l r G) pr₁ (glue c) ⁻¹)
+      III : ap pr₁ (ap (pre-induction l r G) (glue c))
+           ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))
+          ＝ ap pr₁ (ap (pre-induction l r G) (glue c)
+           ∙ pre-induction-comp-inrr l r G (g c))
+      III = ap-∙ pr₁ (ap (pre-induction l r G) (glue c))
+                 (pre-induction-comp-inrr l r G (g c)) ⁻¹
+      IV : ap pr₁ (ap (pre-induction l r G) (glue c)
+          ∙ pre-induction-comp-inrr l r G (g c))
+         ＝ ap pr₁ (pre-induction-comp-inll l r G (f c)
+          ∙ to-Σ-＝ (glue c , G c))  
+      IV = ap (ap pr₁) (pre-induction-comp-glue l r G c)
+      V : ap pr₁ (pre-induction-comp-inll l r G (f c)
+          ∙ to-Σ-＝ (glue c , G c))
+        ＝ ap pr₁ (pre-induction-comp-inll l r G (f c))
+          ∙ ap pr₁ (to-Σ-＝ (glue c , G c)) 
+      V = ap-∙ pr₁ (pre-induction-comp-inll l r G (f c)) (to-Σ-＝ (glue c , G c))
+      VI : ap pr₁ (to-Σ-＝ (glue c , G c)) ＝ ap id (glue c) 
+      VI = ap pr₁ (to-Σ-＝ (glue c , G c)) ＝⟨ ap-pr₁-to-Σ-＝ (glue c , G c) ⟩
+           glue c                          ＝⟨ ap-id-is-id' (glue c) ⟩
+           ap id (glue c)                  ∎
+      VII : ap pr₁ (pre-induction-comp-inll l r G (f c))
+           ∙ ap pr₁ (to-Σ-＝ (glue c , G c))
+          ＝ ap pr₁ (pre-induction-comp-inll l r G (f c))
+           ∙ ap id (glue c)   
+      VII = ap (ap pr₁ (pre-induction-comp-inll l r G (f c)) ∙_) VI 
+
+  pre-induction-family
+   : {P : pushout → 𝓣  ̇}
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → (x : pushout) → P (pre-induction-id l r G x)
+  pre-induction-family l r G = pr₂ ∘ pre-induction l r G
+
+  pre-induction-family-comp-inll
+   : {P : pushout → 𝓣  ̇}
+   → (l : (a : A) → P (inll a))
+   → (r : (b : B) → P (inrr b))
+   → (G : (c : C) → transport P (glue c) (l (f c)) ＝ r (g c))
+   → (a : A)
+   → transport P (pre-induction-id-is-id l r G (inll a))
+                 (pre-induction-family l r G (inll a))
+   ＝ l a
+  pre-induction-family-comp-inll l r G a
+   = {!!}
+   where
+    I : (a : A)
+      → pre-induction-id-is-id l r G (inll a)
+      ＝ ap pr₁ (pre-induction-comp-inll l r G a)
+    I a = {!pushout-rec-comp-inll!}
 
 \end{code}
 
@@ -726,7 +766,7 @@ Now we can define the induction principle and computation rules.
   : {P : pushout → 𝓣  ̇}
   → Pushout-Computation-Rule₁ pushout f g (inll , inrr , glue) P pushout-induction 
  pushout-induction-comp-inll l r H a
-  = {!pushout-induction l r H (inll a) ＝⟨ ? ⟩ ?!}
+  = pre-induction-family-comp-inll l r H a
 
  pushout-induction-comp-inrr
   : {P : pushout → 𝓣  ̇}
@@ -740,3 +780,4 @@ Now we can define the induction principle and computation rules.
  pushout-induction-comp-glue = {!!}
 
 \end{code}
+

From 7273aaac562afd16b07a404d52762bb6fa60057e Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Fri, 7 Feb 2025 12:04:41 -0500
Subject: [PATCH 17/18] Splitting files

---
 source/UF/CoconesofSpans.lagda | 257 +++++++++++++++++++++++++++++++++
 source/UF/Pushouts.lagda       | 223 ++++++++++------------------
 2 files changed, 332 insertions(+), 148 deletions(-)
 create mode 100644 source/UF/CoconesofSpans.lagda

diff --git a/source/UF/CoconesofSpans.lagda b/source/UF/CoconesofSpans.lagda
new file mode 100644
index 000000000..b2b1a5baf
--- /dev/null
+++ b/source/UF/CoconesofSpans.lagda
@@ -0,0 +1,257 @@
+Ian Ray, 15th January 2025
+
+We will prove some results about cocones of spans.
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+open import UF.FunExt
+
+module UF.CoconesofSpans (fe : Fun-Ext) where
+
+open import MLTT.Spartan
+open import UF.Base
+open import UF.Equiv
+open import UF.EquivalenceExamples
+open import UF.PropIndexedPiSigma
+open import UF.Retracts
+open import UF.Subsingletons
+open import UF.Yoneda
+
+\end{code}
+
+We start by defining cocones and characerizing their identity type.
+
+\begin{code}
+
+cocone : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+         (f : C → A) (g : C → B) (X : 𝓣  ̇)
+       → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
+cocone {𝓤} {𝓥} {𝓦} {𝓣} {A} {B} {C} f g X =
+ Σ i ꞉ (A → X) , Σ j ꞉ (B → X) , (i ∘ f ∼ j ∘ g)
+
+cocone-vertical-map : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                      (f : C → A) (g : C → B) (X : 𝓣  ̇)
+                    → cocone f g X
+                    → (A → X)
+cocone-vertical-map f g X (i , j , K) = i
+
+cocone-horizontal-map : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                        (f : C → A) (g : C → B) (X : 𝓣  ̇)
+                      → cocone f g X
+                      → (B → X)
+cocone-horizontal-map f g X (i , j , K) = j
+
+cocone-commuting-square : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                          (f : C → A) (g : C → B) (X : 𝓣  ̇)
+                        → ((i , j , K) : cocone f g X)
+                        → i ∘ f ∼ j ∘ g
+cocone-commuting-square f g X (i , j , K) = K
+
+cocone-family : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                (f : C → A) (g : C → B) (X : 𝓣  ̇)
+              → cocone f g X → cocone f g X
+              → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
+cocone-family f g X (i , j , H) (i' , j' , H') =
+ Σ K ꞉ i ∼ i' , Σ L ꞉ j ∼ j' ,
+  ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g)
+
+canonical-map-from-identity-to-cocone-family
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+   (f : C → A) (g : C → B) (X : 𝓣  ̇)
+ → (u u' : cocone f g X)
+ → u ＝ u'
+ → cocone-family f g X u u'
+canonical-map-from-identity-to-cocone-family
+ f g X (i , j , H) .(i , j , H) refl =
+ (∼-refl , ∼-refl , λ - → refl-left-neutral)
+
+cocone-family-is-identity-system
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+   (f : C → A) (g : C → B) (X : 𝓣  ̇)
+ → (x : cocone f g X)
+ → is-contr (Σ y ꞉ cocone f g X , cocone-family f g X x y)
+cocone-family-is-identity-system {_} {_} {_} {𝓣} {A} {B} {C} f g X (i , j , H) =
+ equiv-to-singleton e 𝟙-is-singleton
+ where
+  e : (Σ y ꞉ cocone f g X , cocone-family f g X (i , j , H) y) ≃ 𝟙 { 𝓣 }
+  e = (Σ y ꞉ cocone f g X , cocone-family f g X (i , j , H) y) ≃⟨ I ⟩
+      (Σ i' ꞉ (A → X) , Σ j' ꞉ (B → X) ,
+        Σ H' ꞉ (i' ∘ f ∼ j' ∘ g) ,
+         Σ K ꞉ i ∼ i' , Σ L ꞉ j ∼ j' ,
+          ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g))              ≃⟨ II ⟩
+      (Σ i' ꞉ (A → X) , Σ K ꞉ i ∼ i' ,
+        Σ j' ꞉ (B → X) , Σ L ꞉ j ∼ j' ,
+         Σ H' ꞉ (i' ∘ f ∼ j' ∘ g) ,
+          ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g))              ≃⟨ VII ⟩
+      (Σ H' ꞉ (i ∘ f ∼ j ∘ g) , H' ∼ H)                        ≃⟨ IXV ⟩
+      𝟙                                                        ■
+   where
+    I = ≃-comp Σ-assoc (Σ-cong (λ i' → Σ-assoc))
+    II = Σ-cong (λ _ → ≃-comp (Σ-cong
+          (λ _ → ≃-comp Σ-flip (Σ-cong (λ K → Σ-flip)))) Σ-flip)
+    III = (Σ i' ꞉ (A → X) , i ∼ i')  ≃⟨ IV ⟩
+          (Σ i' ꞉ (A → X) , i ＝ i') ≃⟨ V ⟩
+          𝟙                          ■
+     where
+      IV = Σ-cong (λ - → ≃-sym (≃-funext fe i -))
+      V = singleton-≃-𝟙 (singleton-types-are-singletons i)
+    VI = ≃-comp (Σ-cong (λ - → ≃-sym (≃-funext fe j -)))
+                (singleton-≃-𝟙 (singleton-types-are-singletons j))
+    VII = (Σ i' ꞉ (A → X) , Σ K ꞉ i ∼ i' ,
+            Σ j' ꞉ (B → X) , Σ L ꞉ j ∼ j' ,
+             Σ H' ꞉ (i' ∘ f ∼ j' ∘ g) ,
+              ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g))           ≃⟨ IIIV ⟩
+          (Σ (i' , K) ꞉ (Σ i' ꞉ (A → X) , i ∼ i') ,
+            Σ j' ꞉ (B → X) , Σ L ꞉ j ∼ j' ,
+             Σ H' ꞉ (i' ∘ f ∼ j' ∘ g) ,
+              ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g))           ≃⟨ IX ⟩
+           (Σ j' ꞉ (B → X) , Σ L ꞉ j ∼ j' ,
+             Σ H' ꞉ (i ∘ f ∼ j' ∘ g) ,
+              ∼-trans (∼-refl ∘ f) H' ∼ ∼-trans H (L ∘ g))      ≃⟨ XI ⟩
+           (Σ (j' , L) ꞉ (Σ j' ꞉ (B → X) , j ∼ j') ,
+             Σ H' ꞉ (i ∘ f ∼ j' ∘ g) ,
+              ∼-trans (∼-refl ∘ f) H' ∼ ∼-trans H (L ∘ g))      ≃⟨ XII ⟩
+           (Σ H' ꞉ (i ∘ f ∼ j ∘ g) ,
+             ∼-trans (∼-refl ∘ f) H' ∼ ∼-trans H (∼-refl ∘ g))  ≃⟨ XIII ⟩
+           (Σ H' ꞉ (i ∘ f ∼ j ∘ g) , H' ∼ H)                    ■
+     where
+      IIIV = ≃-sym Σ-assoc
+      IX = prop-indexed-sum (equiv-to-prop III 𝟙-is-prop) (i , ∼-refl)
+      XI = ≃-sym Σ-assoc
+      XII = prop-indexed-sum (equiv-to-prop VI 𝟙-is-prop) (j , ∼-refl)
+      XIII = Σ-cong (λ H' → Π-cong fe fe (λ c → ＝-cong (refl ∙ H' c)
+                    (∼-trans H (λ _ → refl) c) refl-left-neutral
+                      (refl-right-neutral (H c) ⁻¹)))
+    IXV = ≃-comp (Σ-cong (λ - → ≃-sym (≃-funext fe - H)))
+                 (singleton-≃-𝟙 (equiv-to-singleton (Σ-cong (λ - → ＝-flip))
+                 (singleton-types-are-singletons H)))
+
+cocone-identity-characterization : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                                   (f : C → A) (g : C → B) (X : 𝓣  ̇)
+                                 → (u u' : cocone f g X)
+                                 → (u ＝ u') ≃ (cocone-family f g X u u')
+cocone-identity-characterization f g X u u' =
+ (canonical-map-from-identity-to-cocone-family f g X u u' ,
+   Yoneda-Theorem-forth u (canonical-map-from-identity-to-cocone-family f g X u)
+    (cocone-family-is-identity-system f g X u) u')
+
+inverse-cocone-map : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                     (f : C → A) (g : C → B) (X : 𝓣  ̇)
+                   → (u u' : cocone f g X)
+                   → cocone-family f g X u u'
+                   → u ＝ u'
+inverse-cocone-map f g X u u' =
+ ⌜ (cocone-identity-characterization f g X u u') ⌝⁻¹
+
+\end{code}
+
+We need to define the type of morphisms between cocones. We should give a
+characterization of the identity type but fortunately we only need a map in the
+trivial direction.
+
+\begin{code}
+
+cocone-morphism : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}                   
+                  (f : C → A) (g : C → B) (X : 𝓣  ̇) (P : 𝓣'  ̇)
+                → cocone f g P
+                → cocone f g X
+                → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣 ⊔ 𝓣'  ̇
+cocone-morphism f g X P (i , j , H) s'
+ = Σ u ꞉ (P → X) , cocone-family f g X (u ∘ i , u ∘ j , ∼-ap-∘ u H) s'
+
+cocone-morphism-family : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}                   
+                         (f : C → A) (g : C → B) (X : 𝓣  ̇) (P : 𝓣'  ̇)
+                       → (s : cocone f g P)
+                       → (s' : cocone f g X)
+                       → cocone-morphism f g X P s s'
+                       → cocone-morphism f g X P s s'
+                       → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣 ⊔ 𝓣'  ̇
+cocone-morphism-family {_} {_} {_} {_} {_} {A} {B} {C} f g X P
+ (i , j , H) (i' , j' , H') (u , K , L , M) (u' , K' , L' , M')
+ = Σ θ ꞉ ((x : P) → u x ＝ u' x) , Σ ϕl ꞉ ((a : A) → θ (i a) ∙ K' a ＝ K a) ,
+   Σ ϕr ꞉ ((b : B) → θ (j b) ∙ L' b ＝ L b) , ((c : C) → M c ＝ Γ θ ϕl ϕr c)
+ where
+  Γ : (θ : (x : P) → u x ＝ u' x)
+      (ϕl : (a : A) → θ (i a) ∙ K' a ＝ K a)
+      (ϕr : (b : B) → θ (j b) ∙ L' b ＝ L b)
+      (c : C)
+    → K (f c) ∙ H' c ＝ ap u (H c) ∙ L (g c)
+  Γ θ ϕl ϕr c = K (f c) ∙ H' c                         ＝⟨ I ⟩
+                (θ (i (f c)) ∙ K' (f c)) ∙ H' c        ＝⟨ II ⟩
+                θ (i (f c)) ∙ (K' (f c) ∙ H' c)        ＝⟨ III ⟩
+                θ (i (f c)) ∙ (ap u' (H c) ∙ L' (g c)) ＝⟨ IV ⟩
+                (θ (i (f c)) ∙ ap u' (H c)) ∙ L' (g c) ＝⟨ V ⟩
+                (ap u (H c) ∙ θ (j (g c))) ∙ L' (g c)  ＝⟨ VI ⟩
+                ap u (H c) ∙ (θ (j (g c)) ∙ L' (g c))  ＝⟨ VII ⟩
+                ap u (H c) ∙ L (g c)                   ∎
+   where
+    I = ap (_∙ H' c) (ϕl (f c) ⁻¹)
+    II = ∙assoc (θ (i (f c))) (K' (f c)) (H' c)
+    III = ap (θ (i (f c)) ∙_) (M' c)
+    IV = ∙assoc (θ (i (f c))) (ap u' (H c)) (L' (g c)) ⁻¹
+    V = ap (_∙ L' (g c)) (homotopies-are-natural u u' θ)
+    VI = ∙assoc (ap u (H c)) (θ (j (g c))) (L' (g c))
+    VII = ap (ap u (H c) ∙_) (ϕr (g c))
+
+canonical-map-to-cocone-morphism-family
+ : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}                   
+   (f : C → A) (g : C → B) (X : 𝓣  ̇) (P : 𝓣'  ̇)
+ → (s : cocone f g P)
+ → (s' : cocone f g X)
+ → (m : cocone-morphism f g X P s s')
+ → (m' : cocone-morphism f g X P s s')
+ → m ＝ m'
+ → cocone-morphism-family f g X P s s' m m'
+canonical-map-to-cocone-morphism-family {_} {_} {_} {_} {_} {A} {B} {C}
+ f g X P (i , j , H) (i' , j' , H') (u , K , L , M) .(u , K , L , M) refl
+ = (∼-refl , (λ - → refl-left-neutral) , (λ - → refl-left-neutral) , λ c → I c ⁻¹)
+ where
+  I : (c : C)
+    → ap (_∙ H' c) (refl-left-neutral ⁻¹)
+      ∙ ∙assoc (∼-refl (i (f c))) (K (f c)) (H' c)
+      ∙ ap (∼-refl (i (f c)) ∙_) (M c)
+      ∙ ∙assoc (∼-refl (i (f c))) (ap u (H c)) (L (g c)) ⁻¹
+      ∙ ap (_∙ L (g c)) (homotopies-are-natural u u ∼-refl)
+      ∙ ∙assoc (ap u (H c)) (∼-refl (j (g c))) (L (g c))
+      ∙ ap (ap u (H c) ∙_) (refl-left-neutral) ＝ M c
+  I c = ap (_∙ H' c) (refl-left-neutral ⁻¹)
+       ∙ ∙assoc (∼-refl (i (f c))) (K (f c)) (H' c)
+       ∙ ap (∼-refl (i (f c)) ∙_) (M c)
+       ∙ ∙assoc (∼-refl (i (f c))) (ap u (H c)) (L (g c)) ⁻¹
+       ∙ ap (_∙ L (g c)) (homotopies-are-natural u u ∼-refl)
+       ∙ ∙assoc (ap u (H c)) (∼-refl (j (g c))) (L (g c))
+       ∙ ap (ap u (H c) ∙_) (refl-left-neutral)                ＝⟨ ap {!!} II ⟩
+       refl-left-neutral ⁻¹
+       ∙ ap (∼-refl (i (f c)) ∙_) (M c)
+       ∙ ∙assoc (∼-refl (i (f c))) (ap u (H c)) (L (g c)) ⁻¹
+       ∙ ap (_∙ L (g c)) (homotopies-are-natural u u ∼-refl)
+       ∙ ∙assoc (ap u (H c)) (∼-refl (j (g c))) (L (g c))
+       ∙ ap (ap u (H c) ∙_) (refl-left-neutral)                ＝⟨ {!!} ⟩
+       {!!}
+   where
+    II : {Y : 𝓤  ̇} {x y z : Y} {p : x ＝ y} {q : y ＝ z}
+       → ap (_∙ q) (refl-left-neutral ⁻¹) ∙ ∙assoc refl p q ＝ refl-left-neutral ⁻¹
+    II {𝓤} {Y} {x} {y} {z} {refl} {refl} = refl
+    III : {Y : 𝓤  ̇} {x y z : Y} {p : x ＝ y} {q : y ＝ z}
+        → ∙assoc p refl q ∙ ap (p ∙_) (refl-left-neutral) ＝ ap (_∙ q) (refl)
+    III {𝓤} {Y} {x} {y} {z} {refl} {refl} = refl
+
+\end{code}
+
+We also introduce the notion of a dependent cocone.
+
+TODO. Characterize the identity type of dependent cocones.
+
+\begin{code}
+
+dependent-cocone : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
+                   (f : C → A) (g : C → B) (X : 𝓣  ̇)
+                   (t : cocone f g X) (P : X → 𝓣'  ̇)
+                 → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣'  ̇
+dependent-cocone {_} {_} {_} {_} {_} {A} {B} {C} f g X (i , j , H) P =
+ Σ i' ꞉ ((a : A) → P (i a)) , Σ j' ꞉ ((b : B) → P (j b)) ,
+  ((c : C) → transport P (H c) (i' (f c)) ＝ j' (g c))
+
+\end{code}
diff --git a/source/UF/Pushouts.lagda b/source/UF/Pushouts.lagda
index 6677de151..590559e03 100644
--- a/source/UF/Pushouts.lagda
+++ b/source/UF/Pushouts.lagda
@@ -14,6 +14,7 @@ module UF.Pushouts (fe : Fun-Ext) where
 
 open import MLTT.Spartan
 open import UF.Base
+open import UF.CoconesofSpans fe
 open import UF.Equiv
 open import UF.EquivalenceExamples
 open import UF.PropIndexedPiSigma
@@ -23,147 +24,6 @@ open import UF.Yoneda
 
 \end{code}
 
-We start by defining cocones and characerizing their identity type.
-
-\begin{code}
-
-cocone : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
-         (f : C → A) (g : C → B) (X : 𝓣  ̇)
-       → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
-cocone {𝓤} {𝓥} {𝓦} {𝓣} {A} {B} {C} f g X =
- Σ i ꞉ (A → X) , Σ j ꞉ (B → X) , (i ∘ f ∼ j ∘ g)
-
-cocone-vertical-map : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
-                      (f : C → A) (g : C → B) (X : 𝓣  ̇)
-                    → cocone f g X
-                    → (A → X)
-cocone-vertical-map f g X (i , j , K) = i
-
-cocone-horizontal-map : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
-                        (f : C → A) (g : C → B) (X : 𝓣  ̇)
-                      → cocone f g X
-                      → (B → X)
-cocone-horizontal-map f g X (i , j , K) = j
-
-cocone-commuting-square : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
-                          (f : C → A) (g : C → B) (X : 𝓣  ̇)
-                        → ((i , j , K) : cocone f g X)
-                        → i ∘ f ∼ j ∘ g
-cocone-commuting-square f g X (i , j , K) = K
-
-cocone-family : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
-                (f : C → A) (g : C → B) (X : 𝓣  ̇)
-              → cocone f g X → cocone f g X → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣  ̇
-cocone-family f g X (i , j , H) (i' , j' , H') =
- Σ K ꞉ i ∼ i' , Σ L ꞉ j ∼ j' ,
-  ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g)
-
-canonical-map-from-identity-to-cocone-family
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
-   (f : C → A) (g : C → B) (X : 𝓣  ̇)
- → (u u' : cocone f g X)
- → u ＝ u'
- → cocone-family f g X u u'
-canonical-map-from-identity-to-cocone-family
- f g X (i , j , H) .(i , j , H) refl =
- (∼-refl , ∼-refl , λ - → refl-left-neutral)
-
-cocone-family-is-identity-system
- : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
-   (f : C → A) (g : C → B) (X : 𝓣  ̇)
- → (x : cocone f g X)
- → is-contr (Σ y ꞉ cocone f g X , cocone-family f g X x y)
-cocone-family-is-identity-system {_} {_} {_} {𝓣} {A} {B} {C} f g X (i , j , H) =
- equiv-to-singleton e 𝟙-is-singleton
- where
-  e : (Σ y ꞉ cocone f g X , cocone-family f g X (i , j , H) y) ≃ 𝟙 { 𝓣 }
-  e = (Σ y ꞉ cocone f g X , cocone-family f g X (i , j , H) y) ≃⟨ I ⟩
-      (Σ i' ꞉ (A → X) , Σ j' ꞉ (B → X) ,
-        Σ H' ꞉ (i' ∘ f ∼ j' ∘ g) ,
-         Σ K ꞉ i ∼ i' , Σ L ꞉ j ∼ j' ,
-          ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g))              ≃⟨ II ⟩
-      (Σ i' ꞉ (A → X) , Σ K ꞉ i ∼ i' ,
-        Σ j' ꞉ (B → X) , Σ L ꞉ j ∼ j' ,
-         Σ H' ꞉ (i' ∘ f ∼ j' ∘ g) ,
-          ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g))              ≃⟨ VII ⟩
-      (Σ H' ꞉ (i ∘ f ∼ j ∘ g) , H' ∼ H)                        ≃⟨ IXV ⟩
-      𝟙                                                        ■
-   where
-    I = ≃-comp Σ-assoc (Σ-cong (λ i' → Σ-assoc))
-    II = Σ-cong (λ _ → ≃-comp (Σ-cong
-          (λ _ → ≃-comp Σ-flip (Σ-cong (λ K → Σ-flip)))) Σ-flip)
-    III = (Σ i' ꞉ (A → X) , i ∼ i')  ≃⟨ IV ⟩
-          (Σ i' ꞉ (A → X) , i ＝ i') ≃⟨ V ⟩
-          𝟙                          ■
-     where
-      IV = Σ-cong (λ - → ≃-sym (≃-funext fe i -))
-      V = singleton-≃-𝟙 (singleton-types-are-singletons i)
-    VI = ≃-comp (Σ-cong (λ - → ≃-sym (≃-funext fe j -)))
-                (singleton-≃-𝟙 (singleton-types-are-singletons j))
-    VII = (Σ i' ꞉ (A → X) , Σ K ꞉ i ∼ i' ,
-            Σ j' ꞉ (B → X) , Σ L ꞉ j ∼ j' ,
-             Σ H' ꞉ (i' ∘ f ∼ j' ∘ g) ,
-              ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g))           ≃⟨ IIIV ⟩
-          (Σ (i' , K) ꞉ (Σ i' ꞉ (A → X) , i ∼ i') ,
-            Σ j' ꞉ (B → X) , Σ L ꞉ j ∼ j' ,
-             Σ H' ꞉ (i' ∘ f ∼ j' ∘ g) ,
-              ∼-trans (K ∘ f) H' ∼ ∼-trans H (L ∘ g))           ≃⟨ IX ⟩
-           (Σ j' ꞉ (B → X) , Σ L ꞉ j ∼ j' ,
-             Σ H' ꞉ (i ∘ f ∼ j' ∘ g) ,
-              ∼-trans (∼-refl ∘ f) H' ∼ ∼-trans H (L ∘ g))      ≃⟨ XI ⟩
-           (Σ (j' , L) ꞉ (Σ j' ꞉ (B → X) , j ∼ j') ,
-             Σ H' ꞉ (i ∘ f ∼ j' ∘ g) ,
-              ∼-trans (∼-refl ∘ f) H' ∼ ∼-trans H (L ∘ g))      ≃⟨ XII ⟩
-           (Σ H' ꞉ (i ∘ f ∼ j ∘ g) ,
-             ∼-trans (∼-refl ∘ f) H' ∼ ∼-trans H (∼-refl ∘ g))  ≃⟨ XIII ⟩
-           (Σ H' ꞉ (i ∘ f ∼ j ∘ g) , H' ∼ H)                    ■
-     where
-      IIIV = ≃-sym Σ-assoc
-      IX = prop-indexed-sum (equiv-to-prop III 𝟙-is-prop) (i , ∼-refl)
-      XI = ≃-sym Σ-assoc
-      XII = prop-indexed-sum (equiv-to-prop VI 𝟙-is-prop) (j , ∼-refl)
-      XIII = Σ-cong (λ H' → Π-cong fe fe (λ c → ＝-cong (refl ∙ H' c)
-                    (∼-trans H (λ _ → refl) c) refl-left-neutral
-                      (refl-right-neutral (H c) ⁻¹)))
-    IXV = ≃-comp (Σ-cong (λ - → ≃-sym (≃-funext fe - H)))
-                 (singleton-≃-𝟙 (equiv-to-singleton (Σ-cong (λ - → ＝-flip))
-                 (singleton-types-are-singletons H)))
-
-cocone-identity-characterization : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
-                                   (f : C → A) (g : C → B) (X : 𝓣  ̇)
-                                 → (u u' : cocone f g X)
-                                 → (u ＝ u') ≃ (cocone-family f g X u u')
-cocone-identity-characterization f g X u u' =
- (canonical-map-from-identity-to-cocone-family f g X u u' ,
-   Yoneda-Theorem-forth u (canonical-map-from-identity-to-cocone-family f g X u)
-    (cocone-family-is-identity-system f g X u) u')
-
-inverse-cocone-map : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
-                     (f : C → A) (g : C → B) (X : 𝓣  ̇)
-                   → (u u' : cocone f g X)
-                   → cocone-family f g X u u'
-                   → u ＝ u'
-inverse-cocone-map f g X u u' =
- ⌜ (cocone-identity-characterization f g X u u') ⌝⁻¹
-
-\end{code}
-
-We also introduce the notion of a dependent cocone.
-
-TODO. Characterize the identity type of dependent cocones.
-
-\begin{code}
-
-dependent-cocone : {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇}
-                   (f : C → A) (g : C → B) (X : 𝓣  ̇)
-                   (t : cocone f g X) (P : X → 𝓣'  ̇)
-                 → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣'  ̇
-dependent-cocone {_} {_} {_} {_} {_} {A} {B} {C} f g X (i , j , H) P =
- Σ i' ꞉ ((a : A) → P (i a)) , Σ j' ꞉ ((b : B) → P (j b)) ,
-  ((c : C) → transport P (H c) (i' (f c)) ＝ j' (g c))
-
-\end{code}
-
 Now we will define the universal property, induction principle and propositional
 computation rules for pushouts and show they are inter-derivable.
 
@@ -264,7 +124,7 @@ Pushout-Computation-Rule₃
 Now we will use a record type to give the pushout, point and path constructors,
 and the dependent universal property.
 
-begin{code}
+\begin{code}
 
 record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A) (g : C → B) : 𝓤ω
  where
@@ -289,7 +149,7 @@ record pushouts-exist {A : 𝓤  ̇} {B : 𝓥  ̇} {C : 𝓦  ̇} (f : C → A)
    → Pushout-Computation-Rule₃ pushout f g (inll , inrr , glue) P
       pushout-induction pushout-ind-comp-inll pushout-ind-comp-inrr
 
-end{code}
+\end{code}
 
 We will observe that the pushout is a cocone and begin deriving some key
 results from the induction principles:
@@ -303,7 +163,7 @@ The following are logically equivalent
    uniqueness principle
 3) The universal property.
 
-begin{code}
+\begin{code}
 
  pushout-cocone : cocone f g pushout
  pushout-cocone = (inll , inrr , glue)
@@ -433,7 +293,7 @@ begin{code}
      (pushout-rec-comp-inll l r G , pushout-rec-comp-inrr l r G ,
       ∼-sym (pushout-rec-comp-glue l r G))
    
-end{code}
+\end{code}
 
 We investigate only postulating the (non-dependent) universal property.
 
@@ -583,6 +443,19 @@ computation rules and the uniqueness principles.
      (u , H , H' , λ c → M c ⁻¹)
       (u' , ∼-refl , ∼-refl , λ c → refl-left-neutral))))
 
+ pushout-uniqueness-inll : {X : 𝓣 ̇}
+                         → (u u' : pushout → X)
+                         → (H : (a : A) → u (inll a) ＝ u' (inll a))
+                         → (H' : (b : B) → u (inrr b) ＝ u' (inrr b))
+                         → (M : (c : C)
+                           → ap u (glue c) ∙ H' (g c) ＝ H (f c) ∙ ap u' (glue c))
+                         → (l : A → X)
+                         → (L : (a : A) → u (inll a) ＝ l a)
+                         → (L' : (a : A) → u' (inll a) ＝ l a)
+                         → (a : A)
+                         → pushout-uniqueness u u' H H' M (inll a) ∙ L' a ＝ L a
+ pushout-uniqueness-inll u u' H H' M l L L' a = {!!}
+                    
 \end{code}
 
 Finally, we can derive the induction principle and the corresponding propositional
@@ -742,13 +615,67 @@ call pre-induction.
    → transport P (pre-induction-id-is-id l r G (inll a))
                  (pre-induction-family l r G (inll a))
    ＝ l a
-  pre-induction-family-comp-inll l r G a
-   = {!!}
+  pre-induction-family-comp-inll {_} {P} l r G a
+   = transport (λ - → transport P - (pre-induction-family l r G (inll a)) ＝ l a)
+               (I a ⁻¹) (from-Σ-＝' (pre-induction-comp-inll l r G a))
    where
     I : (a : A)
       → pre-induction-id-is-id l r G (inll a)
       ＝ ap pr₁ (pre-induction-comp-inll l r G a)
-    I a = {!pushout-rec-comp-inll!}
+    I = pushout-uniqueness-inll (pre-induction-id l r G) id
+         (λ a → ap pr₁ (pre-induction-comp-inll l r G a))
+          (λ b → ap pr₁ (pre-induction-comp-inrr l r G b))
+           II inll (λ a → ap pr₁ (pre-induction-comp-inll l r G a)) ∼-refl
+     where
+      II : (c : C)
+         → ap (pre-induction-id l r G) (glue c)
+          ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))
+         ＝ ap pr₁ (pre-induction-comp-inll l r G (f c)) ∙ ap id (glue c)
+      II c = ap (pre-induction-id l r G) (glue c)
+            ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))            ＝⟨ III ⟩
+             ap pr₁ (ap (pre-induction l r G) (glue c))
+            ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))            ＝⟨ IV ⟩
+             ap pr₁ (ap (pre-induction l r G) (glue c)
+            ∙ pre-induction-comp-inrr l r G (g c))                    ＝⟨ V ⟩
+             ap pr₁ (pre-induction-comp-inll l r G (f c)
+            ∙ to-Σ-＝ (glue c , G c))                                 ＝⟨ VI ⟩
+             ap pr₁ (pre-induction-comp-inll l r G (f c))
+            ∙ ap pr₁ (to-Σ-＝ (glue c , G c))                         ＝⟨ VIII ⟩
+             ap pr₁ (pre-induction-comp-inll l r G (f c))
+            ∙ ap id (glue c)                                          ∎
+       where
+        III : ap (pre-induction-id l r G) (glue c)
+             ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))
+            ＝ ap pr₁ (ap (pre-induction l r G) (glue c))
+             ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c)) 
+        III = ap (_∙ ap pr₁ (pre-induction-comp-inrr l r G (g c)))
+                 (ap-ap (pre-induction l r G) pr₁ (glue c) ⁻¹)
+        IV : ap pr₁ (ap (pre-induction l r G) (glue c))
+             ∙ ap pr₁ (pre-induction-comp-inrr l r G (g c))
+            ＝ ap pr₁ (ap (pre-induction l r G) (glue c)
+             ∙ pre-induction-comp-inrr l r G (g c))
+        IV = ap-∙ pr₁ (ap (pre-induction l r G) (glue c))
+                      (pre-induction-comp-inrr l r G (g c)) ⁻¹
+        V : ap pr₁ (ap (pre-induction l r G) (glue c)
+           ∙ pre-induction-comp-inrr l r G (g c))
+          ＝ ap pr₁ (pre-induction-comp-inll l r G (f c)
+           ∙ to-Σ-＝ (glue c , G c))  
+        V = ap (ap pr₁) (pre-induction-comp-glue l r G c)
+        VI : ap pr₁ (pre-induction-comp-inll l r G (f c)
+            ∙ to-Σ-＝ (glue c , G c))
+           ＝ ap pr₁ (pre-induction-comp-inll l r G (f c))
+            ∙ ap pr₁ (to-Σ-＝ (glue c , G c)) 
+        VI = ap-∙ pr₁ (pre-induction-comp-inll l r G (f c))
+                      (to-Σ-＝ (glue c , G c))
+        VII : ap pr₁ (to-Σ-＝ (glue c , G c)) ＝ ap id (glue c) 
+        VII = ap pr₁ (to-Σ-＝ (glue c , G c)) ＝⟨ ap-pr₁-to-Σ-＝ (glue c , G c) ⟩
+              glue c                          ＝⟨ ap-id-is-id' (glue c) ⟩
+              ap id (glue c)                  ∎
+        VIII : ap pr₁ (pre-induction-comp-inll l r G (f c))
+              ∙ ap pr₁ (to-Σ-＝ (glue c , G c))
+             ＝ ap pr₁ (pre-induction-comp-inll l r G (f c))
+              ∙ ap id (glue c)   
+        VIII = ap (ap pr₁ (pre-induction-comp-inll l r G (f c)) ∙_) VII 
 
 \end{code}
 

From 6464833eefdfc8b68db611c091b8749c837b7fec Mon Sep 17 00:00:00 2001
From: Ian Ray <ibray1115@gmail.com>
Date: Sat, 8 Feb 2025 19:04:39 -0500
Subject: [PATCH 18/18] Update... still need to fix unresolved contraints.

---
 source/UF/CoconesofSpans.lagda | 51 ++++++++++++++--------------------
 1 file changed, 21 insertions(+), 30 deletions(-)

diff --git a/source/UF/CoconesofSpans.lagda b/source/UF/CoconesofSpans.lagda
index b2b1a5baf..b7f0c3635 100644
--- a/source/UF/CoconesofSpans.lagda
+++ b/source/UF/CoconesofSpans.lagda
@@ -206,37 +206,28 @@ canonical-map-to-cocone-morphism-family
  → cocone-morphism-family f g X P s s' m m'
 canonical-map-to-cocone-morphism-family {_} {_} {_} {_} {_} {A} {B} {C}
  f g X P (i , j , H) (i' , j' , H') (u , K , L , M) .(u , K , L , M) refl
- = (∼-refl , (λ - → refl-left-neutral) , (λ - → refl-left-neutral) , λ c → I c ⁻¹)
+ = (∼-refl , (λ - → refl-left-neutral) , (λ - → refl-left-neutral) , II)
  where
-  I : (c : C)
-    → ap (_∙ H' c) (refl-left-neutral ⁻¹)
-      ∙ ∙assoc (∼-refl (i (f c))) (K (f c)) (H' c)
-      ∙ ap (∼-refl (i (f c)) ∙_) (M c)
-      ∙ ∙assoc (∼-refl (i (f c))) (ap u (H c)) (L (g c)) ⁻¹
-      ∙ ap (_∙ L (g c)) (homotopies-are-natural u u ∼-refl)
-      ∙ ∙assoc (ap u (H c)) (∼-refl (j (g c))) (L (g c))
-      ∙ ap (ap u (H c) ∙_) (refl-left-neutral) ＝ M c
-  I c = ap (_∙ H' c) (refl-left-neutral ⁻¹)
-       ∙ ∙assoc (∼-refl (i (f c))) (K (f c)) (H' c)
-       ∙ ap (∼-refl (i (f c)) ∙_) (M c)
-       ∙ ∙assoc (∼-refl (i (f c))) (ap u (H c)) (L (g c)) ⁻¹
-       ∙ ap (_∙ L (g c)) (homotopies-are-natural u u ∼-refl)
-       ∙ ∙assoc (ap u (H c)) (∼-refl (j (g c))) (L (g c))
-       ∙ ap (ap u (H c) ∙_) (refl-left-neutral)                ＝⟨ ap {!!} II ⟩
-       refl-left-neutral ⁻¹
-       ∙ ap (∼-refl (i (f c)) ∙_) (M c)
-       ∙ ∙assoc (∼-refl (i (f c))) (ap u (H c)) (L (g c)) ⁻¹
-       ∙ ap (_∙ L (g c)) (homotopies-are-natural u u ∼-refl)
-       ∙ ∙assoc (ap u (H c)) (∼-refl (j (g c))) (L (g c))
-       ∙ ap (ap u (H c) ∙_) (refl-left-neutral)                ＝⟨ {!!} ⟩
-       {!!}
-   where
-    II : {Y : 𝓤  ̇} {x y z : Y} {p : x ＝ y} {q : y ＝ z}
-       → ap (_∙ q) (refl-left-neutral ⁻¹) ∙ ∙assoc refl p q ＝ refl-left-neutral ⁻¹
-    II {𝓤} {Y} {x} {y} {z} {refl} {refl} = refl
-    III : {Y : 𝓤  ̇} {x y z : Y} {p : x ＝ y} {q : y ＝ z}
-        → ∙assoc p refl q ∙ ap (p ∙_) (refl-left-neutral) ＝ ap (_∙ q) (refl)
-    III {𝓤} {Y} {x} {y} {z} {refl} {refl} = refl
+  I : {Y : 𝓤  ̇} {Z : 𝓥  ̇} {x y : Y} {z' z : Z} {f' : Y → Z}
+      {p : x ＝ y} {q : f' y ＝ z} {p' : f' x ＝ z'} {q' : z' ＝ z}
+      {α : p' ∙ q' ＝ (ap f' p) ∙ q}
+    → α ＝ ap (_∙ q') (refl-left-neutral ⁻¹)
+          ∙ ∙assoc refl p' q'
+          ∙ ap (refl ∙_) α
+          ∙ ∙assoc refl (ap f' p) q ⁻¹
+          ∙ ap (_∙ q) (homotopies-are-natural f' f' ∼-refl)
+          ∙ ∙assoc (ap f' p) refl q
+          ∙ ap (ap f' p ∙_) (refl-left-neutral) 
+  I {𝓤} {𝓥} {Y} {Z} {x} {y} {z'} {z} {f'} {refl} {refl} {refl} {q'} {α} = refl
+  II : (c : C)
+     →  M c ＝ ap (_∙ H' c) (refl-left-neutral ⁻¹)
+              ∙ ∙assoc (∼-refl (i (f c))) (K (f c)) (H' c)
+              ∙ ap (∼-refl (i (f c)) ∙_) (M c)
+              ∙ ∙assoc (∼-refl (i (f c))) (ap u (H c)) (L (g c)) ⁻¹
+              ∙ ap (_∙ L (g c)) (homotopies-are-natural u u ∼-refl)
+              ∙ ∙assoc (ap u (H c)) (∼-refl (j (g c))) (L (g c))
+              ∙ ap (ap u (H c) ∙_) (refl-left-neutral)
+  II c = I
 
 \end{code}