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β $Ξ$ and $Ξ£.$ 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π

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β
$(β,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
$PCβ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β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 _ _))