From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6091 Path: news.gmane.org!not-for-mail From: Robert Seely Newsgroups: gmane.science.mathematics.categories Subject: Re: Equality as an adjunction Date: Thu, 2 Sep 2010 11:22:29 -0400 (EDT) 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 1283556288 30904 80.91.229.12 (3 Sep 2010 23:24:48 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Fri, 3 Sep 2010 23:24:48 +0000 (UTC) Cc: categories@mta.ca To: David Leduc Original-X-From: majordomo@mlist.mta.ca Sat Sep 04 01:24:47 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 1Orfcl-0004hO-BB for gsmc-categories@m.gmane.org; Sat, 04 Sep 2010 01:24:47 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:38950) by smtpy.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1OrfbF-0004xF-NN; Fri, 03 Sep 2010 20:23:14 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1OrfbC-0007ZY-LP for categories-list@mlist.mta.ca; Fri, 03 Sep 2010 20:23:10 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6091 Archived-At: David - you might like to look at Lawvere's paper "Equality in hyperdoctrines and the comprehension schema as an adjunct functor" or "Adjointness in foundations" (the latter being a TAC reprint, and so easy to find). My thesis also explored this in detail ("Hyperdoctrines, natural deduction, and the Beck condition", on my webpage, url given below). -= rags =- On Thu, 2 Sep 2010, 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? > > -- [For admin and other information see: http://www.mta.ca/~cat-dist/ ]