Coherence for star-autonomous categories

DOI10.1016/J.APAL.2005.11.003MaRDI QIDQ2498908zbMATH OpenOpenAlexFDO

Publication date 16 August 2006

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/math/0503306

categorical coherence cut elimination star-autonomous categories symmetric monoidal closed categories

Cut-elimination and normal-form theorems (03F05) Categorical logic, topoi (03G30) Foundations, relations to logic and deductive systems (18A15) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Abstract: This paper presents a coherence theorem for star-autonomous categories exactly analogous to Kelly's and Mac Lane's coherence theorem for symmetric monoidal closed categories. The proof of this theorem is based on a categorial cut-elimination result, which is presented in some detail.

Review text

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.

Recommendations

Cites work

Cited in

(13)

This page was built for publication: Coherence for star-autonomous categories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2498908)