[giraj]

I wouldn't be surprised to see anything related to type-theory on here. And I disagree that many people doing HoTT today are proposing it as an alternative foundation in anything except (categorical) homotopy theory, and I'd like to know where you see anyone doing that.

Intuitionism in HoTT isn't about constructivity, which I agree is rejected by mainstream mathematicians. It's about the models of the theory. For example, LEM doesn't hold in the category of bundles over the circle (see my other comment on here). If you think of the axiom of choice as "every surjection has a section", then this doesn't hold for topological spaces. (Take the double cover of the circle; there's no continuous section.) I disagree that these examples are uninteresting to mainstream mathematicians.