Why are there seemingly so many who want to use ETCS, or HoTT, or similar as a foundation of mathematics? I'm aware that HoTT has a good few good aspects, but that doesn't entirely explain the strong desire to find something other than ZFC to use, so I ask:
What is actually wrong with ZFC that drives this desire?
I've heard a few arguments already, though they were a bit vague - I'll list them below.
As all the objects of ZFC are sets, in ZFC questions such as "is $\pi \in 3$" may be asked, and for some reason just the fact that that may be asked is a problem...but I can't really see the issue. You never need to ask those questions so where would they cause a problem?
Another argument is that ZFC has too much "baggage" caused by the cumulative hierarchy - we don't want to have to worry about the set theoretical aspects of the elements of the real numbers, for example. This, again, is lost on me - can anyone give an example of where we ever actually feel the need to say anything at all about such aspects? Surely once you've got your definitions and you have a few properties that you want you can proceed to deduce using only those properties and may safely ignore those you don't want to think about?
You'll never get a false theorem from ignoring an axiom - when one proves something about groups in general it does not matter what extraneous properties individual groups have, they follow the group axioms so the conclusion is valid. Similarly we know what properties we want the real numbers to have, so surely we can deduce from those without any real issue once we have an object with those (though possibly other) properties?
- The last apparent issue I'll mention is categories. Apparently ZFC (let's assume with Universes) is a headache for category theorists. Something about ZFC makes category theory harder than it would be in, say, homotopy type theoretic foundations. So far all I've seen is hand waving - can anyone give an example of where ZFC(+U) truly makes life so much more difficult for category theorists? What is the problem?
I know that this is a negative post, asking what is wrong with ZFC rather than what is right about HoTT, ETCS, etc, it's just that I've seen many vague references from those disgruntled with the set theory, but not yet any concrete grievances.
As with many of my unusual questions, the tags are guesswork.