From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6205 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: Is equality evil? Date: Wed, 22 Sep 2010 12:27:03 +0200 Message-ID: References: <20100918141110.GC9467@mathematik.tu-darmstadt.de> <20100922040041.GB14958@ugcs.caltech.edu> 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 1285330935 763 80.91.229.12 (24 Sep 2010 12:22:15 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Fri, 24 Sep 2010 12:22:15 +0000 (UTC) Cc: categories@mta.ca To: Toby Bartels Original-X-From: majordomo@mlist.mta.ca Fri Sep 24 14:22: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 1Oz7I4-0000O0-HC for gsmc-categories@m.gmane.org; Fri, 24 Sep 2010 14:22:12 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:59799) by smtpx.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1Oz7Gm-0005me-4i; Fri, 24 Sep 2010 09:20:52 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1Oz7Gi-0001hz-U3 for categories-list@mlist.mta.ca; Fri, 24 Sep 2010 09:20:49 -0300 Content-Disposition: inline In-Reply-To: <20100922040041.GB14958@ugcs.caltech.edu> Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6205 Archived-At: I suspected already that you want to use no identity types at all. Well, in category theory one needs at least equality on morphisms. What I meant was that when one just considers finite types over a base type (typically N) one can use an equality defined by recursion on the type structure. But that's an ontology good for analysis and not for category theory. Moreover, there will be maps between these types which don't respect the inductively defined equality. Alternatively, one coud work with setoids as suggested by Palmgren. But that has also its intricacies since the binary predicates forming part of setoids are proof-relevant in general (see Palmgren's posting). As to Leibniz equality. If x and y are Leibniz equal, i.e. \forall P : A -> Prop. P(x) -> P(y), then this doesn't allow one to construct a map B(x) -> B(y) in case B : A -> Set (simply because Set is not Prop). Of course, dropping impredicativity you loose the theory of toposes. But maybe that's not so bad since van den Berg and Moerdijk have developed predicative algebraic set theroy in a sequence of papers available on the arXiv. Predicative topos theory is less well developed. But notice that they work with extensional equality (expressed by the reqirement that regular monos are small). I must say I remain unconvinced about working without equality as long as I haven't seen a convincing account of (presheaf) toposes and fibered categories in such a restricted setting. But presumably, people have other application areas in mind. It would be interesting to identify those. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]