From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6056 Path: news.gmane.org!not-for-mail From: =?ISO-8859-1?Q?Rasmus_M=F8gelberg?= Newsgroups: gmane.science.mathematics.categories Subject: Re: product for free Date: Wed, 18 Aug 2010 16:36:41 +0200 Message-ID: References: Reply-To: =?ISO-8859-1?Q?Rasmus_M=F8gelberg?= NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1282215946 7038 80.91.229.12 (19 Aug 2010 11:05:46 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Thu, 19 Aug 2010 11:05:46 +0000 (UTC) Cc: categories@mta.ca To: David Leduc Original-X-From: majordomo@mlist.mta.ca Thu Aug 19 13:05:45 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpx.mta.ca ([138.73.1.138]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1Om2wH-0000QW-RV for gsmc-categories@m.gmane.org; Thu, 19 Aug 2010 13:05:42 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:57061) by smtpx.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1Om2uM-0002n8-KB; Thu, 19 Aug 2010 08:03:42 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1Om2uJ-0008Mh-Vz for categories-list@mlist.mta.ca; Thu, 19 Aug 2010 08:03:40 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6056 Archived-At: Dear David, If you consider not only a closed monoidal category, but a full model of dual intuitionistic linear logic (DILL) with parametric polymorphism, the answer is yes. A model of DILL means among other things that the tensor is symmetric, and that there is a comonad, usually denoted ! . Writing --o for the closed structure and --> for the Girard encoding A --> B =3D !A --o B, then one can first encode coproducts as A + B =3D forall C . (A --o C) --> (B --o C) --> C and then products as A x B =3D forall C . ((A --o C) + (B --o C)) --o C Further details on these encodings can be found in Linear Abadi and Plotkin Logic, by Birkedal, M=C3=B8gelberg and Petersen, Logical methods in Computer Science, 2(5). Rasmus On 17 August 2010 15:27, David Leduc wrote: > Hi, > > In lambda-calculus one can define the product of types A and B by: > > =C2=A0 forall C, (A->B->C)->C. > > with pairing and projections defined as: > > pair =E2=89=A1 =CE=BBx.=CE=BBy.=CE=BBz.z x y > fst =E2=89=A1 =CE=BBp.p (=CE=BBx.=CE=BBy.x) > snd =E2=89=A1 =CE=BBp.p (=CE=BBx.=CE=BBy.y) > > What would be the equivalent in a closed monoidal category? > Would we get a product for free? > [For admin and other information see: http://www.mta.ca/~cat-dist/ ]