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

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🔗

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

Initial algebras are inductive types🔗

We will now show the other direction of the correspondence: given an initial we recover the type and its induction principle, albeit with a propositional computation rule.

It’s easy to invert the construction of W-algebra to obtain a type W' and a candidate “constructor” sup', by projecting the corresponding components from the given

    W' : Type _
    W' = alg .fst

    sup' : (a : A) (b : B a  W')  W'
    sup' a b = alg .snd (a , b)

We will now show that W' satisfies the induction principle of To that end, suppose we have a predicate the motive for induction, and a function — the method — showing given the data of the constructor and the induction hypotheses

  module
    _ (P : W'  Type (  ℓ'))
      (psup :  {a f} (f' : (b : B a)  P (f b))  P (sup' (a , f)))
    where

The first part of the construction is observing that is precisely what is needed to equip the total space of the motive with structure. Correspondingly, we call this a “total algebra” of and write it

    total-alg : WAlg A B
    total-alg .fst = Σ[ x  W' ] P x
    total-alg .snd (x , ff') = sup' (x , fst  ff') , psup (snd  ff')

By our assumed initiality of we then have a morphism

      elim-hom : alg W→ total-alg
      elim-hom = init total-alg .centre

To better understand this, we can write out the components of this map. First, we have an underlying function which sends an element to a pair with and Since indexes a fibre of we refer to it as the index of the result; the returned element is the datum.

      index : W'  W'
      index x = elim-hom .fst x .fst

      datum :  x  P (index x)
      datum x = elim-hom .fst x .snd

We also have the equation expressing that elim-hom is an algebra map, which says that index and datum both commute with supremum, where the second identification depends on the first.

    beta
      : (a : A) (f : (x : B a)  W')
       (index (sup' (a , f)) , datum (sup' (a , f)))
         (sup' (a , index  f) , psup (datum  f))
    beta a f = happly (elim-hom .snd) (a , f)

The datum part of elim-hom is almost what we want, but it’s not quite a section of To get the actual elimination principle, we’ll have to get rid of the index in its type. The insight now is that, much like a total category admits a projection functor to the base, the total algebra of should admit a projection morphism to the base

The composition would then be an algebra morphism, inhabiting the contractible type which is also inhabited by the identity. But note that the function part of this composition is exactly so we obtain a homotopy

    φ :  x  index x  x
    φ = happly (ap fst htpy) module φ where
      πe : alg W→ alg
      πe .fst           = index
      πe .snd i (a , z) = beta a z i .fst

      htpy = is-contr→is-prop (init alg) πe idW

We can then define the eliminator at by transporting along Since we’ll want to characterise the value of using the second component of we can not directly define in terms of the composition Instead, we equip with a bespoke algebra structure, where the proof that comes from the first component of

    elim :  x  P x
    elim w = subst P (φ w) (datum w)

Since the construction of works at the level of algebra morphisms, rather than their underlying functions, we obtain a coherence fitting in the diagram below.

To show that commutes with we can then perform a short calculation using the second component of the coherence and some stock facts about substitution.

    β : (a : A) (f : (x : B a)  W')  elim (sup' (a , f))  psup (elim  f)
    β a f =
      let
        ψ :  a f  sym (ap fst (beta a f))  φ (sup' (a , f))  ap sup'' (funext λ i  φ (f i))
        ψ a z = square→commutes  i j  φ.htpy j .snd (~ i) (a , z))  ∙-idr _
      in
        subst P (φ (sup'' f))  datum (sup' (a , f))                                ≡⟨ ap! (from-pathp⁻ (ap snd (beta a f))) 
        subst P (φ (sup'' f)) (subst P (sym (ap fst (beta a f))) (psup (datum  f))) ≡⟨ sym (subst-∙ P _ _ _)  ap₂ (subst P) (ψ a f) refl 
        subst P (ap sup'' (funext λ z  φ (f z))) (psup (datum  f))                 ≡⟨ nat index datum (funext φ) a f 
        psup  z  subst P (φ (f z)) (datum (f z)))