Most undergraduates learn mathematics in the language of sets. If they're doing algebra, then the underlying structures of their groups, rings, etc. are always sets. Same for topology and logic (e.g. classical model theory). An extreme example of this set-theoretic thinking is defining the real numbers in terms of Dedekind cuts.
Category theory, very slowly, changes this perspective. If you study this for years, you will come to realise there is more to mathematics than sets. And your way of thinking will shift. You will learn to ask different questions. For example, instead of defining things in terms of their underlying set (often breaking symmetries), you will ask 'does it have a universal property?' and so on. Note, there are still tons of reasons to use sets / ZFC, even when working with categories mostly. But I do not want to get into that and it's irrelevant for the point I'm trying to make.
Final note: the 'language of sets', i.e. the language of undergraduate mathematics, is very different from set theory. 'Set theory' is like the language talking about itself. The same goes for pure category theory.
In the 20th century it became trendy to (a) try to base everything on set theory, (b) write mathematics in a very dry and formal style, taking inspiration from the Bourbaki project.
My impression is that undergraduates are taught in the language of sets partly because it is serviceable for describing the subjects they are trying to learn (esp. analysis) but also more importantly because mid-20th century mathematicians who set up the curriculum we are still using wanted to thoroughly teach (indoctrinate?) undergraduates the trendy style of the time.
Personally I think it has been a mixed bag; the style is a big turn-off to many people, and ends up chasing people out of mathematics who could otherwise make valuable contributions. The people who remain seem to mostly like it okay though. YMMV.
First, why the scare quotes around "rigorous"? Set theory literally did make the foundations of analysis more rigorous.
Second of all, we don't use set theory because it's "trendy" or because we want to "indoctrinate" undergraduates, we use it because it's the best known foundation for mathematics. If there was something less complicated or annoying that worked, we'd use that instead. But as far as we know, there isn't, and there are good reasons to believe we won't find something better.
But I've come to understand that I was not realizing that I didn't like mathematics or thought it was too hard, but instead that if I made that my life's work, I'd be working with many more people like that, rather than the people I wanted to - bright and creative, yet kind and humble.
I don't think set theory or any other set of tools is the problem behind potential academics getting turned off. It's the people, and the culture of glorified monkhood.
It is possible to use categories as basic building blocks instead if sets but, in my anecdotal experience, this us not what the majority of graduate programs in Mathematics do.
It will be interesting to see whether this will change in the next 20 yea.
This issue has been litigated extensively, and in my view successfully, by Harvey Friedman on the Foundations of Mathematics mailing list, if you want to check its archives.
The vast majority of mathematicians go their entire lives without using the word "category" in a paper. What are they missing out on?
One amusing problem is discussed here: https://mathoverflow.net/questions/289711/defining-sun-in-ho....
But suppose HoTT were equally good. What compelling reason is there for a working mathematician to learn it? We already know about set theory, and it meets all of our needs.
I also think it's important to point out for anyone reading that one certainly doesn't need category theory to do proof verification. Some other options, and some gripes with the Coq community along the lines of the previous paragraph, are listed here: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa....
Also, if your foundational theory doesn't allow me to (easily) define a fundamental geometric object like SU(n), then it's just a non-starter. Again, I have not been able to find a reason why we ought to endure such pain to do simple things when we already have a perfectly good foundational theory. Re: the HoTT book, it is precisely because I've looked at the book that I have these questions.
- Category theory has a number of very intuitive looking graphical notations which nevertheless translate to very exact algebraic expressions. This is pretty dang nice. Category theory is a road to a very principled formulation of things that are already done in dataflow languages, tensor diagrams, and UML and things like that. These graphical languages are a reasonable user facing interface.
- Empirically in mathematics, category theory has been found to be a flexible and "simple" language to describe and interconnect very disparate things. In programming terms that means that it is a plausible source of inspiration for consistent interfaces that can do the same.
- Point free DSLs are really nice to work with as library/compiler writer. It makes optimizations way easier to recognize and implement correctly. Named references are phantom links attaching different points in a syntax tree and make it hard to manipulate them correctly. In slightly different (and vague) terms, category theory gives a methodology to turn abstract syntax graphs into trees by making all links very explicit.
I can't comment much on what category theory contributes to mathematics, but I think there are similar points. I think category theory can make precise analogies between extremely disparate fields like logic, set theory, and linear algebra. I think categorical intuitions lead to clean definitions when specialized to some particular field. Combinatory categorical logic does make some aspects of logic less spooky.
Further, none of the proofs from an undergrad abstract algebra are going to be "easier" with categories. (Show me one?) At the end of the day, you have to prove the same propositions. Categories just give a different and sometimes more convenient language.
As for the second part, it's not that one single proof or another is easier with category theory. But the entire presentation is very elegant. Thinking of Aluffi Chapter 0 where he uses universal property extensively to simplify a lot of proofs. My personal favorite presentation of Algebra, but everyone has an opinion here.
Re: Aluffi, it's a fine book, but I'm not sure I'd teach it that way, because I'm not sure what introducing universal properties and so on really buys you at that level. I guess it make sense if you commit to getting to the end with the abstract perspective on homological algebra. But for a grad student just looking to pass his or her quals? The discussion in Hatcher is concrete, motivated, and involves zero category talk.
Being slightly facetious here as obviously Griffiths and Harris uses sheaves extensively and no category theory.
It's just I see a lot of category hype on here and I want to yell that it's mostly just linguistic! It's not some deep or scary thing. The analogy to matrix notation is really good.
Of course, all mathematics is abstraction, and all abstractions are leaky. Calculus just chooses not to study non-differentiable and non-integrable functions. Topology chooses not to study discontinuous transformations, and abstracts away the spatial metric.
In category theory, the property under study is compositionality: the property that given a path from A->B, and another from B->C, you have a path A->C. Of course, anyone who's ever written a computer program knows that this is not as guaranteed as it sounds. All abstractions are leaky, and if your "paths" are functions, in the programming sense, then the second one could throw an exception, leaving you high and dry with the intuitive transitive property being straight-up wrong. Likewise, if your "paths" are mathematical functions, composition can preserve continuity (f . g for continuous f and g is continuous), but if either one is discontinuous, the result will fail to be continuous.
So category theory abstracts away the "exceptions" and "discontinuities" by ruling them illegal: in a category of topological spaces and continuous functions, everything, by construction, preserves continuity. We thus have an entire field of mathematics devoted to asking and answering the question: "what sorts of properties are preserved under transitive composition in what sorts of settings?"
Category theory is useful for studying mathematical structures in general — by its nature, it’s results are going to be fairly abstract and general, but that doesn’t make it useless.
So more or less the history of mathematics was something like:
Geometry -> Analysis -> Set Theory -> Category Theory
Number theorists should not be discounted; they are a separate split after analysis and graph theory is technically more like number theory than category theory. Later on they come back and join category theory again. This is my own opinion and I say it because of the methods that they like to use. You have bridges between them in the form of things like algebraic geometry or functional analysis. Analysis also includes calculus and I would say set theory includes topology.
Now, I think your question was a sort of general question about why one should do category theory, but I think the best way is to answer it in two ways. A third point is added as an afterthought.
I) Does it lead to synergistic results? Yes, for example Cayley's theorem is an instance of the Yoneda embedding. You can embed any group injectively into the permutation group of the underlying set. But Yoneda is a bunch of other things at the same time too. So by doing the correct generalisation, you solve all the specifications thereof. And then sometimes when people say category theory is foundational, they mean that: Within a special type of category called a topos, you can do all of mathematics. 
II) Why should we use category theory in computer science? This is maybe the more relevant question for the audience and I would say we aren't using it. So yes, there are these monad like things in functional programming and functional programming has monoids (a monad is a higher dimensional monoid). But they don't use much of the mathematics that Grothendieck invented and also I haven't seen many posts on functional programming that mention Lawvere. My opinion is that we still haven't implemented the real insights of category theory and that functional programming is actually the extension into practice of maybe Church's lambda calculus, not category theory. In the same way that quantum mechanics has waited 50 years to start using category theory I think computer science doesn't use exactly category theory. I guess my point is that there is a difference between ideas percolating down and ideas being applied over. One area where I would like to see more formal methods being used is reactive programming. So for example, why can't your programming language be specified entirely in category theory? But I think the problem is not that category theory cannot be applied, it is that category theory is percolating to other fields; those fields are only glancing at the mathematics; and a lot of mathematicians can't program at all for that matter. I don't say this as a type of lament or apologetically; I think it's just a matter of time and the right commitment.
This is my own opinion and I would like to be disproven by top researchers that are experts in both category theory and functional programming. I also think it is that we are not always aware of which work is important until it has become important. And said differently: I think Excel probably has a very interesting reactive framework and I have never seen anything about that posted on HN. So the fact that no-one is mentioning it doesn't mean that it doesn't exist. (Could Excel's reactivity be undocumented?)
III) Does it end at category theory? This is not really a question, but more a footnote. I asked my supervisor this once and he answered (rather surprisingly quickly): Probably not, and probably it will look different. For example, a lot of category theorists have not even heard of something like the Langlands Project  and the Langlands group seem to also be looking for unifications of theories too. I also asked my supervisor about whether he knew the Langlands project and he just said "No," and he didn't seem to want to say anything else. I have read of lone mathematicians that have their own unique way of approaching mathematics. So it is more a case of: Take what you need, see where you can get. Personally, I would prefer to linger a while with category theory as you can get further with less than in something like traditional analysis (where you have perhaps a thousand rules for integrals).
 You can do all of mathematics in set theory and you can do set theory in category theory. A topos is like a generalised set theory where functions have taken preference as the route of abstraction. Topos theory is also the reason why I say that classical mathematics includes in it constructive mathematics, but that is another topic that seems to have a somewhat emotive history. The bottom line is that the logic you use to spend your money at the supermarket is not going to change when someone discovers something new in mathematics.
If you think about the quadratic formula, the Babylonians used it without having a way to write down the equation.
But, having mentioned the caveats, I think the answer is that we don't have a nice example yet for category theory. I personally think that the key application of category theory will be in quantum mechanics and in reactive behaviour of programs and formal methods around that. So, for example when you prove your program does something rather than testing it 1000 times. (You'll have to test it in any case due to things like implimentation bugs.)
  M. Johnson and R. Rosebrugh, Fibrations and universal view updatability, Theoretical Computer Science 388.1, 2007, 109–129.
Have you seen "Multi-Level Languages are Generalized Arrows" by Adam Megacz? https://arxiv.org/abs/1007.2885
dom and cod are the domain and codomain of a morphism. They are functions that given a morphism will return the object at the head or tail of the morphism.
I don't think that these articles are a very good self contained explanation of category theory. At the moment, I've been aiming at a supplement written in concrete python to something more thorough.
Bartosz Milewski's series https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
RydeHeard and Burstall - http://www.cs.man.ac.uk/~david/categories/book/book.pdf
Milewski, Fong, and Spivak's course - http://brendanfong.com/programmingcats.html
From a mathematical perspective:
MacLane, Awodey's book, Conceptual Mathematics by Lawvere and Schanuel.
I think I started from known Haskell names, some conventions that I may have absorbed from catlab.jl and other places, and some unthoughtful accidents. I really really wanted id to be the identity, but I'm pretty sure it's a python keyword. I added a d and vowed to never speak of it again. Ever written a program about schools and had to use the variable Klass?
I don't feel too bad about mplus and mzero. It's still pretty clear that they are something like plus and zero, but the m gives you pause. And it should, since in one case mplus is in fact multiplication.
If this was rolled out into a library maybe I'd have both long and short names? I'd never want a library to have only long names for really common things. cod and dom don't actually give me a seconds pause. I like them having the same length too. Makes code prettier and easier to read. I also intend to replace some things with operators which would be even more inscrutable to a newcomer. @ has to be compose for example (to mimic numpy).
It's a built-in function, but you can overload it within a scope you control without problems:
<built-in function id>
>>> id = 7
Good point! I take this part back.
As for having identifiers the same length, I know the urge, but usually find the superficial "elegance" it's not worth it.
Even different programming languages have different conventions (short identifiers fir C and Fortran, long ones for Java and C#), which reflect the habits and preferences of their creators and users.
Besides Category Theory, what other topics are worth reading about to broaden one's CS background? I write a lot of code without formal CS training so I was hoping to expose myself to interesting, preferably "mind-blowing" topics without having to take a course or go through the whole SICP.
I'm having a hard time thinking about a blog posts worth of content that is mind blowing. Mind blows tend to take more investment than that.
I'd recommend checking out an algorithms course https://ocw.mit.edu/courses/electrical-engineering-and-compu... This one is very good. Has free videos.
I'd recommend giving functional programming a try. I'm an FP fiend. I found SICP tough going though.
I'd recommend giving low level programming a try.
Learning prolog is pretty mind blowing http://www.learnprolognow.org/
Digital Circuitry is pretty mind blowing https://www.nand2tetris.org/
Making interpreters can be pretty mind blowing https://craftinginterpreters.com/contents.html
It also doesn’t even try to make the given code applicable to real problems. It seems as if someone writing an article of how to use functions.partial while never mentioning when those partials could be practically used.
All in all, 0 respect for the reader; seems like a badly typed retelling of a university course.