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

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.