 # Teorema di coerenza di Mac Lane

In category theory, a branch of mathematics, Mac Lane coherence theorem states, in the words of Saunders Mac Lane, “every diagram commutes”. More precisely (cf. #Counter-example), it states every formal diagram commutes, where “formal diagram” is an analog of well-formed formulae and terms in proof theory.

## Counter-example

It is not reasonable to expect we can show literally every diagram commutes, due to the following example of Isbell.

Let {\displaystyle {\mathsf {Set}}_{0}\subset {\mathsf {Set}}} be a skeleton of the category of sets and D a unique countable set in it; note {\displaystyle D\times D=D} by uniqueness. Let {\displaystyle p:D=D\times D\to D} be the projection onto the first factor. For any functions {\displaystyle f,g:D\to D} , we have {\displaystyle f\circ p=p\circ (f\times g)} . Now, suppose the natural isomorphisms {\displaystyle \alpha :X\times (Y\times Z)\simeq (X\times Y)\times Z} are the identity; in particular, that is the case for {\displaystyle X=Y=Z=D} . Then for any {\displaystyle f,g,h:D\to D} , since {\displaystyle \alpha } is the identity and is natural,

{\displaystyle f\circ p=p\circ (f\times (g\times h))=p\circ \alpha \circ (f\times (g\times h))=p\circ ((f\times g)\times h)\circ \alpha =(f\times g)\circ p} .

Since {\displaystyle p} is an epimorphism, this implies {\displaystyle f=f\times g} . Similarly, using the projection onto the second factor, we get {\displaystyle g=f\times g} and so {\displaystyle f=g} , which is absurd.