Comment by bluGill
Type theory comes from math. Numbers in math do in fact have types. Most of the time we ignore it but numbers in math have types. math also has the concept of max number rolling back to zero ogain something anyone who has studied types in math would know. Rounding error is studied in several different math fields.
negative zero isn't in any math I know of. It is only in obsolete computer science though.
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".