From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6092 Path: news.gmane.org!not-for-mail From: Michael Shulman Newsgroups: gmane.science.mathematics.categories Subject: Re: Equality as an adjunction Date: Thu, 2 Sep 2010 10:56:38 -0700 Message-ID: References: Reply-To: Michael Shulman NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1283556318 31013 80.91.229.12 (3 Sep 2010 23:25:18 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Fri, 3 Sep 2010 23:25:18 +0000 (UTC) Cc: categories@mta.ca To: David Leduc Original-X-From: majordomo@mlist.mta.ca Sat Sep 04 01:25:13 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 1OrfdA-0004qx-FM for gsmc-categories@m.gmane.org; Sat, 04 Sep 2010 01:25:12 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:36582) by smtpx.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1Orfc0-000114-Ip; Fri, 03 Sep 2010 20:24:00 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1Orfby-0007aP-6s for categories-list@mlist.mta.ca; Fri, 03 Sep 2010 20:23:58 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6092 Archived-At: Hi David The two categories involved are Pred([A]) and Pred([A A]), the categories (perhaps preorders) of predicates over the contexts A and A A in the contextual category of the logic (or in some semantic interpretation of it). The diagonal morphism [A] --> [A A] induces a pullback functor \Delta^*: Pred([A A]) --> Pred([A]) which interprets a predicate P(x,x') as a predicate with only one variable of type A by duplication: P(x,x). Its left adjoint \Delta_! interprets a predicate of one variable as a predicate of two variables which is only true when the two variables are equal, i.e. it adds x=3Dx' to the predicate. I believe this adjunction was first noticed by Lawvere in "Equalities in hyperdoctrines and comprehension schema as an adjoint functor." Mike On Wed, Sep 1, 2010 at 6:40 PM, David Leduc w= rote: > 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. > > =A0 =A0 =A0 Phi |- P(x,x) =A0 [x:A] > =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D > Phi, x=3Dx' |- P(x,x') =A0 [x x':A] > > What are the left and right adjoint functors here? > [For admin and other information see: http://www.mta.ca/~cat-dist/ ]