Coherence of the Double Involution on *-Autonomous Categories

by J.R.B. Cockett, M. Hasegawa and R.A.G. Seely

This paper is available from the authors' pages

and might be of some interest for those woking on proof theory/type theory and semantics of Linear Logic. It addresses the following "coherence" question.

Many formulations of proof nets and sequent calculi for Classical Linear Logic (CLL) take it for granted that a type A is "identical" to its double negation A^{\bot\bot}. On the other hand, it has been assumed that *-autonomous categories are the appropriate semantic models of (the multiplicative fragment of) CLL. However, in general, in a *-autonomous category an object A is only "canonically isomorphic" to its double involution A^{**}. This raises the questions whether *-autonomous categories do not, after all, provide an accurate semantic model for these proof nets and whether there could be semantically non-identical proofs (or morphisms), which must be identified in any system which assumes a type is identical to its double negation.

Fortunately, there is no such semantic gap: in this paper we provide a "coherence theorem" for the double involution on *-autonomous categories, which tells us that there is no difference between the up-to-identity approach and the up-to-isomorphism approach, as far as this double-negation problem is concerned. This remains true under the presence of exponentials and/or additives. Our proof is fairly short and simple, and we suspect that this is folklore among specialists, though we are not aware of an explicit treatment of this issue in the literature.

Robin Cockett
Masahito Hasegawa
Robert Seely