Comment by ncfavier
There arguably has been a failure of communication between type theorists and "traditional" mathematicians, but Buzzard unfortunately has a bit of a history of vocally spreading less-than-accurate information about type theory. I'd suggest not focusing too much on this one person's opinions and engaging with the subject for yourself if it interests you.
It's also worth keeping in mind that mathematicians traditionally haven't cared too much about foundations, and are not necessarily the best people to ask about them; see Hilbert, Bourbaki and the scorning of logic¹. Among people who are interested in foundations (logicians, category theorists, computer scientists, philosophers, ...), there is a pretty clear consensus that HoTT is a major step forward; but of course it's not the kind of "step forward" with immediate, observable results. As David Madore puts it, you wouldn't cut the roots of an apple tree just because no apples grow there.
[1] https://web.archive.org/web/20210506180228if_/https://www.dp...
> but of course it's not the kind of "step forward" with immediate, observable results.
Nice, it looks like you agree with Kevin Buzzard's claim about HoTT in the presentation I linked above. While mathematicians as a whole have historically not cared all that much about the practicality of formal foundations, it's worth noting that Kevin Buzzard has quite some expertise in dealing with the Grothendieck-style fuzzy, informal reasoning about equality that happens to be a key motivation behind HoTT itself and the univalence approach. What he seems to claim on the topic is that HoTT makes it a tiny bit easier to phrase a formal treatment of these issues, but you still have to do all the really hard work of proving that everything "respects" the equalities you claim it respects. The fact that you can then "transport" mathematical objects, proofs etc. along equalities is nifty but is also the kind of thing that would be glossed over to begin with in any informal treatment, so there's no real gain wrt. that.