open import 1Lab.Prelude

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

module Data.Wellfounded.W where


The idea behind WW 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 WW is much simpler: A value of WABW_A B is a tree with nodes labelled by x:Ax : A, and such that the branching factor of such a node is given by B(x)B(x). WW-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)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:WABx : W_A B, we may as well assume it’s been proven for any (transitive) subtree of xx.

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