open import 1Lab.Prelude

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

module Data.Wellfounded.W where

W-types🔗

The idea behind $W$ 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 \text{.}$ However, the humble $W$ is much simpler: A value of $W_{A}B$ is a tree with nodes labelled by $x:A\text{,}$ and such that the branching factor of such a node is given by $B(x)\text{.}$ $W\text{-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)$ 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:W_{A}B\text{,}$ we may as well assume it’s been proven for any (transitive) subtree of $x\text{.}$

  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 induction→initial {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') where

We can use $W$ types to illustrate the general fact that inductive types correspond to initial algebras for certain endofunctors. Here, we are working in the “ambient” $(\infty ,1)\text{-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 $P\text{-}$algebra (or $W\text{-}$algebra) is simply a type $C$ with a function $PC\to C\text{.}$

  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

  idW : ∀ {A} → A W→ A
  idW .fst = id
  idW .snd = refl

  _W∘_ : ∀ {A B C} → B W→ C → A W→ B → A W→ C
  (f W∘ g) .fst x = f .fst (g .fst x)
  (f W∘ g) .snd = ext λ a b → ap (f .fst) (happly (g .snd) (a , b)) ∙ happly (f .snd) _

Now the inductive W type defined above gives us a canonical $W\text{-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 $W\text{-algebras.}$ This means that, for any other $W\text{-algebra}$ $C\text{,}$ there is exactly one homomorphism $I\to C\text{.}$

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

Existence is easy: the algebra $C$ 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 $W\text{-algebra,}$ we recover the type $W_{A}B$ and its induction principle, albeit with a propositional computation rule.

open induction→initial using (WAlg ; is-initial-WAlg ; W-initial) public

module initial→induction {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') (alg : WAlg A B) (init : is-initial-WAlg A B alg) where
  open induction→initial A B using (_W→_ ; idW ; _W∘_)
  module _ where private

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\text{-algebra.}$

    W' : Type _
    W' = alg .fst

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

  open Σ alg renaming (fst to W' ; snd to sup')

We will now show that W' satisfies the induction principle of $W_{A}B\text{.}$ To that end, suppose we have a predicate $P:W^{\prime }\to \mathrm{Type}\text{,}$ the motive for induction, and a function — the method $m$ — showing $P(\sup (a,f))$ given the data of the constructor $a:A\text{,}$ $f:(b:Ba)\to W^{\prime }\text{,}$ and the induction hypotheses $f^{\prime }:(b:Ba)\to P(fb)\text{.}$

  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 $m$ is precisely what is needed to equip the total space ${\Sigma }_{x:W^{\prime }}P(x)$ of the motive $P$ with $W\text{-algebra}$ structure. Correspondingly, we call this a “total algebra” of $P\text{,}$ and write it $\int P\text{.}$

    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 $W^{\prime }\text{,}$ we then have a $W\text{-algebra}$ morphism $e:W^{\prime }\to \int P\text{.}$

    private module _ where private

      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 $W^{\prime }\to \int P\text{,}$ which sends an element $x:W^{\prime }$ to a pair $(i,d)\text{,}$ with $i:W^{\prime }$ and $d:P(i)\text{.}$ Since $i$ indexes a fibre of $P\text{,}$ we refer to it as the index of the result; the returned element $d$ 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

    open is-contr (init total-alg) renaming (centre to elim-hom)
    module _ (x : W') where
      open Σ (elim-hom .fst x) renaming (fst to index ; snd to datum) public

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 $P\text{.}$ 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 $P$ should admit a projection morphism to the base $W^{\prime }\text{.}$

The composition $$W^{\prime }\stackrel{e}{\to }\int P\stackrel{\pi }{\to }{W}^{\prime }$$ would then be an algebra morphism, inhabiting the contractible type $W^{\prime }\to W^{\prime }\text{,}$ which is also inhabited by the identity. But note that the function part of this composition is exactly $i\text{,}$ so we obtain a homotopy $\phi :i\equiv \mathrm{id}\text{.}$

    φ : ∀ 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 $e^{\prime }:\forall x,Px$ at $w:W^{\prime }$ by transporting $d(w):P(iw)$ along $\phi \text{.}$ Since we’ll want to characterise the value of $e^{\prime }(\sup f)$ using the second component of $\beta \text{,}$ we can not directly define $\phi$ in terms of the composition $\pi \circ e\text{.}$ Instead, we equip $i$ with a bespoke algebra structure, where the proof that $i(\sup f)=\sup (i\circ f)$ comes from the first component of $\beta \text{.}$

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

Since the construction of $\phi$ works at the level of algebra morphisms, rather than their underlying functions, we obtain a coherence $\psi \text{,}$ fitting in the diagram below.

To show that $e^{\prime }$ commutes with $\sup \text{,}$ we can then perform a short calculation using the second component of $\beta \text{,}$ the coherence $\psi \text{,}$ 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)))                                 ∎

      where
      sup'' : ∀ {a} (f : B a → W') → W'
      sup'' f = sup' (_ , f)


      nat-t : (ix : W' → W') (h : ix ≡ id) (dt : ∀ x → P (ix x)) → _
      nat-t ix h dt =
        ∀ a (f : B a → W')
        → subst P (ap sup'' (funext λ z → happly h (f z))) (psup (dt ∘ f))
        ≡ psup (λ z → subst P (happly h (f z)) (dt (f z)))

      nat : ∀ ix dt h → nat-t ix h dt
      nat ix dt h = J (λ ix h → ∀ dt → nat-t ix (sym h) dt)
        (λ dt a f → Regularity.fast! refl)
        (sym h) dt