> Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations.
Yes, but only the foundations. A math undergrad doesn't actually care whether an ordered pair (a, b) is encoded as {{a},{a,b}} or as an instance of the product type, and they don't care whether the natural number 2 is encoded as the set {{},{{}}} or as a value S(S(Z)) of the inductive type of the natural numbers. Although if pressured to choose, I bet they'd prefer the latter, since it gets a lot closer to how everyone thinks of "ordered pairs" and "natural numbers".
Since mathematicians always work with higher-level abstractions anyway, I don't think the fact that the very lowest layer of these abstractions is set theory actually gets in the way of formalization efforts.
Yes, but only the foundations. A math undergrad doesn't actually care whether an ordered pair (a, b) is encoded as {{a},{a,b}} or as an instance of the product type, and they don't care whether the natural number 2 is encoded as the set {{},{{}}} or as a value S(S(Z)) of the inductive type of the natural numbers. Although if pressured to choose, I bet they'd prefer the latter, since it gets a lot closer to how everyone thinks of "ordered pairs" and "natural numbers".
Since mathematicians always work with higher-level abstractions anyway, I don't think the fact that the very lowest layer of these abstractions is set theory actually gets in the way of formalization efforts.