In category theory, a branch of mathematics, Mac Lane's coherence theorem states, in the words of Saunders Mac Lane, “every diagram commutes”.
[1] But regarding a result about certain commutative diagrams, Kelly is states as follows: "no longer be seen as constituting the essence of a coherence theorem".
#Counter-example), it states every formal diagram commutes, where "formal diagram" is an analog of well-formed formulae and terms in proof theory.
The theorem can be stated as a strictification result; namely, every monoidal category is monoidally equivalent to a strict monoidal category.
[3] It is not reasonable to expect we can show literally every diagram commutes, due to the following example of Isbell.
be a skeleton of the category of sets and D a unique countable set in it; note
be the projection onto the first factor.
Now, suppose the natural isomorphisms
are the identity; in particular, that is the case for
is the identity and is natural, Since
Similarly, using the projection onto the second factor, we get
In monoidal category
, the following two conditions are called coherence conditions: To satisfy the coherence condition, it is enough to prove just the pentagon and triangle identity, which is essentially the same as what is stated in Kelly's (1964) paper.
This category theory-related article is a stub.