English
There is a natural isomorphism between the W-type WType Natβ and the natural numbers, with the forward map toNat and the backward map ofNat as inverse pieces. Concretely, toNat sends a node with zero label to 0, and a node with succ label to 1 plus the toNat of the sole subtree.
Русский
Существует естественный биекция между WType Natβ и натуральными числами, осуществляемая отображениями toNat и ofNat; нода с меткой нуля идёт в 0, нода со меткой succ даёт 1 плюс значение из единственного поддерева.
LaTeX
$$$$\mathrm{toNat}: WType(\mathrm{Nat},\beta) \to \mathbb{N},\quad \mathrm{toNat}(\mathrm{WType.mk}(\mathrm{Nat\alpha.zero},\phi))=0,\quad \mathrm{toNat}(\mathrm{WType.mk}(\mathrm{Nat\alpha.succ}, f))=\mathrm{succ}(\mathrm{toNat}(f(\mathrm{unit}))).$$$$
Lean4
/-- The isomorphism from the `WType` of the naturals to the naturals -/
@[simp]
def toNat : WType Natβ → ℕ
| WType.mk Natα.zero _ => 0
| WType.mk Natα.succ f => (f ()).toNat.succ
