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

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