English
The naturals are equivalent to their associated W-type: there is an equivalence between WType Natβ and ℕ given by toNat and ofNat.
Русский
Естественным образом натуральные числа эквивалентны своему соответствующему W-type: существует биекция между WType Natβ и ℕ, задаваемая toNat и ofNat.
LaTeX
$$$$\mathrm{equivNat}: WType(\mathrm{Nat},\beta) \simeq \mathbb{N},\quad \mathrm{toFun}=\mathrm{toNat},\ \mathrm{invFun}=\mathrm{ofNat}.$$$$
Lean4
/-- The naturals are equivalent to their associated `WType` -/
def equivNat : WType Natβ ≃ ℕ where
toFun := toNat
invFun := ofNat
left_inv := leftInverse_nat
right_inv := rightInverse_nat
