From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7051 Path: news.gmane.org!not-for-mail From: Robert Seely Newsgroups: gmane.science.mathematics.categories Subject: Re: The boringness of the dual of exponential Date: Fri, 11 Nov 2011 16:08:25 -0500 (EST) Message-ID: References: Reply-To: Robert Seely NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Trace: dough.gmane.org 1321054244 4273 80.91.229.12 (11 Nov 2011 23:30:44 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Fri, 11 Nov 2011 23:30:44 +0000 (UTC) Cc: categories@mta.ca To: Vaughan Pratt Original-X-From: majordomo@mlist.mta.ca Sat Nov 12 00:30:38 2011 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpx.mta.ca ([138.73.1.4]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1RP0YO-0000KS-IW for gsmc-categories@m.gmane.org; Sat, 12 Nov 2011 00:30:36 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:57713) by smtpx.mta.ca with esmtp (Exim 4.76) (envelope-from ) id 1RP0XA-0002CF-0Z; Fri, 11 Nov 2011 19:29:20 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1RP0X8-0004no-Gx for categories-list@mlist.mta.ca; Fri, 11 Nov 2011 19:29:18 -0400 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7051 Archived-At: On Thu, 10 Nov 2011, Vaughan Pratt wrote: > ... Well, Set x Set^op is equivalent (in fact > isomorphic) to Chu(Set, 1). For *any* set K, both exponentiation and > dual exponentiation are admissible in Chu(Set,K), product being of the > tensor kind in this case. > > How did I know *that*? Well, every Chu category is a *-autonomous > category in the sense of Barr 1979. If you don't know why every > *-autonomous category contains both exponentiation and dual > exponentiation, then like Ebert and Siskel I'm not going to give away > the plot and you'll just have to fork out to see the movie, or steal it > if you're a nerd, or watch this space (someone is bound to be a spoiler). I hadn't intended to say this, but since Vaughan brought up *-autonomous cats, here goes. In Cockett-Seely "Proof theory for full intuitionistic linear logic, bilinear logic, and MIX categories" (TAC 1997) we showed that bilinear logic, formulated with both exponentials (ie suitable left adjoints to tensoring with an object) and dual exponentials (ie suitable right adjoints to co-tensoring ("par'ing") with an object), are just *-autonomous categories. So not only do *-autonomous cats have these two types of "internal homs" (4 operators in all, in the non-symmetric case), but if (eg) a linearly distributive category has them all, then it must be *-autonomous. (In the paper the result is a bit "finer", since we consider two variants of bilinear logic, the Lambek-style one as above, and what we call "Grishin categories", BILL and GILL in the paper. Both amount to different presentations of *-autonomous cats.) So, in the non-Cartesian context, suitable duals to exponentials are anything but boring ... -= rags =- -- [For admin and other information see: http://www.mta.ca/~cat-dist/ ]