[zozbot234]

Kevin Buzzard (a standard mathematician who has direct expertise in the sorts of things HoTT is supposed to help with) argues that we simply don't know yet. See the references I previously mentioned in https://news.ycombinator.com/item?id=44151283

[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...

[zozbot234]

> 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.

[YetAnotherNick]

In podcasts or open conversation he is far more critical of HoTT.

[zozbot234]

Do you have a reference for that, such as a podcast link? His paper on Grothendieck's use of equality is implicitly rather critical of HoTT proponents' claims anyway (which is why I linked that too), but I'm curious to know if he has publicly said anything more specific than that.

[YetAnotherNick]

Go to 2:04:00 at https://www.youtube.com/watch?v=0zBDNYRfdlU

> Constructivism is a cancer in my view.

[zozbot234]

Thanks for the reference! That take of his sounds a bit confused in-context (univalence and constructivism are not directly related, you can work non-constructively and still use the overall featureset of HoTT/univalence) but then his remark about how he's just working on non-constructive stuff that we don't even know how to phrase constructively is just fair.

Relatedly, the kind of philosophical constructivism that would make claims like "non-constructive mathematics is just wrong and useless" has been a bit problematic in many ways, he's not totally off-base about this.

I disliked his skepticism about proofs-as-programs the most, but that's because I think "a direct proof is a program" is very much a worthwhile statement. Of course some mathematicians will opt not to care about that.