That might be a case of the author be really used to a certain crowd and writing for them. The work by Spivak on databases is well-known in ACT so the connection comes pretty easily. Also, in fairness, is pretty easy to Google your way around that claim.
> As a programmer and hobbyist math reader, I found category theory to be very unrewarding (and I gave up on it) because of the lack of interesting theorems and lemmas. My takeaway was that there's Yoneda lemma and really nothing interesting before you reach that. Like, CT describes a set of rules but very little emerges from those rules.
The fact it's so rare to find a counterintuitive fact in CT, so that you rarely find yourself proving something and you mostly spend your time constructing effective tools, it's a feature not a bug!
McBride's "Don't touch the green slime!" is a great paper/saying about this principle. Work with the compiler, not against it. The compiler is very dumb so it understands only trivial things.
There's a legacy pseudomachist culture of 'hard is good' in mathematics (but really, it's transversal to science) which rewards working hard and not working smart.
> As a programmer and hobbyist math reader, I found category theory to be very unrewarding (and I gave up on it) because of the lack of interesting theorems and lemmas. My takeaway was that there's Yoneda lemma and really nothing interesting before you reach that. Like, CT describes a set of rules but very little emerges from those rules.
This is correct. The only somewhat interesting result in Category theory is the Yoneda Lemma, everything else is machinery for diagram chasing. It's ubiquitous in the same way that short exact sequences are ubiquitous -- and about as interesting as short exact sequences.
I think most hobbyists or those who are intellectually curious would be better off studying physics or engineering first, and then picking up the math with applications along the way. For example, you can study multivariable calculus and then complex analysis, which naturally leads to questions of topology as you find try to solve integral equations, and then obstruction theory can come up. Lots of cool stuff to study that is actually interesting. I would never foist category theory on someone who finds math to be interesting and enjoyable -- that would be like throwing a match that just caught flame into the rain.
My formulation is "if it's not trivial, it's probably not good" when I implement the necessary functions for the "type class" (to take a haskellism) to work. If your `bind` implementation monad doesn't look like it could have been written by someone who just used the function types, it's probably not right. Thanks for the link to the mcbride-ism:
And students need not memorise the equation, instead they can derive it from another equally unintuitive equation then go through many logical steps of multiplication, simplification and refactoring - each being locations where students are likely to introduce errors.
This is not simpler for the student. Its is, at best, a simpler way to derive the equation, a thing which most people will never do.
