In this paper certain proof-theoretic techniques of [BCST] are applied to non-symmetric linearly distributive categories, corresponding to non-commutative negation-free multiplicative linear logic (mLL). First, the correctness criterion for the two-sided proof nets developed in [BCST] is adjusted to work in the non-commutative setting. Second, these proof nets are used to represent morphisms in a (non-symmetric) linearly distributive category; a notion of proof-net equivalence is developed which permits a considerable sharpening of the previous coherence results concerning these categories, including a decision procedure for the equality of maps when there is a certain restriction on the units. In particular a decision procedure is obtained for the equivalence of proofs in non-commutative negation-free mLL without non-logical axioms.
Keywords: categorical proof theory, linear logic, monoidal categories.
1991 MSC: 03B60, 03F05, 03F07, 03G30, 18D10, 18D15.
Theory and Applications of Categories, Vol. 6, 1999, No. 9, pp 105-146.
http://www.tac.mta.ca/tac/volumes/6/n9/n9.dvi
http://www.tac.mta.ca/tac/volumes/6/n9/n9.ps
http://www.tac.mta.ca/tac/volumes/6/n9/n9.pdf
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n9/n9.dvi
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n9/n9.ps