From 0008acedb634a5fd83459ef218897fac07778650 Mon Sep 17 00:00:00 2001
From: jake-87 <jakehfreebsd@gmail.com>
Date: Sat, 27 Jul 2024 16:52:38 +1000
Subject: [PATCH 01/10] Added homotopy pushouts

---
 src/HoTT.lagda.md             |  16 +++
 src/Homotopy/Pushout.lagda.md | 252 ++++++++++++++++++++++++++++++++++
 2 files changed, 268 insertions(+)
 create mode 100644 src/Homotopy/Pushout.lagda.md

diff --git a/src/HoTT.lagda.md b/src/HoTT.lagda.md
index 8e4b5420f..b8a3b2d49 100644
--- a/src/HoTT.lagda.md
+++ b/src/HoTT.lagda.md
@@ -58,6 +58,7 @@ open import Homotopy.Space.Circle
 open import Homotopy.Space.Sphere
 open import Homotopy.Space.Torus
 open import Homotopy.Truncation
+open import Homotopy.Pushout
 open import Homotopy.Wedge
 open import Homotopy.Base
 
@@ -604,6 +605,21 @@ _ = T²
 
 * The torus: `T²`{.Agda}.
 
+### 6.8: Pushouts
+<!--
+```agda
+_ = Pushout
+_ = cocone
+_ = Susp≡Pushout-⊤←A→⊤
+_ = Pushout→E≡coconeE 
+```
+-->
+
+* The pushout: `Pushout`{.Agda}
+* Definition 6.8.1: `cocone`{.Agda}
+* Lemma 6.8.2: `Pushout→E≡coconeE`{.Agda}
+* Observation: `Susp≡Pushout-⊤←A→⊤`{.Agda}
+
 ### 6.9: Truncations
 
 <!--
diff --git a/src/Homotopy/Pushout.lagda.md b/src/Homotopy/Pushout.lagda.md
new file mode 100644
index 000000000..413840539
--- /dev/null
+++ b/src/Homotopy/Pushout.lagda.md
@@ -0,0 +1,252 @@
+<!--
+```agda
+open import 1Lab.Prelude
+
+open import Homotopy.Space.Suspension
+```
+-->
+
+
+```agda
+module Homotopy.Pushout where
+```
+
+# Pushouts {defines="pushout"}
+
+Given the following span:
+
+~~~{.quiver}
+\begin{tikzpicture}
+\node[] (c) at (0, 0) {$C$};
+\node[] (a) at (0, -2) {$A$};
+\node[] (b) at (2, 0) {$B$};
+\draw[->] (c) -- (a) node[midway,xshift=-10]{${f}$};
+\draw[->] (c) -- (b) node[midway,above]{${g}$};
+\end{tikzpicture}
+~~~
+
+The `Pushout`{.Agda} of this span is defined as the higher inductive type
+presented by:
+```agda
+data Pushout {ℓ} (C : Type ℓ)
+                 (A : Type ℓ) (f : C → A)
+                 (B : Type ℓ) (g : C → B)
+                 : Type ℓ where
+```
+
+Two functions `inl`{.Agda} and `inr`{.Agda}, that "connect" from `A` and `B`:
+
+```agda
+  inl : A → Pushout C A f B g
+  inr : B → Pushout C A f B g
+```
+
+And, for every `c : C`, a path
+`commutes : inl (f c) ≡ inr (g c)`{.Agda}:
+
+```agda
+  commutes : ∀ c → inl (f c) ≡ inr (g c)
+```
+
+These combine to give the following:
+
+~~~{.quiver}
+\begin{tikzpicture}
+\node[] (c) at (0, 0) {$C$};
+\node[] (a) at (0, -2) {$A$};
+\node[] (b) at (2, 0) {$B$};
+\node[] (d) at (2, -2) {$Push$};
+\draw[->] (c) -- (a) node[midway,xshift=-10]{${f}$};
+\draw[->] (c) -- (b) node[midway,above]{${g}$};
+\draw[->] (a) -- (d) node[midway,below]{$inl$};
+\draw[->] (b) -- (d) node[midway,right]{$inr$};
+
+\draw[->,shorten <=0.2cm,shorten >=0.2cm,very thick] (a) -- (b) node[midway,above left]{$h$};
+\end{tikzpicture}
+~~~
+where $h$ is our path `commutes`{.Agda}, and $Push$ our Pushout. [^comm].
+
+[^comm]: Big words, small diagram.
+
+## Suspensions as Pushouts
+
+First, recall the `Susp`{.Agda}, which serves to increase the
+connectedness of a space. Suspension can be expressed as a
+`Pushout`{.Agda} of some type
+$A$, alongside two instaces of $⊤$; i.e., the span `⊤ ← A → ⊤`{.Agda}
+or the following:
+
+~~~{.quiver}
+\begin{tikzpicture}
+\node[] (c) at (0, 0) {$C$};
+\node[] (a) at (0, -2) {$\top$};
+\node[] (b) at (2, 0) {$\top$};
+\draw[->] (c) -- (a) node[midway,xshift=-15]{$\rm{con}$};
+\draw[->] (c) -- (b) node[midway,above]{$\rm{con}$};
+\end{tikzpicture}
+~~~
+
+where 
+
+```agda
+to-top : {A : Type} → A → ⊤
+to-top _ = tt
+```
+There is only one element of `⊤`{.Agda}, and hence only one choice
+for the function projecting into `⊤`{.Agda}.
+
+If one considers the structure we're creating, it becomes very
+obvious that this is equivalent to suspension - we take our
+`inl`{.Agda} and `inr`{.Agda} constructors to `N`{.Agda} and
+`S`{.Agda}, as the input into them is now `⊤`{.Agda}, which only
+has one element anyway. Likewise, we turn `commutes`{.Agda} into
+`merid`{.Agda}, as our functions `f`{.Agda} and `g`{.Agda} can only
+be `con`{.Agda}, so it reduces (with a suitable element of `C`{.Agda})
+from `∀ c → inl (f c) ≡ inr (g c)`{.Agda} to `inl tt ≡ inr tt`{.Agda}, or
+by funext, `inl ≡ inr`{.Agda}.
+
+We therefore aim to show:
+
+```agda
+Susp≡Pushout-⊤←A→⊤ : ∀ {A} → Susp A ≡ Pushout A ⊤ to-top ⊤ to-top
+```
+
+The left and right functions are very simple:
+
+```agda
+Susp→Pushout-⊤←A→⊤ : ∀ {A} → Susp A → Pushout A ⊤ to-top ⊤ to-top
+Susp→Pushout-⊤←A→⊤ N = inl tt
+Susp→Pushout-⊤←A→⊤ S = inr tt
+Susp→Pushout-⊤←A→⊤ (merid x i) = commutes x i
+
+Pushout-⊤←A→⊤→Susp : ∀ {A} → Pushout A ⊤ to-top ⊤ to-top → Susp A
+Pushout-⊤←A→⊤→Susp (inl x) = N
+Pushout-⊤←A→⊤→Susp (inr x) = S
+Pushout-⊤←A→⊤→Susp (commutes c i) = merid c i
+```
+
+We then have:
+
+```agda
+Susp≡Pushout-⊤←A→⊤ = ua (Susp→Pushout-⊤←A→⊤ , is-iso→is-equiv iso-pf) where
+```
+
+<details><summary> We then verify that our two functions above are in fact
+an equivalence. This is entirely `refl`{.Agda}, due to the noted
+similarities in structure.</summary>
+```agda
+  open is-iso
+
+  iso-pf : is-iso Susp→Pushout-⊤←A→⊤
+  iso-pf .inv = Pushout-⊤←A→⊤→Susp
+  iso-pf .rinv (inl x) = refl
+  iso-pf .rinv (inr x) = refl
+  iso-pf .rinv (commutes c i) = refl
+  iso-pf .linv N = refl
+  iso-pf .linv S = refl
+  iso-pf .linv (merid x i) = refl
+```
+</details>
+
+## The Universal property of a pushout
+
+We can also formulate the universal property of a pushout. We first
+do this by introducing the `cocone`{.Adga}. A `cocone`{.Agda},
+given a type `D`{.Agda} and a span $\mathcal{D}$:
+
+~~~{.quiver}
+\begin{tikzpicture}
+\node[] (c) at (2, 0) {$C$};
+\node[] (a) at (0, 0) {$A$};
+\node[] (b) at (4, 0) {$B$};
+\draw[->] (c) -- (a) node[midway,above]{${f}$};
+\draw[->] (c) -- (b) node[midway,above]{${g}$};
+\end{tikzpicture}
+~~~
+
+consists of functions:
+<!--
+```agda
+module _ (A B C D : Type) (f : C → A) (g : C → B)
+  (i' : A → D) (j' : B → D) (h' : (c : C) → i' (f c) ≡ j' (g c))
+  where
+```
+-->
+```agda
+  i : A → D
+  j : B → D
+``` 
+and a homotopy
+```agda
+  h : (c : C) → i (f c) ≡ j (g c)
+```
+<!--
+```agda
+  i = i'
+  j = j'
+  h = h'
+```
+-->
+forming:
+
+~~~{.quiver}
+\begin{tikzpicture}
+\node[] (c) at (0, 0) {$C$};
+\node[] (a) at (0, -2) {$A$};
+\node[] (b) at (2, 0) {$B$};
+\node[] (d) at (2, -2) {$D$};
+\draw[->] (c) -- (a) node[midway,xshift=-10]{${f}$};
+\draw[->] (c) -- (b) node[midway,above]{${g}$};
+\draw[->] (a) -- (d) node[midway,below]{$i$};
+\draw[->] (b) -- (d) node[midway,right]{$j$};
+\draw[->,shorten <=0.2cm,shorten >=0.2cm,very thick] (a) -- (b) node[midway,above left]{$h$};
+\end{tikzpicture}
+~~~
+
+One can then note the similarities between this definition,
+and our previous `Pushout`{.Agda} definition. We denote the type of `cocone`{.Agda}s as:
+
+```agda
+cocone : {C A B : Type} → (f : C → A) → (g : C → B) → (D : Type) → Type
+cocone {C} {A} {B} f g D =
+  Σ[ i ∈ (A → D) ]
+    Σ[ j ∈ (B → D) ]
+      ((c : C) → i (f c) ≡ j (g c))
+```
+
+We can then show that the canonical `cocone`{.Agda} consisting of a `Pushout`{.Agda}
+is the universal `cocone`{.Agda}.
+
+```agda
+Pushout→E≡coconeE : ∀ {A B C E f g} →
+                    (Pushout C A f B g → E) ≡ (cocone f g E)
+Pushout→E≡coconeE = ua ( pushout→cocone , is-iso→is-equiv iso-pc ) where
+```
+
+<details><summary> Once again we show that the above is an equivalence;
+this proof is essentially a transcription of Lemma 6.8.2 in the [HoTT](HoTT.html) book,
+and again mostly reduces to `refl`{.Agda}.
+</summary>
+```agda
+  open is-iso
+
+  pushout→cocone : ∀ {A B C E f g} → (Pushout C A f B g → E) → cocone f g E
+  cocone→pushout : ∀ {A B C E f g} → cocone f g E → (Pushout C A f B g → E)
+  iso-pc : is-iso pushout→cocone
+
+  pushout→cocone t = (λ x → t (inl x)) ,
+                     (λ x → t (inr x)) ,
+                     (λ c i → ap t (commutes c) i)
+
+  cocone→pushout t (inl x) = fst t x 
+  cocone→pushout t (inr x) = fst (snd t) x
+  cocone→pushout t (commutes c i) = snd (snd t) c i
+
+  iso-pc .inv = cocone→pushout
+  iso-pc .rinv _ = refl
+  iso-pc .linv _ = funext (λ { (inl y) → refl;
+                                (inr y) → refl;
+                                (commutes c i) → refl
+                           })
+```
+</details>

From eeaa5f09f9d5fcecfd6a95c208b67c8866d9148d Mon Sep 17 00:00:00 2001
From: jake-87 <jakehfreebsd@gmail.com>
Date: Sat, 27 Jul 2024 19:27:17 +1000
Subject: [PATCH 02/10] Better diagrams, fixed some prose

---
 src/HoTT.lagda.md             |   8 +-
 src/Homotopy/Pushout.lagda.md | 183 +++++++++++++++++-----------------
 2 files changed, 94 insertions(+), 97 deletions(-)

diff --git a/src/HoTT.lagda.md b/src/HoTT.lagda.md
index b8a3b2d49..000b27dee 100644
--- a/src/HoTT.lagda.md
+++ b/src/HoTT.lagda.md
@@ -609,15 +609,15 @@ _ = T²
 <!--
 ```agda
 _ = Pushout
-_ = cocone
+_ = Cocone
+_ = Pushout→E≡CoconeE
 _ = Susp≡Pushout-⊤←A→⊤
-_ = Pushout→E≡coconeE 
 ```
 -->
 
 * The pushout: `Pushout`{.Agda}
-* Definition 6.8.1: `cocone`{.Agda}
-* Lemma 6.8.2: `Pushout→E≡coconeE`{.Agda}
+* Definition 6.8.1: `Cocone`{.Agda}
+* Lemma 6.8.2: `Pushout→E≡CoconeE`{.Agda}
 * Observation: `Susp≡Pushout-⊤←A→⊤`{.Agda}
 
 ### 6.9: Truncations
diff --git a/src/Homotopy/Pushout.lagda.md b/src/Homotopy/Pushout.lagda.md
index 413840539..cf3274564 100644
--- a/src/Homotopy/Pushout.lagda.md
+++ b/src/Homotopy/Pushout.lagda.md
@@ -11,21 +11,21 @@ open import Homotopy.Space.Suspension
 module Homotopy.Pushout where
 ```
 
-# Pushouts {defines="pushout"}
+# Pushouts {defines="pushout cocone"}
 
 Given the following span:
 
 ~~~{.quiver}
-\begin{tikzpicture}
-\node[] (c) at (0, 0) {$C$};
-\node[] (a) at (0, -2) {$A$};
-\node[] (b) at (2, 0) {$B$};
-\draw[->] (c) -- (a) node[midway,xshift=-10]{${f}$};
-\draw[->] (c) -- (b) node[midway,above]{${g}$};
-\end{tikzpicture}
+\[\begin{tikzcd}
+  C && B \\
+  \\
+  A
+  \arrow["g", from=1-1, to=1-3]
+  \arrow["f"', from=1-1, to=3-1]
+\end{tikzcd}\]
 ~~~
 
-The `Pushout`{.Agda} of this span is defined as the higher inductive type
+The **Pushout** of this span is defined as the higher inductive type
 presented by:
 ```agda
 data Pushout {ℓ} (C : Type ℓ)
@@ -51,81 +51,80 @@ And, for every `c : C`, a path
 These combine to give the following:
 
 ~~~{.quiver}
-\begin{tikzpicture}
-\node[] (c) at (0, 0) {$C$};
-\node[] (a) at (0, -2) {$A$};
-\node[] (b) at (2, 0) {$B$};
-\node[] (d) at (2, -2) {$Push$};
-\draw[->] (c) -- (a) node[midway,xshift=-10]{${f}$};
-\draw[->] (c) -- (b) node[midway,above]{${g}$};
-\draw[->] (a) -- (d) node[midway,below]{$inl$};
-\draw[->] (b) -- (d) node[midway,right]{$inr$};
-
-\draw[->,shorten <=0.2cm,shorten >=0.2cm,very thick] (a) -- (b) node[midway,above left]{$h$};
-\end{tikzpicture}
+\[\begin{tikzcd}
+	C && B \\
+	\\
+	A && {\rm{Pushout}}
+	\arrow["g", from=1-1, to=1-3]
+	\arrow["f"', from=1-1, to=3-1]
+	\arrow["{\rm{inl}}", from=1-3, to=3-3]
+	\arrow["{\rm{commutes}}"{description}, shorten <=6pt, shorten >=6pt, Rightarrow, from=3-1, to=1-3]
+	\arrow["{\rm{inl}}"', from=3-1, to=3-3]
+\end{tikzcd}\]
 ~~~
-where $h$ is our path `commutes`{.Agda}, and $Push$ our Pushout. [^comm].
-
-[^comm]: Big words, small diagram.
 
 ## Suspensions as Pushouts
 
 First, recall the `Susp`{.Agda}, which serves to increase the
 connectedness of a space. Suspension can be expressed as a
-`Pushout`{.Agda} of some type
-$A$, alongside two instaces of $⊤$; i.e., the span `⊤ ← A → ⊤`{.Agda}
-or the following:
+`Pushout`{.Agda} of, for some type `A`, the span `⊤ ← A → ⊤`{.Agda}:
 
 ~~~{.quiver}
-\begin{tikzpicture}
-\node[] (c) at (0, 0) {$C$};
-\node[] (a) at (0, -2) {$\top$};
-\node[] (b) at (2, 0) {$\top$};
-\draw[->] (c) -- (a) node[midway,xshift=-15]{$\rm{con}$};
-\draw[->] (c) -- (b) node[midway,above]{$\rm{con}$};
-\end{tikzpicture}
+\[\begin{tikzcd}
+	C && \top \\
+	\\
+	\top && {\rm{Pushout}}
+	\arrow["{\rm{const\,tt}}", from=1-1, to=1-3]
+	\arrow["{\rm{const\,tt}}"', from=1-1, to=3-1]
+	\arrow["{\rm{inl}}", from=1-3, to=3-3]
+	\arrow["{\rm{commutes}}"{description}, shorten <=6pt, shorten >=6pt, Rightarrow, from=3-1, to=1-3]
+	\arrow["{\rm{inl}}"', from=3-1, to=3-3]
+\end{tikzcd}\]
 ~~~
 
-where 
-
+<!--
 ```agda
-to-top : {A : Type} → A → ⊤
-to-top _ = tt
+const : {A B : Type} → A → B → A
+const t _ = t
 ```
+-->
+
 There is only one element of `⊤`{.Agda}, and hence only one choice
-for the function projecting into `⊤`{.Agda}.
+for the function projecting into `⊤`{.Agda} - `const tt`{.Agda}.
 
 If one considers the structure we're creating, it becomes very
-obvious that this is equivalent to suspension - we take our
-`inl`{.Agda} and `inr`{.Agda} constructors to `N`{.Agda} and
-`S`{.Agda}, as the input into them is now `⊤`{.Agda}, which only
-has one element anyway. Likewise, we turn `commutes`{.Agda} into
+obvious that this is equivalent to suspension - because both of our
+non-path constructors have input `⊤`{.Agda}, they're indistiguishable
+from members of the pushout; therefore, we take the
+`inl`{.Agda} and `inr`{.Agda} to `N`{.Agda} and
+`S`{.Agda} respectively.
+Likewise, we turn `commutes`{.Agda} into
 `merid`{.Agda}, as our functions `f`{.Agda} and `g`{.Agda} can only
-be `con`{.Agda}, so it reduces (with a suitable element of `C`{.Agda})
-from `∀ c → inl (f c) ≡ inr (g c)`{.Agda} to `inl tt ≡ inr tt`{.Agda}, or
-by funext, `inl ≡ inr`{.Agda}.
+be `to-top`{.Agda}, so it reduces (with a suitable element of `C`{.Agda})
+from `∀ c → inl (f c) ≡ inr (g c)`{.Agda} to `inl tt ≡ inr tt`{.Agda},
+or equivalently `inl ≡ inr`{.Agda}.
 
 We therefore aim to show:
 
 ```agda
-Susp≡Pushout-⊤←A→⊤ : ∀ {A} → Susp A ≡ Pushout A ⊤ to-top ⊤ to-top
+Susp≡Pushout-⊤←A→⊤ : ∀ {A} → Susp A ≡ Pushout A ⊤ (const tt) ⊤ (const tt)
 ```
 
-The left and right functions are very simple:
+The left and right functions are trival:
 
 ```agda
-Susp→Pushout-⊤←A→⊤ : ∀ {A} → Susp A → Pushout A ⊤ to-top ⊤ to-top
+Susp→Pushout-⊤←A→⊤ : ∀ {A} → Susp A → Pushout A ⊤ (const tt) ⊤ (const tt)
 Susp→Pushout-⊤←A→⊤ N = inl tt
 Susp→Pushout-⊤←A→⊤ S = inr tt
 Susp→Pushout-⊤←A→⊤ (merid x i) = commutes x i
 
-Pushout-⊤←A→⊤→Susp : ∀ {A} → Pushout A ⊤ to-top ⊤ to-top → Susp A
-Pushout-⊤←A→⊤→Susp (inl x) = N
-Pushout-⊤←A→⊤→Susp (inr x) = S
-Pushout-⊤←A→⊤→Susp (commutes c i) = merid c i
+Pushout-⊤←A→⊤-to-Susp : ∀ {A} → Pushout A ⊤ (const tt) ⊤ (const tt) → Susp A
+Pushout-⊤←A→⊤-to-Susp (inl x) = N
+Pushout-⊤←A→⊤-to-Susp (inr x) = S
+Pushout-⊤←A→⊤-to-Susp (commutes c i) = merid c i
 ```
 
-We then have:
+So we then have:
 
 ```agda
 Susp≡Pushout-⊤←A→⊤ = ua (Susp→Pushout-⊤←A→⊤ , is-iso→is-equiv iso-pf) where
@@ -138,7 +137,7 @@ similarities in structure.</summary>
   open is-iso
 
   iso-pf : is-iso Susp→Pushout-⊤←A→⊤
-  iso-pf .inv = Pushout-⊤←A→⊤→Susp
+  iso-pf .inv = Pushout-⊤←A→⊤-to-Susp 
   iso-pf .rinv (inl x) = refl
   iso-pf .rinv (inr x) = refl
   iso-pf .rinv (commutes c i) = refl
@@ -148,20 +147,17 @@ similarities in structure.</summary>
 ```
 </details>
 
-## The Universal property of a pushout
+## The Universal property of a pushout, via Cocones
 
-We can also formulate the universal property of a pushout. We first
-do this by introducing the `cocone`{.Adga}. A `cocone`{.Agda},
-given a type `D`{.Agda} and a span $\mathcal{D}$:
+To formulate the universal property of a pushout, we first introduce the **Cocone**.
+A `Cocone`{.Agda}, given a type `D`{.Agda} and a span:
 
 ~~~{.quiver}
-\begin{tikzpicture}
-\node[] (c) at (2, 0) {$C$};
-\node[] (a) at (0, 0) {$A$};
-\node[] (b) at (4, 0) {$B$};
-\draw[->] (c) -- (a) node[midway,above]{${f}$};
-\draw[->] (c) -- (b) node[midway,above]{${g}$};
-\end{tikzpicture}
+\[\begin{tikzcd}
+	A & C & B
+	\arrow["f"', from=1-2, to=1-1]
+	\arrow["g", from=1-2, to=1-3]
+\end{tikzcd}\]
 ~~~
 
 consists of functions:
@@ -190,37 +186,38 @@ and a homotopy
 forming:
 
 ~~~{.quiver}
-\begin{tikzpicture}
-\node[] (c) at (0, 0) {$C$};
-\node[] (a) at (0, -2) {$A$};
-\node[] (b) at (2, 0) {$B$};
-\node[] (d) at (2, -2) {$D$};
-\draw[->] (c) -- (a) node[midway,xshift=-10]{${f}$};
-\draw[->] (c) -- (b) node[midway,above]{${g}$};
-\draw[->] (a) -- (d) node[midway,below]{$i$};
-\draw[->] (b) -- (d) node[midway,right]{$j$};
-\draw[->,shorten <=0.2cm,shorten >=0.2cm,very thick] (a) -- (b) node[midway,above left]{$h$};
-\end{tikzpicture}
+\[\begin{tikzcd}
+	C && B \\
+	\\
+	A && D
+	\arrow["g", from=1-1, to=1-3]
+	\arrow["f"', from=1-1, to=3-1]
+	\arrow["j", from=1-3, to=3-3]
+	\arrow["h"{description}, shorten <=6pt, shorten >=6pt, Rightarrow, from=3-1, to=1-3]
+	\arrow["i"', from=3-1, to=3-3]
+\end{tikzcd}\]
 ~~~
 
+
 One can then note the similarities between this definition,
-and our previous `Pushout`{.Agda} definition. We denote the type of `cocone`{.Agda}s as:
+and our previous `Pushout`{.Agda} definition. We denote the type of
+`Cocone`{.Agda}s as:
 
 ```agda
-cocone : {C A B : Type} → (f : C → A) → (g : C → B) → (D : Type) → Type
-cocone {C} {A} {B} f g D =
+Cocone : {C A B : Type} → (f : C → A) → (g : C → B) → (D : Type) → Type
+Cocone {C} {A} {B} f g D =
   Σ[ i ∈ (A → D) ]
     Σ[ j ∈ (B → D) ]
       ((c : C) → i (f c) ≡ j (g c))
 ```
 
-We can then show that the canonical `cocone`{.Agda} consisting of a `Pushout`{.Agda}
-is the universal `cocone`{.Agda}.
+We can then show that the canonical `Cocone`{.Agda} consisting of a `Pushout`{.Agda}
+is the universal `Cocone`{.Agda}.
 
 ```agda
-Pushout→E≡coconeE : ∀ {A B C E f g} →
-                    (Pushout C A f B g → E) ≡ (cocone f g E)
-Pushout→E≡coconeE = ua ( pushout→cocone , is-iso→is-equiv iso-pc ) where
+Pushout→E≡CoconeE : ∀ {A B C E f g} →
+                    (Pushout C A f B g → E) ≡ (Cocone f g E)
+Pushout→E≡CoconeE = ua ( pushout→Cocone , is-iso→is-equiv iso-pc ) where
 ```
 
 <details><summary> Once again we show that the above is an equivalence;
@@ -230,19 +227,19 @@ and again mostly reduces to `refl`{.Agda}.
 ```agda
   open is-iso
 
-  pushout→cocone : ∀ {A B C E f g} → (Pushout C A f B g → E) → cocone f g E
-  cocone→pushout : ∀ {A B C E f g} → cocone f g E → (Pushout C A f B g → E)
-  iso-pc : is-iso pushout→cocone
+  pushout→Cocone : ∀ {A B C E f g} → (Pushout C A f B g → E) → Cocone f g E
+  Cocone→pushout : ∀ {A B C E f g} → Cocone f g E → (Pushout C A f B g → E)
+  iso-pc : is-iso pushout→Cocone
 
-  pushout→cocone t = (λ x → t (inl x)) ,
+  pushout→Cocone t = (λ x → t (inl x)) ,
                      (λ x → t (inr x)) ,
                      (λ c i → ap t (commutes c) i)
 
-  cocone→pushout t (inl x) = fst t x 
-  cocone→pushout t (inr x) = fst (snd t) x
-  cocone→pushout t (commutes c i) = snd (snd t) c i
+  Cocone→pushout t (inl x) = fst t x 
+  Cocone→pushout t (inr x) = fst (snd t) x
+  Cocone→pushout t (commutes c i) = snd (snd t) c i
 
-  iso-pc .inv = cocone→pushout
+  iso-pc .inv = Cocone→pushout
   iso-pc .rinv _ = refl
   iso-pc .linv _ = funext (λ { (inl y) → refl;
                                 (inr y) → refl;

From 7f39bc6ae3bb3eaf00d83eb5314162ec9eacf3a5 Mon Sep 17 00:00:00 2001
From: jake-87 <jakehfreebsd@gmail.com>
Date: Sat, 27 Jul 2024 19:40:40 +1000
Subject: [PATCH 03/10] Remove conflicting definition

---
 src/Homotopy/Pushout.lagda.md | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/Homotopy/Pushout.lagda.md b/src/Homotopy/Pushout.lagda.md
index cf3274564..43cedaaea 100644
--- a/src/Homotopy/Pushout.lagda.md
+++ b/src/Homotopy/Pushout.lagda.md
@@ -11,7 +11,7 @@ open import Homotopy.Space.Suspension
 module Homotopy.Pushout where
 ```
 
-# Pushouts {defines="pushout cocone"}
+# Pushouts {defines="pushout"}
 
 Given the following span:
 
@@ -217,7 +217,7 @@ is the universal `Cocone`{.Agda}.
 ```agda
 Pushout→E≡CoconeE : ∀ {A B C E f g} →
                     (Pushout C A f B g → E) ≡ (Cocone f g E)
-Pushout→E≡CoconeE = ua ( pushout→Cocone , is-iso→is-equiv iso-pc ) where
+Pushout→E≡CoconeE = ua ( Pushout→Cocone , is-iso→is-equiv iso-pc ) where
 ```
 
 <details><summary> Once again we show that the above is an equivalence;
@@ -227,19 +227,19 @@ and again mostly reduces to `refl`{.Agda}.
 ```agda
   open is-iso
 
-  pushout→Cocone : ∀ {A B C E f g} → (Pushout C A f B g → E) → Cocone f g E
-  Cocone→pushout : ∀ {A B C E f g} → Cocone f g E → (Pushout C A f B g → E)
-  iso-pc : is-iso pushout→Cocone
+  Pushout→Cocone : ∀ {A B C E f g} → (Pushout C A f B g → E) → Cocone f g E
+  Cocone→Pushout : ∀ {A B C E f g} → Cocone f g E → (Pushout C A f B g → E)
+  iso-pc : is-iso Pushout→Cocone
 
-  pushout→Cocone t = (λ x → t (inl x)) ,
+  Pushout→Cocone t = (λ x → t (inl x)) ,
                      (λ x → t (inr x)) ,
                      (λ c i → ap t (commutes c) i)
 
-  Cocone→pushout t (inl x) = fst t x 
-  Cocone→pushout t (inr x) = fst (snd t) x
-  Cocone→pushout t (commutes c i) = snd (snd t) c i
+  Cocone→Pushout t (inl x) = fst t x 
+  Cocone→Pushout t (inr x) = fst (snd t) x
+  Cocone→Pushout t (commutes c i) = snd (snd t) c i
 
-  iso-pc .inv = Cocone→pushout
+  iso-pc .inv = Cocone→Pushout
   iso-pc .rinv _ = refl
   iso-pc .linv _ = funext (λ { (inl y) → refl;
                                 (inr y) → refl;

From 3a687f159d66e84ff048c9365ba7906252500915 Mon Sep 17 00:00:00 2001
From: j <68929154+jake-87@users.noreply.github.com>
Date: Fri, 2 Aug 2024 12:22:23 +1000
Subject: [PATCH 04/10] Wording

---
 src/Homotopy/Pushout.lagda.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Homotopy/Pushout.lagda.md b/src/Homotopy/Pushout.lagda.md
index 43cedaaea..7d23f4404 100644
--- a/src/Homotopy/Pushout.lagda.md
+++ b/src/Homotopy/Pushout.lagda.md
@@ -42,7 +42,7 @@ Two functions `inl`{.Agda} and `inr`{.Agda}, that "connect" from `A` and `B`:
 ```
 
 And, for every `c : C`, a path
-`commutes : inl (f c) ≡ inr (g c)`{.Agda}:
+`inl (f c) ≡ inr (g c)`{.Agda}:
 
 ```agda
   commutes : ∀ c → inl (f c) ≡ inr (g c)
@@ -98,7 +98,7 @@ non-path constructors have input `⊤`{.Agda}, they're indistiguishable
 from members of the pushout; therefore, we take the
 `inl`{.Agda} and `inr`{.Agda} to `N`{.Agda} and
 `S`{.Agda} respectively.
-Likewise, we turn `commutes`{.Agda} into
+Likewise, we take `commutes`{.Agda} to
 `merid`{.Agda}, as our functions `f`{.Agda} and `g`{.Agda} can only
 be `to-top`{.Agda}, so it reduces (with a suitable element of `C`{.Agda})
 from `∀ c → inl (f c) ≡ inr (g c)`{.Agda} to `inl tt ≡ inr tt`{.Agda},
@@ -110,7 +110,7 @@ We therefore aim to show:
 Susp≡Pushout-⊤←A→⊤ : ∀ {A} → Susp A ≡ Pushout A ⊤ (const tt) ⊤ (const tt)
 ```
 
-The left and right functions are trival:
+The left and right functions are therefore trival:
 
 ```agda
 Susp→Pushout-⊤←A→⊤ : ∀ {A} → Susp A → Pushout A ⊤ (const tt) ⊤ (const tt)

From bebab6150d31a6f7be44e677fa6e60c791f0555e Mon Sep 17 00:00:00 2001
From: Wren H <>
Date: Sat, 3 Aug 2024 20:06:22 +1000
Subject: [PATCH 05/10] Wording & Naming

---
 src/Homotopy/Pushout.lagda.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Homotopy/Pushout.lagda.md b/src/Homotopy/Pushout.lagda.md
index 43cedaaea..7b67d949d 100644
--- a/src/Homotopy/Pushout.lagda.md
+++ b/src/Homotopy/Pushout.lagda.md
@@ -147,7 +147,7 @@ similarities in structure.</summary>
 ```
 </details>
 
-## The Universal property of a pushout, via Cocones
+## The universal property of a pushout, via Cocones
 
 To formulate the universal property of a pushout, we first introduce the **Cocone**.
 A `Cocone`{.Agda}, given a type `D`{.Agda} and a span:
@@ -215,9 +215,9 @@ We can then show that the canonical `Cocone`{.Agda} consisting of a `Pushout`{.A
 is the universal `Cocone`{.Agda}.
 
 ```agda
-Pushout→E≡CoconeE : ∀ {A B C E f g} →
+Pushout-is-universal-cocone : ∀ {A B C E f g} →
                     (Pushout C A f B g → E) ≡ (Cocone f g E)
-Pushout→E≡CoconeE = ua ( Pushout→Cocone , is-iso→is-equiv iso-pc ) where
+Pushout-is-universal-cocone = ua ( Pushout→Cocone , is-iso→is-equiv iso-pc ) where
 ```
 
 <details><summary> Once again we show that the above is an equivalence;

From d11b5eaf7a632f1ab9e8029b2e67d0bfd4a5c762 Mon Sep 17 00:00:00 2001
From: Wren H <>
Date: Sat, 3 Aug 2024 20:12:36 +1000
Subject: [PATCH 06/10] Remove newline

---
 src/Homotopy/Pushout.lagda.md | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Homotopy/Pushout.lagda.md b/src/Homotopy/Pushout.lagda.md
index 29453b575..eb1e9dae4 100644
--- a/src/Homotopy/Pushout.lagda.md
+++ b/src/Homotopy/Pushout.lagda.md
@@ -215,8 +215,7 @@ We can then show that the canonical `Cocone`{.Agda} consisting of a `Pushout`{.A
 is the universal `Cocone`{.Agda}.
 
 ```agda
-Pushout-is-universal-cocone : ∀ {A B C E f g} →
-                    (Pushout C A f B g → E) ≡ (Cocone f g E)
+Pushout-is-universal-cocone : ∀ {A B C E f g} → (Pushout C A f B g → E) ≡ (Cocone f g E)
 Pushout-is-universal-cocone = ua ( Pushout→Cocone , is-iso→is-equiv iso-pc ) where
 ```
 

From 3b624f36888a17346dcba9a4b79e59a75830ee93 Mon Sep 17 00:00:00 2001
From: Wren H <>
Date: Sat, 3 Aug 2024 20:14:21 +1000
Subject: [PATCH 07/10] Forgot to update HoTT page

---
 src/HoTT.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/HoTT.lagda.md b/src/HoTT.lagda.md
index 000b27dee..742d02a54 100644
--- a/src/HoTT.lagda.md
+++ b/src/HoTT.lagda.md
@@ -610,14 +610,14 @@ _ = T²
 ```agda
 _ = Pushout
 _ = Cocone
-_ = Pushout→E≡CoconeE
+_ = Pushout-is-universal-cocone
 _ = Susp≡Pushout-⊤←A→⊤
 ```
 -->
 
 * The pushout: `Pushout`{.Agda}
 * Definition 6.8.1: `Cocone`{.Agda}
-* Lemma 6.8.2: `Pushout→E≡CoconeE`{.Agda}
+* Lemma 6.8.2: `Pushout-is-universal-cocone`{.Agda}
 * Observation: `Susp≡Pushout-⊤←A→⊤`{.Agda}
 
 ### 6.9: Truncations

From 5a163aa0f6e2404d79f77f1b0babebaee44da047 Mon Sep 17 00:00:00 2001
From: Wren H <>
Date: Sat, 3 Aug 2024 20:58:38 +1000
Subject: [PATCH 08/10] Suggestions from ncfavier

---
 src/Homotopy/Pushout.lagda.md | 69 +++++++----------------------------
 1 file changed, 13 insertions(+), 56 deletions(-)

diff --git a/src/Homotopy/Pushout.lagda.md b/src/Homotopy/Pushout.lagda.md
index eb1e9dae4..d425da080 100644
--- a/src/Homotopy/Pushout.lagda.md
+++ b/src/Homotopy/Pushout.lagda.md
@@ -25,26 +25,15 @@ Given the following span:
 \end{tikzcd}\]
 ~~~
 
-The **Pushout** of this span is defined as the higher inductive type
+The **pushout** of this span is defined as the higher inductive type
 presented by:
 ```agda
 data Pushout {ℓ} (C : Type ℓ)
                  (A : Type ℓ) (f : C → A)
                  (B : Type ℓ) (g : C → B)
                  : Type ℓ where
-```
-
-Two functions `inl`{.Agda} and `inr`{.Agda}, that "connect" from `A` and `B`:
-
-```agda
   inl : A → Pushout C A f B g
   inr : B → Pushout C A f B g
-```
-
-And, for every `c : C`, a path
-`inl (f c) ≡ inr (g c)`{.Agda}:
-
-```agda
   commutes : ∀ c → inl (f c) ≡ inr (g c)
 ```
 
@@ -57,26 +46,25 @@ These combine to give the following:
 	A && {\rm{Pushout}}
 	\arrow["g", from=1-1, to=1-3]
 	\arrow["f"', from=1-1, to=3-1]
-	\arrow["{\rm{inl}}", from=1-3, to=3-3]
+	\arrow["{\rm{inr}}", from=1-3, to=3-3]
 	\arrow["{\rm{commutes}}"{description}, shorten <=6pt, shorten >=6pt, Rightarrow, from=3-1, to=1-3]
 	\arrow["{\rm{inl}}"', from=3-1, to=3-3]
 \end{tikzcd}\]
 ~~~
 
-## Suspensions as Pushouts
+## Suspensions as pushouts
 
-First, recall the `Susp`{.Agda}, which serves to increase the
-connectedness of a space. Suspension can be expressed as a
-`Pushout`{.Agda} of, for some type `A`, the span `⊤ ← A → ⊤`{.Agda}:
+The [[suspension]] of a type $A$ can be expressed as the  `Pushout`{.Agda}
+of the span `⊤ ← A → ⊤`{.Agda}:
 
 ~~~{.quiver}
 \[\begin{tikzcd}
 	C && \top \\
 	\\
 	\top && {\rm{Pushout}}
-	\arrow["{\rm{const\,tt}}", from=1-1, to=1-3]
-	\arrow["{\rm{const\,tt}}"', from=1-1, to=3-1]
-	\arrow["{\rm{inl}}", from=1-3, to=3-3]
+	\arrow["{\rm{!}}", from=1-1, to=1-3]
+	\arrow["{\rm{!}}"', from=1-1, to=3-1]
+	\arrow["{\rm{inr}}", from=1-3, to=3-3]
 	\arrow["{\rm{commutes}}"{description}, shorten <=6pt, shorten >=6pt, Rightarrow, from=3-1, to=1-3]
 	\arrow["{\rm{inl}}"', from=3-1, to=3-3]
 \end{tikzcd}\]
@@ -99,20 +87,11 @@ from members of the pushout; therefore, we take the
 `inl`{.Agda} and `inr`{.Agda} to `N`{.Agda} and
 `S`{.Agda} respectively.
 Likewise, we take `commutes`{.Agda} to
-`merid`{.Agda}, as our functions `f`{.Agda} and `g`{.Agda} can only
-be `to-top`{.Agda}, so it reduces (with a suitable element of `C`{.Agda})
-from `∀ c → inl (f c) ≡ inr (g c)`{.Agda} to `inl tt ≡ inr tt`{.Agda},
-or equivalently `inl ≡ inr`{.Agda}.
-
-We therefore aim to show:
+`merid`{.Agda}.
 
 ```agda
 Susp≡Pushout-⊤←A→⊤ : ∀ {A} → Susp A ≡ Pushout A ⊤ (const tt) ⊤ (const tt)
-```
-
-The left and right functions are therefore trival:
 
-```agda
 Susp→Pushout-⊤←A→⊤ : ∀ {A} → Susp A → Pushout A ⊤ (const tt) ⊤ (const tt)
 Susp→Pushout-⊤←A→⊤ N = inl tt
 Susp→Pushout-⊤←A→⊤ S = inr tt
@@ -147,9 +126,9 @@ similarities in structure.</summary>
 ```
 </details>
 
-## The universal property of a pushout, via Cocones
+## The universal property of pushouts
 
-To formulate the universal property of a pushout, we first introduce the **Cocone**.
+To formulate the universal property of a pushout, we first introduce **cocones**.
 A `Cocone`{.Agda}, given a type `D`{.Agda} and a span:
 
 ~~~{.quiver}
@@ -160,30 +139,8 @@ A `Cocone`{.Agda}, given a type `D`{.Agda} and a span:
 \end{tikzcd}\]
 ~~~
 
-consists of functions:
-<!--
-```agda
-module _ (A B C D : Type) (f : C → A) (g : C → B)
-  (i' : A → D) (j' : B → D) (h' : (c : C) → i' (f c) ≡ j' (g c))
-  where
-```
--->
-```agda
-  i : A → D
-  j : B → D
-``` 
-and a homotopy
-```agda
-  h : (c : C) → i (f c) ≡ j (g c)
-```
-<!--
-```agda
-  i = i'
-  j = j'
-  h = h'
-```
--->
-forming:
+consists of functions `i : A → D`{.Agda} & `j : B → D`{.Agda}, and a homotopy
+`h : (c : C) → i (f c) ≡ j (g c)`{.Agda}, forming:
 
 ~~~{.quiver}
 \[\begin{tikzcd}

From 98786e5fe6949dd45f470e702e19f027abac4d0a Mon Sep 17 00:00:00 2001
From: Wren H <>
Date: Sat, 3 Aug 2024 21:01:24 +1000
Subject: [PATCH 09/10] Inline latex

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

diff --git a/src/Homotopy/Pushout.lagda.md b/src/Homotopy/Pushout.lagda.md
index d425da080..872227605 100644
--- a/src/Homotopy/Pushout.lagda.md
+++ b/src/Homotopy/Pushout.lagda.md
@@ -55,7 +55,7 @@ These combine to give the following:
 ## Suspensions as pushouts
 
 The [[suspension]] of a type $A$ can be expressed as the  `Pushout`{.Agda}
-of the span `⊤ ← A → ⊤`{.Agda}:
+of the span $\top \ot A \to \top$:
 
 ~~~{.quiver}
 \[\begin{tikzcd}

From 207439745e71002bb1a93b2f9845a5edb50e57d9 Mon Sep 17 00:00:00 2001
From: j <68929154+jake-87@users.noreply.github.com>
Date: Sat, 3 Aug 2024 21:02:07 +1000
Subject: [PATCH 10/10] Inline latex
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Naïm Favier <n@monade.li>
---
 src/Homotopy/Pushout.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Homotopy/Pushout.lagda.md b/src/Homotopy/Pushout.lagda.md
index 872227605..a424f277d 100644
--- a/src/Homotopy/Pushout.lagda.md
+++ b/src/Homotopy/Pushout.lagda.md
@@ -139,8 +139,8 @@ A `Cocone`{.Agda}, given a type `D`{.Agda} and a span:
 \end{tikzcd}\]
 ~~~
 
-consists of functions `i : A → D`{.Agda} & `j : B → D`{.Agda}, and a homotopy
-`h : (c : C) → i (f c) ≡ j (g c)`{.Agda}, forming:
+consists of functions $i : A \to D$, $j : B \to D$, and a homotopy
+$h : (c : C) \to i (f c) \is j (g c)$, forming:
 
 ~~~{.quiver}
 \[\begin{tikzcd}