A question, that if it has a known answer would probably have been settled long before electronically searchable media arose, came up in the project a student of mine is working on for his dissertation. Obviously the coherence theorem for symmetric monoidal categories applies to cartesian monoidal categories. The question is: Is there anything better? More specifically is anyone aware of (with a citation to where it is proved) a coherence theorem asserting a large class of diagrams commute in any cartesian monoidal category, or giving criteria for their commuting, when the diagrams are made not just prolongations of the monoidal structure maps, but also involve projections (or equivalently unique arrows to the terminal object 3D monoidal identity) or diagonals. (If the "or" turns out to be exclusive, I'd be happiest for a theorem including diagonals, but not projections, since those come up more in my student's work.) Of course I'd be happy with a modern-style coherence result, characterizing free cartesian monoidal categories, too, since we should be able to read off the "all-[these] diagrams commute" sort of theorem from it. Best Thoughts, David Yetter [For admin and other information see: http://www.mta.ca/~cat-dist/ ]