English
There is a canonical way to embed the natural numbers into a W-type built from natural-number labels. Define ofNat by sending 0 to a leaf (a node with label 0 and no children) and sending n+1 to a node labeled by succ with a single subtree equal to ofNat n. This yields a natural correspondence between ℕ and the corresponding W-type.
Русский
Существует каноническое вложение натуральных чисел в W-type, построенный из меток натуральных чисел. Определим ofNat так: 0 отображается в вершину-лист, не имеющую потомков; n+1 отображается в вершину с меткой succ и единственным потомком, равным ofNat n. Таким образом, существует естественная связь между ℕ и соответствующим W-type.
LaTeX
$$$$\mathrm{ofNat}: \mathbb{N} \to WType(\mathrm{Nat},\beta),\quad \mathrm{ofNat}(0)=\mathrm{WType.mk}\,\mathrm{Nat\alpha.zero}\,\mathrm{Empty.elim},\quad \mathrm{ofNat}(n+1)=\mathrm{WType.mk}\,\mathrm{Nat\alpha.succ}\, (\lambda\_:\beta.\mathrm{ofNat}(n)).$$$$
Lean4
/-- The isomorphism from the naturals to its corresponding `WType` -/
@[simp]
def ofNat : ℕ → WType Natβ
| Nat.zero => ⟨Natα.zero, Empty.elim⟩
| Nat.succ n => ⟨Natα.succ, fun _ ↦ ofNat n⟩
