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🔗
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
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-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.
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' : 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
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
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))) ∎
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