nat.cast
Canonical homomorphism from
ℕ
to a type
α
with
0
,
1
and
+
.