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