From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5522 Path: news.gmane.org!not-for-mail From: Dusko Pavlovic Newsgroups: gmane.science.mathematics.categories Subject: Re: equality Date: Wed, 13 Jan 2010 12:53:30 -0800 Message-ID: References: Reply-To: Dusko Pavlovic NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 (Apple Message framework v936) Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1263478356 3418 80.91.229.12 (14 Jan 2010 14:12:36 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Thu, 14 Jan 2010 14:12:36 +0000 (UTC) To: Categories Original-X-From: categories@mta.ca Thu Jan 14 15:12:28 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1NVQR1-0001Za-Cs for gsmc-categories@m.gmane.org; Thu, 14 Jan 2010 15:12:27 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1NVPx1-00029L-Kw for categories-list@mta.ca; Thu, 14 Jan 2010 09:41:27 -0400 In-Reply-To: Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5522 Archived-At: hi. several people suggest dependent type theory as a foundation to formalize categories. maybe it is worth mentioning that per martin- loef (the originatory of dependent types) worked this out, prolly in the 70s. that was one of his early examples. many people who implemented basic category theory in the 80s (burstall-rydeheard, NuPRL team etc) followed this design. i am sure that there are people on the list who know much more about this than i do. while martin-loef's construction is quite natural and easy to reconstruct, one idea that still seems to be missing here, and leads to some confusion: the distinction between the extensional equality, ie term conversion, and the intentional equality, ie equality types. without going into any details, let me suggest that this formalization may clarify some confusion. in martin loef's formalization, the composition operation does not involve equality: no equality expressions occur in the expression Hom(A,B) # Hom(B,C) ---> Hom(A,C). what does occur are two copies of B. but ***being able to copy B is not the same thing as being able to decide the equality predicate***. mapping things along the diagonal is not the same thing as being able to decide whether something lies in the image or not. in practice, if i give you an object (say a group B) you will have no problem to make two identical copies of that group, in whichever form it may be given. but if i give you two big complicated groups, and you want to know whether they are equal on the nose, then you need to see how they are represented. in other words, you need to open the black boxes, and see what exactly are the elements of these groups etc. and this is not very categorical. as we all know, the whole point of eg the universal properties is that you describe things without opening any black boxes. one more thing, also apparent from any formalization: the reason why the object equality is no problem for small (internal) categories is that their objects can be viewed as arrows of the base category (and the arrows are, of course, in the business of being equal or not). -- dusko [For admin and other information see: http://www.mta.ca/~cat-dist/ ]