From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6098 Path: news.gmane.org!not-for-mail From: Vaughan Pratt Newsgroups: gmane.science.mathematics.categories Subject: Re: Equality as an adjunction Date: Fri, 03 Sep 2010 00:06:18 -0700 Message-ID: References: Reply-To: Vaughan Pratt NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: dough.gmane.org 1283556624 32033 80.91.229.12 (3 Sep 2010 23:30:24 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Fri, 3 Sep 2010 23:30:24 +0000 (UTC) To: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Sat Sep 04 01:30:23 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 1OrfiA-0006fm-Dz for gsmc-categories@m.gmane.org; Sat, 04 Sep 2010 01:30:22 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:47306) by smtpx.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1Orfgv-0001bB-HL; Fri, 03 Sep 2010 20:29:05 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1Orfgs-0007j0-UP for categories-list@mlist.mta.ca; Fri, 03 Sep 2010 20:29:03 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6098 Archived-At: On 9/1/2010 6:40 PM, David Leduc wrote: > In "Categorical Logic", Pitts explains that equality can be defined as > an adjunction. See Fig. 8, page 55 > (http://www.cl.cam.ac.uk/~amp12/papers/catl/catl.ps.gz) > > He writes the definition as a bidirectional typing rule for the > internal language of a suitable category. > > Phi |- P(x,x) [x:A] > =================== > Phi, x=x' |- P(x,x') [x x':A] > > What are the left and right adjoint functors here? There's a certain tension between logic and algebra here. The algebraist's response to a question of this nature should be, adjunction is third-order equality, where isomorphism is second-order and commutative diagrams are first-order. The adjunction case is best understood 3-categorically, representable quite easily with origami. I can't find the origami I constructed to demonstrate this, I should build it again and post a photo of it at some point. Using adjunctions to explain equality is fine, just as using a hammer two sizes too large to crack a peanut works fine when wielded gently, as Andy has done here. Vaughan [For admin and other information see: http://www.mta.ca/~cat-dist/ ]