Coherence for star-autonomous categories (Q2498908)

The paper contains a coherence theorem for *-autonomous categories (in the sense of Barr) exactly analogous to Kelly and Mac Lane's coherence theorem for symmetric monoidal closed categories. The *-autonoumous categories may be seen as symmetric monoidal closed categories that have a dualizing object. This situation is sufficiently common in algebraic examples and explains why *-autonomous categories attracted considerable interest. The paper is not completely self-contained, it is connected with many papers based on proof-theoretical approaches to coherence. The proof is based on a categorical cut-elimination result, which is presented in some detail. A ``pedagogically'' commendable aspect of this paper is that many useful notions, often used in such coherence proofs and their connections are clearly and compactly described: several categories based on propositional languages (with \(\vee, \wedge, \neg\) or \(\rightarrow, \wedge\) as connectives), related categories of graphs, the general notion of proof-net category and proof-net functor, etc. In the same vein, many technical results concerning the connections between these data (faithfullness of certain functors, etc.) are included.