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

W-elim : βˆ€ {β„“ β„“β€² β„“β€²β€²} {A : Type β„“} {B : A β†’ Type β„“β€²} {C : W A B β†’ Type β„“β€²β€²}
       β†’ ({a : A} {f : B a β†’ W A B} β†’ (βˆ€ ba β†’ C (f ba)) β†’ C (sup a f))
       β†’ (w : W A B) β†’ C w
W-elim {C = C} ps (sup a f) = ps (Ξ» ba β†’ W-elim {C = C} ps (f ba))

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πŸ”—

module _ {β„“ β„“β€²} (A : Type β„“) (B : A β†’ Type β„“β€²) where

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