Coherence

Take a category. Now add a tensor product. Slap in a unit for the tensor product. Add a dose of associativity for the tensor product. While you're at it, stir in some commutativity also. Fold in some diagrams saying that the associativity, commutativity and unit behave properly. What you have now is a symmetric monoidal category. This is the basic building block for making categorical semantics of substructural logics such as, say, linear logic.

If you're smart as a whip, you'll be able to prove a coherence theorem. In grandiose wording, this says that "every diagram commutes". More down to earth, any diagram built only out of the associativity, commutativity and unit maps commutes. This was first formulated and proven by Kelley and Mac Lane in response to a question of Steenrod (when is there a canonical map between modules of certain "shapes" over a fixed ring). First, those Cat maniacs formulated the problem in terms of monoidal categories (heck, they cooked up the categories on the spot!). Then they ran into a bit of a problem. Sure, there are some shapes that have a canonical map between them. The problem, however, is constructing the map. Generally you need to compose together a few maps to get it. Only, sometimes an intermediate shape appears in the composition which is in neither the domain nor codomain. And this object's size is unbounded. Oh, woe is canonicity!

Notice something there? This is precisely the same as the situation with the cut rule. The problem with it is that it leads to intermediate formulae of unbounded size in the proof. Kelley and Mac Lane noticed this analogy, but were not able to make it into anything more than just an analogy. Instead, they proved coherence by defining a notion of a constructible map and proving that every canonical map is constructible. Sounds familiar, eh? This is precisely the point of cut elimination.

Now, via Kreisel, Mac Lane started up a correspondence with Grigori Mints, who was still in the Soviet Union at the time. Mints was able to turn the analogy with cut elimination into more than just an analogy. He showed Mac Lane how the terms arising in a monoidal category are, for all intents and purposes, the same as the terms arising in a certain relevant logic. By proving cut elimination for this logic, Mints was able to conclude coherence immediately! For a short summary of the correspondence between Mac Lane and Mints, see:

"Why Commutative diagrams coincide with equivalent proofs", Saunders Mac Lane, Contemporary Mathematics vol 13, 1982; 387--401

In short, if you have any interest in proof theory and have not read this article yet, then what are you doing still sitting at your computer? Go get it!

What blew me away with this article is that it pretty much covers most of the category theory wizardry used in (exponential free) linear logic, but predates Girard's paper by 5 years. Moreover, the stuff that it speaks about happened way before the article itself was published! Crazy!