If HoTT helps you prove theorems, great. In particular I could see it being of interest to people working in higher category theory (and such people have responded in other comments here!). My remarks were meant for the other 99% of mathematicians – most of whom go their entire lives without ever writing the word "category" in a paper.
> it's not clear to me why you necessarily want the language you use to rigorously investigate the foundations of mathematics to be the same one you use to do proof verification.
Among other things, I want theorems about foundations to be useful to non-foundational mathematicians. Working on type theory can improve, at the very least, formal verification tools. In my view, traditional ZFC-based mathematical logic has a much smaller likelihood of being useful for regular mathematicians. For example, the vast majority of mathematicians will never explicitly assume the existence of a large cardinal in a paper. It seems to me that the difference in usefulness is probably due to their relative distance from common discourse.
More generally, it's not clear to me why you necessarily want the language you use to rigorously investigate the foundations of mathematics to be the same one you use to do proof verification. ZFC – and set-theoretic approaches more broadly – facilitate proving things about mathematics (meta-mathematical theorems), and for that they are very useful. E.g., the strength of a theory is equivalent to the size of the cardinals it assumes, loosely speaking [1].
> Mainstream mathematicians are not being prevented from proving theorems because they lack "better ways of reasoning about equality of types."
How do you know? I've made the mistake of assuming that the definition of a certain morphism is natural with respect to a certain object when it wasn't (coevaluation in a rigid monoidal category). Better language for equality and naturality are precisely what HoTT provides. More importantly, the hope is that type theory will not only provide better language, but relieve us of the tedium of checking proofs by hand.
> The importance of ZFC is that it ensures our common language reasoning isn't incoherent.
I don't think this is true. AFAIK, no one has written down the definition of (say) a scheme from first principles in ZFC. In fact, if you care about coherence/verification, you should care even more about type theory. IIRC this is what drew Voevodsky to type theory in the first place -- https://mathoverflow.net/questions/234492/what-is-the-mistak...