[zero-sharp]

>Say I want natural numbers, I need to choose a concrete implementation in set theory

In what situation do you ever actually need a set theoretic foundation of the natural numbers to get work done?

[Atiscant]

As noted in another reply, the natural numbers example is contrived, but illustrative. Nevertheless, if you have a set theoretical foundation, e.g. ZF/C, at some point you need to define what you are doing in that foundation. Most mathematicians do not and happily ignore the problem. That works until it dont. The whole reason Vladimir Voevodsky started work on HoTT and univalent foundations was that he believed we in fact DO need to be able to pull definitions back to foundations and to verify mathematics all the way down.