From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5897 Path: news.gmane.org!not-for-mail From: Thorsten Altenkirch Newsgroups: gmane.science.mathematics.categories Subject: Re: terminology Date: Tue, 1 Jun 2010 08:39:46 +0100 Message-ID: References: Reply-To: Thorsten Altenkirch NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 (iPhone Mail 7E18) Content-Type: text/plain;charset=utf-8; format=flowed;delsp=yes Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1275395691 24685 80.91.229.12 (1 Jun 2010 12:34:51 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Tue, 1 Jun 2010 12:34:51 +0000 (UTC) To: Toby Bartels Original-X-From: categories@mta.ca Tue Jun 01 14:34:50 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 1OJQgE-0006kX-5g for gsmc-categories@m.gmane.org; Tue, 01 Jun 2010 14:34:50 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1OJQI5-0002SA-Jy for categories-list@mta.ca; Tue, 01 Jun 2010 09:09:53 -0300 In-Reply-To: Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5897 Archived-At: Dear Toby, Thank you for your reply. Of course I am aware of this construction. A setoid is the intensional representation of a quotient (ie =20 coequalizer) and any construction involving it should respect this =20 structure. To use the underlying set of a setoid to construct another =20= set seems fundamentally flawed. My understanding of an arrow category is that it's objects are the =20 morphisms of the underlying category and since this is a setoid =20 objects should be represented as a setoid too. You may say that we are only interested in objects upto isomorphism. =20 But what does this mean precisely? Cheers, Thorsten On 30 May 2010, at 21:51, Toby Bartels wrote: > Thorsten Altenkirch wrote: > >> Toby Bartels wrote: > > [I suggested formalising category theory without equality of objects > in intensional Martin-L=C3=B6f type theory, Coq, or SEAR without = equality] > >> I don't know any reasonable formalisation in Intensional Type Theory. >> People usually assume that hom sets are a setoid but objects aren't. >> This means that constructions like arrow categories are not =20 >> available. >> To avoid this one would have to formalize explicitely what is a =20 >> family >> of setoids indexed over a setoid. After this it is hard to see the >> category theory... > ... [For admin and other information see: http://www.mta.ca/~cat-dist/ ]