At least for the introductory category theory material that I have gone through, I have noticed that the hardest thing about proving something in category theory is understanding and unraveling the definitions, in order to figure out *exactly* what must be shown in order to prove a result. Once you get to that point, the results may flow almost automatically, like a computation.

(But: is it different, for proving something more substantial than an exercise, like the Yoneda lemma? Or is that proof just basically a more complex, but still inevitable, computation?)

In any case, the general trend towards abstraction -- which is paramount in category theory -- definitely does involve concentrating complexity in the definitions. It looks like once the definitions are made at their most appropriate general level of abstraction, then they are purified and some results which would otherwise look hard to show will follow almost automatically. If you can do the work of understanding what abstraction X means, and then showing that object Y is an X, then all the things that you know about X become automatic results that apply to Y.

Disclaimer: I haven't gotten very far with category theory -- that's why I'm here, working through it with the team -- so these general comments are more of a gut

assessment than an experienced judgement.

(But: is it different, for proving something more substantial than an exercise, like the Yoneda lemma? Or is that proof just basically a more complex, but still inevitable, computation?)

In any case, the general trend towards abstraction -- which is paramount in category theory -- definitely does involve concentrating complexity in the definitions. It looks like once the definitions are made at their most appropriate general level of abstraction, then they are purified and some results which would otherwise look hard to show will follow almost automatically. If you can do the work of understanding what abstraction X means, and then showing that object Y is an X, then all the things that you know about X become automatic results that apply to Y.

Disclaimer: I haven't gotten very far with category theory -- that's why I'm here, working through it with the team -- so these general comments are more of a gut

assessment than an experienced judgement.