= Solution
I would defend the assertion as a description of what good abstraction achieves, provided it is not taken to mean that finding the abstraction is easy. <Category theory> makes recurring arguments consequences of a common <universal property>, instead of requiring a new calculation in every setting.
The <Yoneda lemma> is an instructive example. A <natural transformation> from $\mathcal C(c,-)$ to a set-valued functor $F$ is determined by its value on $1_c$; naturality forces its value at $u:c\to d$ to be $F(u)$ of that element. Once the right question is asked, the proof is short. Yet the statement explains why representable functors encode objects faithfully, and why a functor can be reconstructed from its elements. The simplicity belongs to the organized argument, not to a claim that these consequences were obvious beforehand.
Likewise, the fact that a <right adjoint> preserves <categorical limits> does not need separate proofs for products, equalizers and pullbacks in every example. The <adjunction> converts a map into the proposed limit into a compatible family of maps, and the <natural bijection> converts that family back. This one argument explains preservation of many different constructions. It also makes the canonical comparison maps clear, which matters more than merely guessing an isomorphism of the resulting objects.
The <monoidal coherence theorem> shows a different benefit. Complicated calculations with bracketed <tensor products> can become transparent because every structural rebracketing is the unique map between its formal source and target. However, the proof that the pentagon and triangle suffice is real work. Suppressing brackets is justified by that proof; it cannot serve as a substitute for it. Abstraction is valuable precisely because it separates an essential compatibility argument from subsequent routine bookkeeping.
There is also a necessary caution. The <general adjoint functor theorem> requires a <solution-set condition>; small-limit preservation by itself does not produce a left adjoint. The reverse-ordinal example makes the missing condition concrete. Similarly, the <monad> of an adjunction need not capture all the structure in the original category: the tower of <nested partial unary operation categories> has arbitrary finite <monadic length>, despite its long composites sharing their first induced monad. These examples prevent formal language from hiding a size problem or an unjustified reconstruction claim.
\b[The persuasive interpretation is that abstraction makes the reason for a result visible and reusable.] It often turns the final step into a direct consequence of definitions, while leaving the discovery of those definitions and the verification of their hypotheses as substantial mathematics.
Back to article page
