3 ms·

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

• zozbot234 1y ago
  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 1y ago
    Go to 2:04:00 at https://www.youtube.com/watch?v=0zBDNYRfdlU https://www.youtube.com/watch?v=0zBDNYRfdlU > Constructivism is a cancer in my view.
    • zozbot234 1y ago
      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.