Comment by ndriscoll
4 days ago
Mathematicians generally work with sets, not types. The first thing you do after defining the reals is agree that the naturals, integers, and rationals are subsets. From a type theory perspective, they are all type ℝ, and, roughly, the naturals satisfy the proposition "n:ℝ is a natural number".
Mathematics has a lot of different theories and some small branches have different rules. I've done mod math for example (it was maybe one week of classes) where you don't get an infinite set of possible numbers. It isn't nearly as interesting as far as mathematicians are concerned (for good reason) so it isn't looked at much but those theories exist.