A coherence theorem question

A coherence theorem question

[David Yetter]

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/ ]

Re: A coherence theorem question

[Paul B Levy]

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:

> 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

-- 
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/ ]