Honest application of category theory

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

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.