 | This article needs attention from an expert in Mathematics. The specific problem is: the page doesn't explain what the theorem says (see talk page). (June 2025) |
In category theory, a branch of mathematics, Mac Lane's coherence theorem states, in the words of Saunders Mac Lane, “every diagram commutes”.[1] This result was once thought to be the essence of the coherence theorem, but regarding a result about certain commutative diagrams, Kelly argued that, "no longer be seen as constituting the essence of a coherence theorem".[2][3] 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.
The theorem can be stated as a strictification result; namely, every monoidal category is monoidally equivalent to a strict monoidal category.[4]
- ^ Mac Lane 1998, Ch VII, § 2.
- ^ Kelly 1974, 1.2
- ^ Power 1989, 1. Introduction
- ^ Schauenburg 2001