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