From 4adf036e0d5a38e922432df7b91259e405780104 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Na=C3=AFm=20Favier?= Date: Wed, 16 Aug 2023 17:05:50 +0200 Subject: [PATCH] defn: W-types are initial algebras --- src/1Lab/Path.lagda.md | 21 ++++++ src/Data/Wellfounded/W.lagda.md | 120 ++++++++++++++++++++++++++++++++ src/HoTT.lagda.md | 23 ++++++ 3 files changed, 164 insertions(+) diff --git a/src/1Lab/Path.lagda.md b/src/1Lab/Path.lagda.md index 30794c0e2..a5e2932a8 100644 --- a/src/1Lab/Path.lagda.md +++ b/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 diff --git a/src/Data/Wellfounded/W.lagda.md b/src/Data/Wellfounded/W.lagda.md index 555b5631a..dd7099bd2 100644 --- a/src/Data/Wellfounded/W.lagda.md +++ b/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 ``` + + 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 + +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 _ refl hom _ + coherent = transpose (flip₁ (∙-filler _ _)) +``` diff --git a/src/HoTT.lagda.md b/src/HoTT.lagda.md index b6e0fc555..8eb925e15 100644 --- a/src/HoTT.lagda.md +++ b/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 + + + +* W-types: `W`{.Agda} + +### 5.4 Inductive types are initial algebras + + + +* Theorem 5.4.7: `W-initial`{.Agda} + ## Chapter 6 Higher inductive types ### 6.2 Induction principles and dependent paths