defn: W-types are initial algebras

src/1Lab/Path.lagda.md

@@ -318,6 +318,27 @@ module _ {ℓ} {A : Type ℓ} {x y : A} {p : x ≡ y} where
     sym-invol i = p
 ```
 
+Given a `Square`{.Agda}, we can "flip" it along either dimension, or along the main diagonal:
+
+```agda
+module _ {ℓ} {A : Type ℓ} {a00 a01 a10 a11 : A}
+  {p : a00 ≡ a01}
+  {q : a00 ≡ a10}
+  {s : a01 ≡ a11}
+  {r : a10 ≡ a11}
+  (α : Square p q s r)
+  where
+
+  flip₁ : Square (sym p) s q (sym r)
+  flip₁ = symP α
+
+  flip₂ : Square r (sym q) (sym s) p
+  flip₂ i j = α i (~ j)
+
+  transpose : Square q p r s
+  transpose i j = α j i
+```
+
 # Paths
 
 While the basic structure of the path type is inherited from its nature

src/Data/Wellfounded/W.lagda.md

@@ -25,6 +25,15 @@ data W {ℓ ℓ′} (A : Type ℓ) (B : A → Type ℓ′) : Type (ℓ ⊔ ℓ
   sup : (x : A) (f : B x → W A B) → W A B
 ```
 
+<!--
+```agda
+W-elim : ∀ {ℓ ℓ′ ℓ′′} {A : Type ℓ} {B : A → Type ℓ′} {C : W A B → Type ℓ′′}
+       → ({a : A} {f : B a → W A B} → (∀ ba → C (f ba)) → C (sup a f))
+       → (w : W A B) → C w
+W-elim {C = C} ps (sup a f) = ps (λ ba → W-elim {C = C} ps (f ba))
+```
+-->
+
 The constructor `sup`{.Agda} stands for **supremum**: it bunches up
 (takes the supremum of) a bunch of subtrees, each subtree being given by
 a value $y : B(x)$ of the branching factor for that node. The natural
@@ -48,3 +57,114 @@ subtree of $x$.
       (λ { (j , p) → subst (Acc _<_) p (W-well-founded (f j)) })
       y<sup
 ```
+
+## Inductive types are initial algebras
+
+<!--
+```agda
+module _ {ℓ ℓ′} (A : Type ℓ) (B : A → Type ℓ′) where
+```
+-->
+
+We can use $W$ types to illustrate the general fact that inductive types
+correspond to *initial algebras* for certain endofunctors. Here, we are working
+in the "ambient" $\io$-category of types and functions, and we are interested in the
+[polynomial functor] `P`{.Agda}:
+
+[polynomial functor]: Cat.Instances.Poly.html
+
+```agda
+  P : Type (ℓ ⊔ ℓ′) → Type (ℓ ⊔ ℓ′)
+  P C = Σ A λ a → B a → C
+
+  P₁ : {C D : Type (ℓ ⊔ ℓ′)} → (C → D) → P C → P D
+  P₁ f (a , h) = a , f ∘ h
+```
+
+A $P$-**algebra** (or $W$-**algebra**) is simply a type $C$ with a function $P\,C \to C$.
+
+```agda
+  WAlg : Type _
+  WAlg = Σ (Type (ℓ ⊔ ℓ′)) λ C → P C → C
+```
+
+Algebras form a [category], where an **algebra homomorphism** is a function that respects
+the algebra structure.
+
+[category]: Cat.Base.html
+
+```agda
+  _W→_ : WAlg → WAlg → Type _
+  (C , c) W→ (D , d) = Σ (C → D) λ f → f ∘ c ≡ d ∘ P₁ f
+```
+
+Now the inductive `W`{.Agda} type defined above gives us a canonical $W$-algebra:
+
+```agda
+  W-algebra : WAlg
+  W-algebra .fst = W A B
+  W-algebra .snd (a , f) = sup a f
+```
+
+The claim is that this algebra is special in that it satisfies a *universal property*:
+it is [initial] in the aforementioned category of $W$-algebras.
+This means that, for any other $W$-algebra $C$, there is exactly one homomorphism $I \to C$.
+
+[initial]: Cat.Diagram.Initial.html
+
+```agda
+  is-initial-WAlg : WAlg → Type _
+  is-initial-WAlg I = (C : WAlg) → is-contr (I W→ C)
+```
+
+Existence is easy: the algebra $C$ gives us exactly the data we need to specify a function `W A B → C`
+by recursion, and the computation rules ensure that this respects the algebra structure definitionally.
+
+```agda
+  W-initial : is-initial-WAlg W-algebra
+  W-initial (C , c) .centre = W-elim (λ {a} f → c (a , f)) , refl
+```
+
+For uniqueness, we proceed by induction, using the fact that `g` is a homomorphism.
+
+```agda
+  W-initial (C , c) .paths (g , hom) = Σ-pathp unique coherent where
+    unique : W-elim (λ {a} f → c (a , f)) ≡ g
+    unique = funext (W-elim λ {a} {f} rec → ap (λ x → c (a , x)) (funext rec)
+                                          ∙ sym (hom $ₚ (a , f)))
+```
+
+There is one subtlety: being an algebra homomorphism is *not* a [proposition] in general,
+so we must also show that `unique`{.Agda} is in fact an **algebra 2-cell**, i.e. that it
+makes the following two identity proofs equal:
+
+[proposition]: 1Lab.HLevel.html#is-prop
+
+~~~{.quiver .tall-15}
+\[\begin{tikzcd}
+	{P\,W} && {P\,C} & {P\,W} && {P\,C} \\
+	\\
+	W && C & W && C
+	\arrow["{\text{sup}}"', from=1-1, to=3-1]
+	\arrow["c", from=1-3, to=3-3]
+	\arrow[""{name=0, anchor=center, inner sep=0}, "f"', curve={height=12pt}, from=3-1, to=3-3]
+	\arrow[""{name=1, anchor=center, inner sep=0}, "{P\,f}"', curve={height=12pt}, from=1-1, to=1-3]
+	\arrow[""{name=2, anchor=center, inner sep=0}, "{P\,g}", curve={height=-12pt}, from=1-1, to=1-3]
+	\arrow["{\text{sup}}"', from=1-4, to=3-4]
+	\arrow["c", from=1-6, to=3-6]
+	\arrow[""{name=3, anchor=center, inner sep=0}, "f"', curve={height=12pt}, from=3-4, to=3-6]
+	\arrow[""{name=4, anchor=center, inner sep=0}, "g", curve={height=-12pt}, from=3-4, to=3-6]
+	\arrow[""{name=5, anchor=center, inner sep=0}, "{P\,g}", curve={height=-12pt}, from=1-4, to=1-6]
+	\arrow["{P\,\text{unique}}"{description}, draw=none, from=1, to=2]
+	\arrow["{\text{refl}}"{description}, draw=none, from=0, to=1]
+	\arrow["{\text{unique}}"{description}, draw=none, from=3, to=4]
+	\arrow["{\text{hom}}"{description}, draw=none, from=4, to=5]
+\end{tikzcd}\]
+~~~
+
+Luckily, this is completely straightforward.
+
+```agda
+    coherent : Square (λ i → unique i ∘ W-algebra .snd) refl hom (λ i → c ∘ P₁ (unique i))
+    coherent = transpose (flip₁ (∙-filler _ _))
+```

src/HoTT.lagda.md

@@ -37,6 +37,7 @@ open import Cat.Bi.Base
 open import Cat.Prelude
 
 open import Data.Set.Surjection
+open import Data.Wellfounded.W
 open import Data.Fin.Finite using (Finite-choice)
 open import Data.Dec
 open import Data.Nat using (ℕ-well-ordered ; Discrete-Nat)
@@ -411,6 +412,28 @@ _ = Map-classifier
 * Lemma 4.8.2: `Total-equiv`{.Agda}
 * Theorem 4.8.3: `Map-classifier`{.Agda}
 
+## Chapter 5 Induction
+
+### 5.3 W-types
+
+<!--
+```agda
+_ = W
+```
+-->
+
+* W-types: `W`{.Agda}
+
+### 5.4 Inductive types are initial algebras
+
+<!--
+```agda
+_ = W-initial
+```
+-->
+
+* Theorem 5.4.7: `W-initial`{.Agda}
+
 ## Chapter 6 Higher inductive types
 
 ### 6.2 Induction principles and dependent paths