[spekcular]

They don't show up much elsewhere even in research-level mathematics. Unless you're doing something related to algebraic geometry or algebraic topology, there's a 95% chance they're a waste of time. The stuff in the linked article is relevant mainly to homotopy theorists.

The importance of category theory in mathematics seems wildly overestimated by HN, judging by the number of stories about it.

[zozbot234]

> The stuff in the linked article is relevant mainly to homotopy theorists.

HoTT makes homotopy theory relevant to the foundations of mathematics. So every mathematician encounters this stuff in some way. It clarifies what it means for mathematical structures to be isomorphic, and what exactly one is doing when treating isomorphisms by analogy with equality, which is often dismissed as an "abuse of notation" but is something that practically everyone does in math.

[AnimalMuppet]

> HoTT makes homotopy theory relevant to the foundations of mathematics.

OK.

> So every mathematician encounters this stuff in some way.

I doubt that. First, not every mathematician cares all that much about foundations. If you're using differential equations in mathematical biology, how much do you actually care about foundations? And second, even if you do care about foundations, HoTT isn't the only possible foundation, nor is it the most common one. You could care about foundations and base those foundations on ZFC without giving a rip about HoTT.

So... I don't buy it. (Unless by "encounters in some way" you mean "hears it in hallway conversations" or "skims journal articles about it now and then".)

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