2. W-types and term algebras
A W-type is the type of well-founded trees over a signature: a
type of shapes together with a family assigning each shape its
branching. mathlib's WType provides the type and its fold
WType.elim, the morphism into an algebra of the polynomial
endofunctor X ↦ Σ a, β a → X. The development adds the two laws
mathlib does not state: the computation rule WType.elim_mk
and the uniqueness WType.elim_unique. Together they make
the W-type the initial algebra of that endofunctor, stated
concretely.
WType.para generalises the fold to a paramorphism, whose
step additionally sees each node's children as subtrees paired
with their folded values (Meertens, 1992)Lambert Meertens (1992). “Paramorphisms”. Formal Aspects of Computing. 4(5), pp. 413–424.:
WType.para {α : Type uA} {β : α → Type uB} (γ : Type uC)
(fγ : (Σ a : α, β a → WType β × γ) → γ) : WType β → γ
Its computation rule is WType.para_mk: the paramorphism at
a node applies the step to the node's children paired with their
own paramorphisms.
The module itself follows, rendered from its source: its module docstring as the prose of the section, and each declaration beside its docstring.