The importance of category theory in mathematics seems wildly overestimated by HN, judging by the number of stories about it.
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.
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".)
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.
Textbook authors let some categorical language slip through so the time, and I think eductors are doing students a disservice my neglecting it. For instance, I was utterly confused about the "natural" isomorphism between a vector space and its double dual, as well as the "universal property" of tensor products, free modules, etc.. I also saw commutative diagrams in my complex analysis and topology books, but no one bothered to explain where they come from or what the rules are. Much later I finally took the time to study category theory on my own, and I can't help but think the whole experience would have been much more efficient had my professors exposed us to the idea of working with abstract morphisms much earlier.
I agree. When teaching, I try to choose my terms carefully so someone would not go astray from the subject matter. It is remarkable how easy it is to get stuck on a side-quest with looking up abstract terms, while-so missing the main topic. imo the graceful way to handle it is to drop references (and disclaimers in case they are time-consuming) when introducing new things.
Somehow math learning has the property that 'struggle with x, finish x. learn y. if I knew y before x it would've been so much smoother!' sounds correct, but in practice it often does not go so well.
An undergrad curriculum is expository in nature, the main goals being diversity of topics and developing a maturity.
Maturity is the biggest prerequisite to approaching cat theory imo. Similarly, without examples and non-examples from various fields, cat theory will feel like esperanto for its own sake. Given this, cat theory should not fall into undergrad territory, but will be present in any grad program.
Categories should show up naturally in Algebra/Algebraic topology, and not much elsewhere (in undergrad). Saying 'category of vector spaces over k' in a (linear) algebra course is effectively a waste of breath due to how little additional insight it provides.