open import 1Lab.Prelude

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

module Data.Wellfounded.W where

W-typesπŸ”—

The idea behind types is much simpler than they might appear at first brush, especially because their form is like that one of the β€œbig two” and However, the humble is much simpler: A value of is a tree with nodes labelled by and such that the branching factor of such a node is given by 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 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 we may as well assume it’s been proven for any (transitive) subtree of 

  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 types to illustrate the general fact that inductive types correspond to initial algebras for certain endofunctors. Here, we are working in the β€œambient” 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 algebra (or algebra) is simply a type with a function 

  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 

  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 This means that, for any other there is exactly one homomorphism 

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

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