# "The purpose of being categorical is to make that which is formal, formally formal" what does it mean?

This is what J. Peter May said once about category theory:

The purpose of being categorical is to make that which is formal, formally formal.

and I have seen people reciting it. Yet, I am not too sure if I understand the wisdom behind it. I would appreciate if some one could elaborate that.

• He paraphrases Peter Freyd: "Perhaps the purpose of categorical algebra is to show that which is trivial is trivially trivial.", P. Freyd, Stable homotopy, Proceedings of a conference on categorical algebra (La Jolla, 1965), 121–172. Springer-Verlag. 1966. Can you give a source for May's quote for context? Nov 28, 2012 at 19:26

Let's consider a "formally formal" phenomenon arising from logic. Suppose we wanted to show that under some hypothesis $P$, either $Q$ or $R$ is true. Naively, one might try to prove this by splitting hypothesis $P$ into cases and showing that in each case we can deduce either $Q$ or $R$, but under the commonly accepted logical principles of mathematics, it is enough to prove that under hypothesis $P$, if $Q$ does not hold, then $R$ must be true. This is because the law of excluded middle tells us that either $Q$ is true or its negation is true: so no matter what hypothesis $P$ is, we can divide into the case where $Q$ is true and the case where $Q$ is false. Obviously, in the case $Q$ is true, we can deduce that either $Q$ or $R$ is true, and if we are able to give a proof of $R$ in the case $Q$ is false, then we can also deduce that either $Q$ or $R$ is true in that case. Since we can deduce either $Q$ or $R$ in both cases, we have the desired proof.
Why is the above "formally formal"? Because it is entirely meaningless: $P$, $Q$, and $R$ are arbitrary propositions, and without knowing what exactly they are, we have concocted a recipe for proving $P \to (Q \lor R)$. In other words, we have an argument that based entirely on form rather than substance.
In much the same way, category theory seeks to provide a general framework for extracting abstract commonalities between different mathematical contexts, so that we become able to make sense of assertions like this: "The proof of the snake lemma for diagrams of abelian sheaves is the same as the proof of the snake lemma for diagrams of $R$-modules, except everywhere we replace ‘$R$-module’ by ‘abelian sheaf’." So how do we make this precise? In this specific case, what we could do is note that the category of $R$-modules and the category of abelian sheaves are both examples of abelian categories, and that there is a proof of the snake lemma that works in any abelian category. In fact, the embedding theorem of Freyd and Mitchell can be used to show that the snake lemma for abelian categories follows from the snake lemma for $R$-modules – a result we could not possibly hope to have obtained without the abstraction afforded by the notion of abelian categories because an abelian sheaf isn't a special kind of $R$-module! (Contrast the assertion that "the proof of the snake lemma for abelian groups is the same as the proof of the snake lemma for $R$-modules" – in this case we can easily make sense of this, because an abelian group is literally the same thing as a $\mathbb{Z}$-module.)