I've been thinking a lot about foundations, again, and specifically how to make isomorphism invariance clearer - which seems to be one of the main purposes of alternative foundations such as Homotopy Type Theory.
The problem seems to be that we often have different models of the same object which we would really like to identify with each other (as a simple example, $\mathbb{N} = \{\varnothing, \{\varnothing\}, \{\varnothing, \{\varnothing\} \}, \dots\}$ is an entirely different set from the $X \subseteq \mathbb{Z}$ we tend to call $\mathbb{N}$) and in ZFC, under the current definitions, we cannot formally do so. What we tend to do if we ever point this out at all is simply call it an abuse of notation, and justify it by claiming that the clear isomorphisms existing between the two models will preserve any theorems we want to invoke.
Homotopy type theory claims to make this easier by making it so that if we have two isomorphic objects we can say they are equal (in some sense I'm not entirely clear on) and so carry across any theorems we like. The problem is that it seems we really need to leave our comfort zone to be able to do this.
My question is...could this all be fixed by changing our point of view on some definitions? For instance, rather than saying "The set of natural numbers is [some specific set]", we could have the definition be phrased something like "$(X, Succ, 0)$ is a natural numbers set if and only if [Peano Axioms]", and then have as a theorem that $\{\varnothing, \{\varnothing\}, \{\varnothing, \{\varnothing\} \}, \dots\}$ is a natural numbers set.
What I'm effectively suggesting is that we relegate the phrase "set of natural numbers" to the same level as "group", so that rather than proving that some statement is true of a particular set which we have called the set of natural numbers, we prove that the statement is true for any set of natural numbers. When we want to work with natural numbers, we simply say "Let $\mathbb{N}$ be a set of natural numbers" in the same way that we often say "Let $G$ be a group".
What kind of problems arise from working in this way?
If I'm not being clear enough please let me know, because I do have a few specific definitions in my head that I could give as examples which might clarify what I mean.
EDIT: While structural set theory is effectively what I want, my question is whether or not this type of definition change would give us the benefits of structural set theory without leaving ZFC.