A common style of proof in CT papers is to draw a huge commutative diagram, number some subset of the faces, and justify why each of these faces commute. However, such an argument alone doesn't imply that the overall diagram commutes. Consider for example a triangle of arrows with three additional arrows connecting each of the corners to a fourth object in the centre. It is very easy to find examples where the three little triangles commute, but not the big outside triangle. E.g. take the three inward-pointing arrows to be 0 morphisms, then we can take f,g,h to be arbitrary on the outside. So, my question is: Is there a simple way of judging soundness for a commutative diagram proof? One answer is to determine what constitutes a legal pasting of diagrams, then only admit those which were obtained inductively by legal pastings of commuting faces. However, its not immediately obvious that, given a diagram without such a decomposition into legal pastings, we can obtain the decomposition efficiently. Has this problem been studied formally somewhere? Best, Aleks [For admin and other information see: http://www.mta.ca/~cat-dist/ ]