Natural deduction and coherence for weakly distributive categories

• Published in: Journal of pure and applied algebra 1996-12, Vol.113 (3), p.229-296
• Main Authors: Blute, R.F., Cockett, J.R.B., Seely, R.A.G., Trimble, T.H.
• Format: Article
• Language: English
• ISSN: 0022-4049; 1873-1376
• DOI: 10.1016/0022-4049(95)00159-X

This paper examines coherence for certain monoidal categories using techniques coming from the proof theory of linear logic, in particular making heavy use of the graphical techniques of proof nets. We define a two sided notion of proof net, suitable for categories like weakly distributive categories which have the two-tensor structure ( times/par) of linear logic, but lack a negation operator. Representing morphisms in weakly distributive categories as such nets, we derive a coherence theorem for such categories. As part of this process, we develop a theory of expansion-reduction systems with equalities and a term calculus for proof nets, each of which is of independent interest. In the symmetric case the expansion-reduction system on the term calculus yields a decision procedure for the equality of maps for free weakly distributive categories. The main results of this paper are these. First we have proved coherence for the full theory of weakly distributive categories, extending similar results for monoidal categories to include the treatment of the tensor units. Second, we extend these coherence results to the full theory of ∗-autonomous categories — providing a decision procedure for the maps of free symmetric ∗-autonomous categories. Third, we derive a conservative extension result for the passage from weakly distributive categories to ∗-autonomous categories. We show strong categorical conservativity, in the sense that the unit of the adjunction between weakly distributive and ∗-autonomous categories is fully faithful.