From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5901 Path: news.gmane.org!not-for-mail From: "Peter LeFanu Lumsdaine" Newsgroups: gmane.science.mathematics.categories Subject: Re: terminology Date: Tue, 1 Jun 2010 09:33:30 -0400 Message-ID: References: Reply-To: "Peter LeFanu Lumsdaine" 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 1275485501 9489 80.91.229.12 (2 Jun 2010 13:31:41 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Wed, 2 Jun 2010 13:31:41 +0000 (UTC) To: categories@mta.ca Original-X-From: categories@mta.ca Wed Jun 02 15:31:40 2010 connect(): No such file or directory 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.69) (envelope-from ) id 1OJo2l-00062z-Dd for gsmc-categories@m.gmane.org; Wed, 02 Jun 2010 15:31:39 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1OJnUR-0005oV-Qi for categories-list@mta.ca; Wed, 02 Jun 2010 09:56:11 -0300 In-Reply-To: Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5901 Archived-At: On Tue, June 1, 2010 03:39, Thorsten Altenkirch wrote: > A setoid is the intensional representation of a quotient (ie > coequalizer) and any construction involving it should respect this > structure. To use the underlying set of a setoid to construct another s= et > seems fundamentally flawed. Indeed; but what we construct is not just a set, it's a category! :-) In Toby's construction \C |---> arr \C, the setoid structure of the hom-sets of \C is _not_ respected if you just look at the underlying objects of arr \C, but it _is_ respected once you look at the whole resulting category arr \C. This is surely no worse than the fact that in just about any construction on setoids X |---> F(X), if you look at the underlying set of F(X), this will not fully respect the setoid structure of X? > My understanding of an arrow category is that it's objects are the > morphisms of the underlying category and since this is a setoid object= s > should be represented as a setoid too. The trouble here is that the original setoid structure is not on the whol= e arrow-set C_1, but on the individual hom-sets C_1(a,b). The arrow category sums this up over all a,b:C_0, and so is no longer a setoid from this data alone. (A dependent sum of setoids over a set doesn't have a natural setoid structure, as far as I can see?) In our case, of course, the object-sets _are_ also naturally setoids, wit= h their equalities given by isomorphisms of the categories. But we don't want to think of this setoid structure as primary: it's just a coarse reflection of part of the overall category structure. > You may say that we are only interested in objects upto isomorphism. > But what does this mean precisely? Going on from the above, it's an extension to the statement "we are only interested in elements of a setoid up to the given equality relation". S= o a more precise statement could go along the lines of: Any construction dependent on objects should respect isomorphisms. Best, -p. --=20 Peter LeFanu Lumsdaine Carnegie Mellon University [For admin and other information see: http://www.mta.ca/~cat-dist/ ]