> But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics.
Most mathematicians spend very little time thinking about the foundations of mathematics though, so I'd take that with a grain of salt. ;)
Seriously though, I think the statement that "all of modern mathematics can be formalized in ZFC" is probably wrong. There have been attempts to do just that (e.g., Bourbaki), but they invariably failed and ended up with extensions of ZFC (e.g., for category theory) or just silently started using higher-order logic.
Type theory seems to be a lot more practical. Both because it is explicitly designed to be an open system (a closed system must fail eventually due to Gödel arguments) and because similar formalization efforts go a lot more smoothly. For example, compare the treatment of category theory in the HoTT book with any introductory text using set theory.
Most mathematicians spend very little time thinking about the foundations of mathematics though, so I'd take that with a grain of salt. ;)
Seriously though, I think the statement that "all of modern mathematics can be formalized in ZFC" is probably wrong. There have been attempts to do just that (e.g., Bourbaki), but they invariably failed and ended up with extensions of ZFC (e.g., for category theory) or just silently started using higher-order logic.
Type theory seems to be a lot more practical. Both because it is explicitly designed to be an open system (a closed system must fail eventually due to Gödel arguments) and because similar formalization efforts go a lot more smoothly. For example, compare the treatment of category theory in the HoTT book with any introductory text using set theory.