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

Inductive types are initial algebrasπŸ”—

We can use WW types to illustrate the general fact that inductive types correspond to initial algebras for certain endofunctors. Here, we are working in the β€œambient” (∞,1)(\infty,1)-category 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 PP-algebra (or WW-algebra) is simply a type CC with a function P Cβ†’CP\,C \to C.

  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 WW-algebra:

  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 WW-algebras. This means that, for any other WW-algebra CC, there is exactly one homomorphism I→CI \to C.

  is-initial-WAlg : WAlg β†’ Type _
  is-initial-WAlg I = (C : WAlg) → is-contr (I W→ C)

Existence is easy: the algebra CC 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 _ _))