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