module Data.Wellfounded.W where
W-typesπ
The idea behind 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 is much simpler: A value of is a tree with nodes labelled by , and such that the branching factor of such a node is given by . -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
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 , we may as well assume itβs been proven for any (transitive) subtree of .
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
types to illustrate the general fact that inductive types correspond to
initial algebras for certain endofunctors. Here, we are working
in the βambientβ
-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 -algebra (or -algebra) is simply a type with a function .
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
-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 -algebras. This means that, for any other -algebra , there is exactly one homomorphism .
is-initial-WAlg : WAlg β Type _ is-initial-WAlg I = (C : WAlg) β is-contr (I Wβ C)
Existence is easy: the algebra
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 _ _))