Another way to see it is to prepend every mathematical text involving ℤ with "for every ℤ such that [essential properties omitted]", so that you can apply it to several definitions of ℤ, rather than awkwardly redefining it after the fact. This is the mathematical equivalent of "programming to the interface", and is actually how mathematics are often formalized in modern proof assistants: as huge functors that abstract these details away.