From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2239 Path: news.gmane.org!not-for-mail From: Hasegawa Masahito Newsgroups: gmane.science.mathematics.categories Subject: preprint: a paper on *-autonomous categories and linear logic Date: Thu, 10 Apr 2003 11:32:25 +0900 Message-ID: <200304100232.h3A2WP703703__48831.1342000545$1241018520$gmane$org@synaphai.kurims.kyoto-u.ac.jp> NNTP-Posting-Host: main.gmane.org X-Trace: ger.gmane.org 1241018519 3195 80.91.229.2 (29 Apr 2009 15:21:59 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:21:59 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Thu Apr 10 12:19:54 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 10 Apr 2003 12:19:54 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 193dlt-0003aC-00 for categories-list@mta.ca; Thu, 10 Apr 2003 12:15:25 -0300 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 7 Original-Lines: 47 Xref: news.gmane.org gmane.science.mathematics.categories:2239 Archived-At: Dear colleagues, The following short paper Coherence of the Double Involution on *-Autonomous Categories by J.R.B. Cockett, M. Hasegawa and R.A.G. Seely available from the authors' pages http://www.kurims.kyoto-u.ac.jp/~hassei/papers/#STAR http://www.math.mcgill.ca/rags/ 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. Best, Robin Cockett Masahito Hasegawa Robert Seely