From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7831 Path: news.gmane.org!not-for-mail From: Robert Seely Newsgroups: gmane.science.mathematics.categories Subject: Re: Non-triviality of *-autonomous categories Date: Sun, 4 Aug 2013 10:10:51 -0400 (EDT) Message-ID: References: <77BE9A54-A589-408D-89B0-9C99D20B7F45@gmail.com> Reply-To: Robert Seely NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Trace: ger.gmane.org 1375659560 13791 80.91.229.3 (4 Aug 2013 23:39:20 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 4 Aug 2013 23:39:20 +0000 (UTC) Cc: categories@mta.ca To: "Harley D. Eades III" Original-X-From: majordomo@mlist.mta.ca Mon Aug 05 01:39:23 2013 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.186]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1V67tS-0005iH-MM for gsmc-categories@m.gmane.org; Mon, 05 Aug 2013 01:39:22 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:58626) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1V67sN-00021Z-TU; Sun, 04 Aug 2013 20:38:15 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1V67sO-0008R8-Ke for categories-list@mlist.mta.ca; Sun, 04 Aug 2013 20:38:16 -0300 In-Reply-To: <77BE9A54-A589-408D-89B0-9C99D20B7F45@gmail.com> Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7831 Archived-At: If you want *-autonomous categories which are not preorders (I assume that's what you mean by "non-trivial"), there is an enormous selection to chose from, including the "first" you mention. One that's simple to use is "the" free *-aut cat (over an arbitrary category, so there are many such free *-aut cats), what we call "circuits" (aka proof nets). One ref: Natural Deduction and Coherence for Weakly Distributive Categories (Blute-Cockett-Seely-Trimble) (JPAA 113(1996)3, pp 229-296) In fact, you can find many examples where the double negation isomorphism is in fact an equality, by the following result: Coherence of the Double Involution on *-Autonomous Categories (Cockett-Hasegawa-Seely) (TAC 17(2006) pp 17-29) (Of course the second paper is online; the first is also available on my webpage.) This illustrates Girard's point (made in his first paper on linear logic) that the double negation isn't inherently non-constructive, rather that the "problem" with classical logic lies with the contraction structure rule. -= rags =- On Sat, 3 Aug 2013, Harley D. Eades III wrote: > Hi, everyone. > > I am having trouble finding a reference. I thought perhaps someone here > might know. > > It is well known that adding the isomorphism: > d : A -> (A => 1) => 1 > to a bicartisan closed category degenerates to a preorder. > > In *-autonomous categories we have such an isomorphism, but > is non-trivial. Where can I find a proof of this? I would like to > reference it. > > I think one could proof this using the category of coherence spaces and linear maps > as a concrete *-autonomous category. See for example: > > [1] R. a. g. Seely. Linear logic, *-autonomous categories and cofree coalgebras. In Computer Science Logic, 1989. > > Any references anyone might have would be great. > > Thanks, > .\ Harley > > > -- [For admin and other information see: http://www.mta.ca/~cat-dist/ ]