(Disclaimer: I'm a mathematician working in HoTT and (higher) category theory.)
Like with most advanced concepts in any field, there are lots of misunderstandings pertaining to HoTT. To me, the underlying insight is that the "right" abstract setting for a lot of classical homotopy theory is that of an infinity-topos (whose precise definition is an open question, but we have candidates). Theorems proven in HoTT hold in any infinity-topos, and HoTT is (conjecturally) the internal language of these.
For anything outside of homotopy theory, HoTT isn't (immediately) interesting. It's certainly not trying to provide foundations for set-based mathematics, but for (categorical) homotopy theory, sure.
Some mathematicians take issue with the logic being intuisionistic; e.g. neither the law of the excluded middle, nor double negation hold in HoTT. This is not about constructivity (which I agree, mainstream mathematicians will reject), but about the spaces being modeled. For example, a mainstream mathematician will say that a space is either empty or has a point. However, in the category of bundles over the circle, points are sections; and so the double cover doesn't have any point, for example. Neither is it empty.
(Disclaimer: I'm a mathematician working in HoTT and (higher) category theory.)
Like with most advanced concepts in any field, there are lots of misunderstandings pertaining to HoTT. To me, the underlying insight is that the "right" abstract setting for a lot of classical homotopy theory is that of an infinity-topos (whose precise definition is an open question, but we have candidates). Theorems proven in HoTT hold in any infinity-topos, and HoTT is (conjecturally) the internal language of these.
For anything outside of homotopy theory, HoTT isn't (immediately) interesting. It's certainly not trying to provide foundations for set-based mathematics, but for (categorical) homotopy theory, sure.
Some mathematicians take issue with the logic being intuisionistic; e.g. neither the law of the excluded middle, nor double negation hold in HoTT. This is not about constructivity (which I agree, mainstream mathematicians will reject), but about the spaces being modeled. For example, a mainstream mathematician will say that a space is either empty or has a point. However, in the category of bundles over the circle, points are sections; and so the double cover doesn't have any point, for example. Neither is it empty.