In category theory, a branch of mathematics, Mac Lane coherence theorem states, in the words of Saunders Mac Lane, “every diagram commutes”.[1] 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.