From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6088 Path: news.gmane.org!not-for-mail From: David Leduc Newsgroups: gmane.science.mathematics.categories Subject: Equality as an adjunction Date: Thu, 2 Sep 2010 01:40:12 +0000 Message-ID: Reply-To: David Leduc NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: dough.gmane.org 1283432876 9247 80.91.229.12 (2 Sep 2010 13:07:56 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Thu, 2 Sep 2010 13:07:56 +0000 (UTC) To: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Thu Sep 02 15:07:54 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 1Or9WD-0000yg-Q5 for gsmc-categories@m.gmane.org; Thu, 02 Sep 2010 15:07:53 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:39187) by smtpy.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1Or9Ug-0005CK-Um; Thu, 02 Sep 2010 10:06:19 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1Or9Uc-00034j-JW for categories-list@mlist.mta.ca; Thu, 02 Sep 2010 10:06:14 -0300 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6088 Archived-At: 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/ ]