I apologize for posting as an answer what should really be a comment, connected to one of Jacques Carette's comments on my earlier answer. Unfortunately, this is way too long for a comment. Jacques asked why we would bother with set-theoretic foundations at all. It happens that I wrote down my opinion about that about 15 years ago (in a private e-mail) and repeated some of it on the fom (= foundations of mathematics) e-mail list. Here's a slightly edited version of that:

Mathematicians generally reason in a theory T which (up to possible minor variations between individual mathematicians) can be described as follows. It is a many-sorted first-order theory. The sorts include numbers (natural, real, complex), sets, ordered pairs and other tuples, functions, manifolds, projective spaces, Hilbert spaces, and whatnot. There are axioms asserting the basic properties of these and the relations between them. For example, there are axioms saying that the real numbers form a complete ordered field, that any formula determines the set of those reals that satisfy it (and similarly with other sorts in place of the reals), that two tuples are equal iff they have the same length and equal components in all positions, etc.

There are no axioms that attempt to reduce one sort to another. In particular, nothing says, for example, that natural numbers or real numbers are sets of any kind. (Different mathematicians may disagree as to whether, say, the real numbers are a subset of the complex ones or whether they are a separate sort with a canonical embedding into the complex numbers. Such issues will not affect the general idea that I'm trying to explain.) So mathematicians usually do not say that the reals are Dedekind cuts (or any other kind of sets), unless they're teaching a course in foundations and therefore feel compelled (by outside forces?) to say such things.

This theory T, large and unwieldy though it is, can be interpreted in far simpler-looking theories. ZFC, with its single sort and single primitive predicate, is the main example of such a simpler theory. (I've left large categories out of T in order to make this literally true, but Feferman has shown how to interpret most of category theory, including large categories, in a conservative extension of ZFC.)

The simplicity and efficiency of ZFC and the fact that T can be interpreted in it (i.e., that all the concepts of T have set-theoretic definitions which make all the axioms of T set-theoretically provable) have, as far as I can see, two main uses. One is philosophical: one doesn't need to understand the nature of all these different abstract entities; if one understands sets (philosophically) then one can explain all the rest. The other is in proofs of consistency and independence. To show that some problem, say in topology, can't be decided in current mathematics means to show it's independent of T. So you'd want to construct lots of models of T to get lots of independence results. But models of T are terribly complicated objects. So instead we construct models of ZFC, which are not so bad, and we rely on the interpretation to convert them into models of T. And usually we don't mention T at all and just identify ZFC with "current mathematics" via the interpretation.

I apologize for posting as an answer what should really be a comment, connected to one of Jacques Carette's comments on my earlier answer. Unfortunately, this is way too long for a comment. Jacques asked why we would bother with set-theoretic foundations at all. It happens that I wrote down my opinion about that about 15 years ago (in a private e-mail) and repeated some of it on the fom (= foundations of mathematics) e-mail list. Here's a slightly edited version of that:

Mathematicians generally reason in a theory T which (up to possible minor variations between individual mathematicians) can be described as follows. It is a many-sorted first-order theory. The sorts include numbers (natural, real, complex), sets, ordered pairs and other tuples, functions, manifolds, projective spaces, Hilbert spaces, and whatnot. There are axioms asserting the basic properties of these and the relations between them. For example, there are axioms saying that the real numbers form a complete ordered field, that any formula determines the set of those reals that satisfy it (and similarly with other sorts in place of the reals), that two tuples are equal iff they have the same length and equal components in all positions, etc.

There are no axioms that attempt to reduce one sort to another. In particular, nothing says, for example, that natural numbers or real numbers are sets of any kind. (Different mathematicians may disagree as to whether, say, the real numbers are a subset of the complex ones or whether they are a separate sort with a canonical embedding into the complex numbers. Such issues will not affect the general idea that I'm trying to explain.) So mathematicians usually do not say that the reals are Dedekind cuts (or any other kind of sets), unless they're teaching a course in foundations and therefore feel compelled (by outside forces?) to say such things.

This theory T, large and unwieldy though it is, can be interpreted in far simpler-looking theories. ZFC, with its single sort and single primitive predicate, is the main example of such a simpler theory. (I've left large categories out of T in order to make this literally true, but Feferman has shown how to interpret most of category theory, including large categories, in a conservative extension of ZFC.)

The simplicity and efficiency of ZFC and the fact that T can be interpreted in it (i.e., that all the concepts of T have set-theoretic definitions which make all the axioms of T set-theoretically provable) have, as far as I can see, two main uses. One is philosophical: one doesn't need to understand the nature of all these different abstract entities; if one understands sets (philosophically) then one can explain all the rest. The other is in proofs of consistency and independence. To show that some problem, say in topology, can't be decided in current mathematics means to show it's independent of T. So you'd want to construct lots of models of T to get lots of independence results. But models of T are terribly complicated objects. So instead we construct models of ZFC, which are not so bad, and we rely on the interpretation to convert them into models of T. And usually we don't mention T at all and just identify ZFC with "current mathematics" via the interpretation.