Added (homotopy) Pushouts and Cocones, and some features/examples of said.

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
+_ = Pushout→E≡CoconeE
+_ = Susp≡Pushout-⊤←A→⊤
+```
+-->
+
+* 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
 
 <!--

src/Homotopy/Pushout.lagda.md

@@ -0,0 +1,249 @@
+<!--
+```agda
+open import 1Lab.Prelude
+
+open import Homotopy.Space.Suspension
+```
+-->
+
+
+```agda
+module Homotopy.Pushout where
+```
+
+# Pushouts {defines="pushout"}
+
+Given the following span:
+
+~~~{.quiver}
+\[\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** 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)
+```
+
+These combine to give the following:
+
+~~~{.quiver}
+\[\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}\]
+~~~
+
+## 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}:
+
+~~~{.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{commutes}}"{description}, shorten <=6pt, shorten >=6pt, Rightarrow, from=3-1, to=1-3]
+	\arrow["{\rm{inl}}"', from=3-1, to=3-3]
+\end{tikzcd}\]
+~~~
+
+<!--
+```agda
+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} - `const tt`{.Agda}.
+
+If one considers the structure we're creating, it becomes very
+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 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:
+
+```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
+Susp→Pushout-⊤←A→⊤ (merid x i) = commutes x 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
+```
+
+So 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→⊤-to-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, 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:
+
+~~~{.quiver}
+\[\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:
+<!--
+```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{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:
+
+```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>