From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6192 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: Is equality evil? Date: Sat, 18 Sep 2010 16:11:10 +0200 Message-ID: References: Reply-To: Thomas Streicher NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: dough.gmane.org 1284906326 27991 80.91.229.12 (19 Sep 2010 14:25:26 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Sun, 19 Sep 2010 14:25:26 +0000 (UTC) Cc: categories@mta.ca To: Toby Bartels Original-X-From: majordomo@mlist.mta.ca Sun Sep 19 16:25:25 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 1OxKpY-0004Kg-Io for gsmc-categories@m.gmane.org; Sun, 19 Sep 2010 16:25:24 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:59830) by smtpy.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1OxKom-0007ND-Id; Sun, 19 Sep 2010 11:24:36 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1OxKoj-0004xW-B9 for categories-list@mlist.mta.ca; Sun, 19 Sep 2010 11:24:33 -0300 Content-Disposition: inline In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6192 Archived-At: It's no problem to come up with logics without equality predicates. Just omit the equality predicate and its associated axioms. For ideological reasons most logic texts give equality a distinguished status for historical reasons. In case of extensional theories it suffices to have equality on base type and lift it `a la logical relations. But then there might be operations which don't respect this kind of equality. In other words identity types are not necessary for doing constructive mathematics. Intensional Id-types arise from putting the idea to an extreme that all logical concepts are "inductively defined", i.e. are given by constructors and eliminators. The notion of equality of types you refer to is a different one. Namely judgemental equality which cannot be used as an ingredient for forming propositions. It seems to me t that the point simply is that use of equality in premisses can be avoided by declaring varibales appropriately. That trick goes a long way in basic category theory. Using Id-types is a different thing. Extensional Id-types together with sums correspond to "cartesian logic" which suffices for declaring a lot of categorical concepts. Intensional Id-types might be convenient for providing a logic where equality gets identified with isomorphism or even weak equivalence. But that's not avoiding equality it's rather `liberal'ising it. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]