open import 1Lab.Prelude

open import Data.Wellfounded.Properties
open import Data.Wellfounded.Base

module Data.Wellfounded.W where


# W-typesπ

The idea behind $W$ types is much simpler than they might appear at first brush, especially because their form is like that one of the βbig twoβ $\Pi$ and $\Sigma$. However, the humble $W$ is much simpler: A value of $W_A B$ is a tree with nodes labelled by $x : A$, and such that the branching factor of such a node is given by $B(x)$. $W$-types can be defined inductively:

data W {β ββ²} (A : Type β) (B : A β Type ββ²) : Type (β β ββ²) where
sup : (x : A) (f : B x β W A B) β W A B

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 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 question to ask, then, is: βsupremum in what order?β. The order given by the βis a subtree ofβ relation!

module _ {β ββ²} {A : Type β} {B : A β Type ββ²} where
_<_ : W A B β W A B β Type _
x < sup i f = β[ j β B i ] (f j β‘ x)


This order is actually well-founded: if we want to prove a property of $x : W_A B$, we may as well assume itβs been proven for any (transitive) subtree of $x$.

  W-well-founded : Wf _<_
W-well-founded (sup x f) = acc Ξ» y y<sup β
β₯-β₯-rec (Acc-is-prop _)
(Ξ» { (j , p) β subst (Acc _<_) p (W-well-founded (f j)) })
y<sup


## Inductive types are initial algebrasπ

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β $(\infty,1)$-category of types and functions, and we are interested in the polynomial functor P:

  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$.

  WAlg : Type _
WAlg = Ξ£ (Type (β β ββ²)) Ξ» C β P C β C


Algebras form a category, where an algebra homomorphism is a function that respects the algebra structure.

  _Wβ_ : WAlg β WAlg β Type _
(C , c) Wβ (D , d) = Ξ£ (C β D) Ξ» f β f β c β‘ d β Pβ f


Now the inductive W type defined above gives us a canonical $W$-algebra:

  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$.

  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.

  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.

  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 is in fact an algebra 2-cell, i.e.Β that it makes the following two identity proofs equal:

Luckily, this is completely straightforward.

    coherent : Square (Ξ» i β unique i β W-algebra .snd) refl hom (Ξ» i β c β Pβ (unique i))
coherent = transpose (flipβ (β-filler _ _))