> There are also people like Per-Martin Lof who want to use HoTT…
Sorry, but this is plainly false.
Per does not want to use HoTT. My impression is that he finds HoTT mildly interesting, and has not really used/advocated it. And, you are implicitly calling him and Voedvodsky "not a mainstream mathematician", which is rather offensive considering their contributions to statistics (Per) and homotopy theory (Vladimir).
Your comment comes out as very reactionary. There is room for a lot of both HoTT (weather classical logic is used or not) and set theory in modern mathematics. In fact, doing set theory in HoTT is a very pleasant experience!
Martin-Lof went to at least one early HoTT conference and his interest is clearly in intuitionistic type theory, so I don't think my statement is inaccurate. Anyway, the broader point is that there's a community of people whose interest comes from that viewpoint.
I also don't think it's inaccurate or offensive to say Martin-Lof no longer works in mainstream mathematics. He hasn't done statistics since the 70s.
Voevodsky was of course a great mathematician, but it seems quite clear that his work in type theory was not mainstream mathematics and not of interest to most mathematicians (quantifying over, say, people who hold jobs as postdocs or professors in math departments worldwide). Whether the work is valuable is a separate question, but the sociological point is, imo, pretty inarguable.
Sorry, but this is plainly false. Per does not want to use HoTT. My impression is that he finds HoTT mildly interesting, and has not really used/advocated it. And, you are implicitly calling him and Voedvodsky "not a mainstream mathematician", which is rather offensive considering their contributions to statistics (Per) and homotopy theory (Vladimir).
Your comment comes out as very reactionary. There is room for a lot of both HoTT (weather classical logic is used or not) and set theory in modern mathematics. In fact, doing set theory in HoTT is a very pleasant experience!