[spekcular]

HoTT is not really relevant to the study of the foundations of mathematics, in the sense that it does not help solve the questions considered important or interesting by the foundations/metamathematics community. The best they can say is basically that they came up with a theory that is mutually interpretable with ZFC, and in their opinion more aesthetically pleasing, which sort of misses the point. The purpose of ZFC isn't to be aesthetically pleasing or "capture how mathematicians actually think" or anything like that, it's to facilitate proving metamathematical theorems.

Also, people understood isomorphisms quite well decades before HoTT was invented.

I hear these talking points repeated often enough on HN that it makes me think I should write a centralized debunking of them and just link it every time a HoTT story hits the front page.