Honest application of category theory I believe that category theory is one of the most fundamental theories of mathematics, and is becoming a fundamental theory for other sciences as well. It allows us to understand many concepts on a higher, unified level. Categorical methods are general, but of course they can be applied to specific categories and thereby help us to solve specific problems. I am not asking for canonical applications in which category theory is used. I have read all answers to similar math.SE questions on applications of category theory, but they don't fit to my question below. I would like to ask for applications of the notions of "category", "functor", and "natural transformation" (perhaps also "limit" and "adjunction") , which go beyond descriptions, but really solve specific problems in an elegant way. I am aware of many, many proofs of theorems which have category-theoretic enhancements, in particular by means of the Yoneda Lemma, but I'm not looking for these kind of applications either. So my question is (even though I know that this is not the task of category theory):

Can you name a specific and rather easy to understand theorem, whose statement naturally does not contain any categorical notions, but whose proof introduces a suitable category / functor / natural transformation in a crucial way and uses some basic category theory? The proof should not just depend on a large theory (such as arithmetic geometry) whose development has used category theory over decades. The proof should not just be a categorical version of a proof which was already known.

So here is an example of this kind, taken from Hartig's wonderful paper "The Riesz Representation Theorem Revisited", and hopefully there are more of them: Let $X$ be a compact Hausdorff space, $M(X)$ the Banach space of Borel measures on $X$ and $C(X)^*$ the dual of the Banach space of continuous functions on $X$. Integration provides a linear isometry
$$\alpha(X) : M(X) \to C(X)^*, ~ \mu \mapsto \bigl(f \mapsto \int f \, d\mu\bigr).$$
The Riesz Representation Theorem asserts that this is an isomorphism. For the "categorical" proof, observe first that the maps $\alpha(X)$ are actually natural, i.e. provide a natural transformation $\alpha : M \to C^*$. Using naturality and facts from functional analysis such as the Hahn-Banach Theorem, one shows that if $X$ satisfies the claim and admits a surjective map to $Y$, then $Y$ satisfies the claim. Since every compact Hausdorff space is the quotient of an extremally disconnected space, namely the Stone-Cech-compactification of its underlying set, we may therefore assume that $X$ is extremally disconnected. Now here comes the actual mathematics, and I will just say that there are enough clopen subsets which allow you to construct enough continuous functions. The general case has been reduced to a very easy one, using the concept of natural transformation.
 A: Here are two proofs that both involve recognizing that a big category is the ind- or pro-category of a smaller category, and then proving something about the smaller category to get it for the bigger category. 

Theorem: The Pontryagin dual $\text{Hom}(A, S^1)$ of a torsion abelian group $A$ is a profinite abelian group and vice versa; these two maps are inverses to each other on isomorphism classes. 

Proof. We will in fact prove a contravariant equivalence of categories. The category of torsion abelian groups is the category $\text{Ind}(\text{FinAb})$ of ind-objects in finite abelian groups, while the category of profinite abelian groups is the category $\text{Pro}(\text{FinAb})$ of pro-objects in finite abelian groups, so it suffices to show that Pontryagin duality is a contravariant equivalence of categories from $\text{FinAb}$ to itself. But this is clear: the Pontryagin dual of the finite cyclic group $C_n$ of order $n$ is (noncaonically) $C_n$ again, and Pontryagin duality respects direct sums. $\Box$

Theorem (Stone's representation theorem): Every Boolean ring $B$ is the Boolean ring $\text{Hom}(X, \mathbb{F}_2)$ of clopen subsets on a profinite space $X$, the Stone space $\text{Hom}(B, \mathbb{F}_2)$ of $B$.

Proof. We will in fact prove a contravariant equivalence of categories. The category of Boolean rings is the ind-category of finite Boolean rings, while the category of profinite spaces is the pro-category of finite sets, so it suffices to show that taking continuous functions to $\mathbb{F}_2$ resp. taking the Stone space is a contravariant equivalence of categories from finite Boolean rings to finite sets. But it's straightforward to prove by induction on the cardinality that every finite Boolean ring is $\mathbb{F}_2^X$ for some finite set $X$ and that it has Stone space $X$. $\Box$
A: Does the following standard proof of the Brouwer fixed point theorem for the two-dimensional disk $D$ count?
Theorem. Any continuous map $f : D \to D$ has a fixed point.
Proof. If $f$ had no fixed point, the map $g : D \to \partial D$ given by $g(x) = \partial D \cap ($ray from $f(x)$ to $x)$ would be a retraction of $D$ onto $\partial D$, that is, $g \circ i = 1_{\partial D}$  where $i : \partial D \to D$ is the inclusion. This implies, by functoriality of $\pi_1$, that $g_\ast \circ i_\ast = 1_{\pi_1(\partial D)}$ which is impossible since $\pi_1(D) = 0$, $\pi_1(\partial D) = \mathbb{Z}$.
A: A nice example from the area of computer science would be John C. Reynolds "Polymorphism is not set-theoretic" (available here: https://hal.inria.fr/inria-00076261/document). The point is that second-order $\lambda$-calculus does not have set-theoretic models (there is a rather natural definition in the paper of what it means to be "set-theoretic").
The proof is by contradiction: we assume the existence of a set-theoretic model, which allows us to define an initial $T$-algebra $\mu T$, where $T$ is a $\mathbf{Set}$-endofunctor:
$$TX = (X \to \mathbb B) \to \mathbb B$$
for a set $\mathbb B$ with $|\mathbb B| \geq 2$. Lambek's lemma says that the action of this initial algebra is an isomorphism, hence
$$|\mu T| \cong |(\mu T \to \mathbb B) \to \mathbb B|$$
which is obviously a contradiction.
The proof is directed by the categorical "approach" to the concept of initiality, and thus has a very categorical feeling, even though there is nothing categorical in the formulation of the theorem or the definition of what it means to be set-theoretic.
A: Here is one example, very classical probably. I hope it counts for your purposes!

Proposition. The fundamental group of a topological group $(G,\ast,e)$ is abelian.

Proof. The fundamental group $\pi_{1}$ is a functor from topological spaces to groups which preserves products, so that it sends group objects into group objects. A topological group is a group in the category of topological spaces and is thus sent via $\pi_{1}$ to a group object in the category of groups, i.e. to an abelian group.
A: You can prove the Poincare Lemma by reducing categorically/homotopy-theoretically to the case of a point. Proof: (re-)state the Poincare lemma (every closed form on a contractible subdomain of $\mathbb{R}^n$ is exact) as a statement about De Rham cohomology, and prove that the De Rham cohomology functor sends homotopy equivalences to isomorphisms. I seem to recall learning the Poincare lemma before learning about homotopy invariance, but apparently it's not necessary to go in that order.
A: I don't know if this fits as an answer, but I think that Michael Barr's existence of free groups is a nice application of some basic category theory.
A: ( This one is from applied mathematics, not theoretical one as all other above!) Take for example a structure where You have a person travelling from New York to San Francisco. CIA is collecting informations about this person, but they are from various sources of information: tickets, credit card records, mobile phone triangulations, wifi access from various places, information form residents in some places etc. All of this informations are in fact functions on different domains ( some of them assigns person to his position - like direct observation, whilst another only in indirect manner - for example plane ticket or wifi data connected with phone imei number). Some of this information may even be lousy related to that person - like not so certain observation of similar car on street camera monitoring.
We put all of this in big data database.
What structure data sources ( reflected in data store) must have in order to perform basic tracking of position of such person and perform some basic operations on it?
The answer is: it mus be a (pre) sheaf - which I found very amusing and interesting.
Take a look here: https://www.youtube.com/watch?v=b1Wu8kTngoE
