From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7833 Path: news.gmane.org!not-for-mail From: "Harley D. Eades III" Newsgroups: gmane.science.mathematics.categories Subject: Re: Non-triviality of *-autonomous categories Date: Sun, 4 Aug 2013 12:44:33 -0500 Message-ID: References: <77BE9A54-A589-408D-89B0-9C99D20B7F45@gmail.com> Reply-To: "Harley D. Eades III" NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 (Mac OS X Mail 6.2 \(1499\)) Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1375659751 15369 80.91.229.3 (4 Aug 2013 23:42:31 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 4 Aug 2013 23:42:31 +0000 (UTC) Cc: categories@mta.ca To: Robert Seely Original-X-From: majordomo@mlist.mta.ca Mon Aug 05 01:42:32 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 1V67wU-0005Lb-Ex for gsmc-categories@m.gmane.org; Mon, 05 Aug 2013 01:42:30 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:58640) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1V67vG-0002R6-HW; Sun, 04 Aug 2013 20:41:14 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1V67vH-0008VJ-Ac for categories-list@mlist.mta.ca; Sun, 04 Aug 2013 20:41:15 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7833 Archived-At: Hi, Robert. On Aug 4, 2013, at 9:10 AM, Robert Seely wrote: > If you want *-autonomous categories which are not preorders (I assume > that's what you mean by "non-trivial"), Yes, this is what I meant. I guess I should have not said = "non-trivial", due to it being somewhat ambiguous.=20 > 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: >=20 > Natural Deduction and Coherence for Weakly Distributive Categories > (Blute-Cockett-Seely-Trimble) (JPAA 113(1996)3, pp 229-296) I have not read this. Grabbing it now. > In fact, you can find many examples where the double negation > isomorphism is in fact an equality, by the following result: >=20 > Coherence of the Double Involution on *-Autonomous Categories > (Cockett-Hasegawa-Seely) (TAC 17(2006) pp 17-29) >=20 > (Of course the second paper is online; the first is also available on > my webpage.) Wonderful! I will grab this too. > 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. Indeed, and this point is wonderful, because it tells us that in linear = logic every connective can have a dual without the equational reasoning=20 collapsing. What do I mean by this? Consider bi-intuitionistic logic. It is well-known (Crolard:2001) that taking a bi-cartisan closed = category and adding co-exponentials we obtain a preorder. =20 What I am working on is showing that we can do a similar construction using linear categories without degenerating to a preorder in general. That is taking a linear category and its dual a collinear category and=20= smashing them together into what I call a dual linear category.=20 Bellin:2012 showed that a collinear category does (unsurprisingly)=20 model a co-linear type theory using Crolard's term assignment to co-inutitionisitc logic. However, I am a bit dubious of his chosen = path. It is well known that Crolard's subtractive logic is not complete for bi-intuitionstic logic. So melding together Bellin's model for=20 co-intutionsitic logic, co-linear categories, with linear categories may not yield a model for bi-intutitionistic linear logic. So this seems to be an open question. Anyway, just thought I would mention what I am working on if anyone has any feedback. Thanks for such a quick response. .\Harley [For admin and other information see: http://www.mta.ca/~cat-dist/ ]