From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6057 Path: news.gmane.org!not-for-mail From: Gordon Plotkin Newsgroups: gmane.science.mathematics.categories Subject: Re: product for free Date: Thu, 19 Aug 2010 13:59:44 +0100 Message-ID: References: Reply-To: Gordon Plotkin 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 1282288450 32746 80.91.229.12 (20 Aug 2010 07:14:10 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Fri, 20 Aug 2010 07:14:10 +0000 (UTC) Cc: categories@mta.ca To: David Leduc Original-X-From: majordomo@mlist.mta.ca Fri Aug 20 09:14:06 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 1OmLni-0004bY-Nd for gsmc-categories@m.gmane.org; Fri, 20 Aug 2010 09:14:06 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:58101) by smtpx.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1OmLmF-0007YX-1A; Fri, 20 Aug 2010 04:12:35 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1OmLm9-0003ng-QW for categories-list@mlist.mta.ca; Fri, 20 Aug 2010 04:12:30 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6057 Archived-At: David, this is a lazy reply - I did not check anything out. One would be working with a second-order linear lambda calculus, presumably, so only the definition below of "pair" works. If one made a suitable "cut-down" version of Rasmus et al's paper, with parametricity, I would expect that, with you= r definition, one gets a tensor product adjoint to the function space. I don'= t have an immediate guess as to what one gets without parametricity. Gordon On Tue, Aug 17, 2010 at 2:27 PM, David Leduc w= rote: > Hi, > > In lambda-calculus one can define the product of types A and B by: > > 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/ ]