open import 1Lab.Prelude

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

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 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π

module _ {β β'} (A : Type β) (B : A β Type β') where


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β 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

  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 This means that, for any other 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 _ _))