open import 1Lab.Prelude

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

module Data.Wellfounded.W where

W-typesπŸ”—

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