From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6060 Path: news.gmane.org!not-for-mail From: Robert Seely Newsgroups: gmane.science.mathematics.categories Subject: Re: product for free Date: Thu, 19 Aug 2010 22:16:06 -0400 (EDT) Message-ID: References: Reply-To: Robert Seely NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1282288634 937 80.91.229.12 (20 Aug 2010 07:17:14 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Fri, 20 Aug 2010 07:17:14 +0000 (UTC) Cc: David Leduc , categories@mta.ca To: soloviev@irit.fr Original-X-From: majordomo@mlist.mta.ca Fri Aug 20 09:17:13 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpy.mta.ca ([138.73.1.139]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1OmLqe-0006Hr-Dr for gsmc-categories@m.gmane.org; Fri, 20 Aug 2010 09:17:09 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:34271) by smtpy.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1OmLpg-0006fs-E3; Fri, 20 Aug 2010 04:16:08 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1OmLpc-0003s8-03 for categories-list@mlist.mta.ca; Fri, 20 Aug 2010 04:16:04 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6060 Archived-At: More to the point, it is a "weak product" (lacking the uniqueness condition one usually has) - I think this is discussed in Lambek Scott, but am away from my library to verify this ... -=3D rags =3D- On Wed, 18 Aug 2010, soloviev@irit.fr wrote: > Remark: > > as far as I remember, one need to be cautios > calling this a product, because ordinary product > equations do not hold with this definition and > standard equality of lambda-calculus. > > Best wishes > > Sergei Soloviev > >> 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 =FF=FF =FF=FFx.=FF=FFy.=FF=FFz.z x y >> fst =FF=FF =FF=FFp.p (=FF=FFx.=FF=FFy.x) >> snd =FF=FF =FF=FFp.p (=FF=FFx.=FF=FFy.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/ ]