A question, that if it has a known answer would probably have been settled long before electronically searchable media arose, came up in
Dear David, Zoran Petric's paper "Coherence in substructural categories", Studia Logica 70 (2002) pages 271-296. Paul On 17/03/15 14:25, David Yetter wrote: 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
-- Paul Blain Levy School of Computer Science, University of Birmingham http://www.cs.bham.ac.uk/~pbl [For admin and other information see: http://www.mta.ca/~cat-dist/ ]