From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5907 Path: news.gmane.org!not-for-mail From: Toby Bartels Newsgroups: gmane.science.mathematics.categories Subject: Re: terminology Date: Tue, 1 Jun 2010 11:22:49 -0700 Message-ID: References: <7BF50141-7775-4D3C-A4AF-D543891666B9@cs.nott.ac.uk> Reply-To: Toby Bartels NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: dough.gmane.org 1275485554 9670 80.91.229.12 (2 Jun 2010 13:32:34 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Wed, 2 Jun 2010 13:32:34 +0000 (UTC) Cc: "categories@mta.ca" To: Thorsten Altenkirch Original-X-From: categories@mta.ca Wed Jun 02 15:32:31 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 1OJo3a-0006Zq-16 for gsmc-categories@m.gmane.org; Wed, 02 Jun 2010 15:32:30 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1OJnWY-0005tv-VT for categories-list@mta.ca; Wed, 02 Jun 2010 09:58:23 -0300 Content-Disposition: inline Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5907 Archived-At: Thorsten Altenkirch wrote in part: >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 >set seems fundamentally flawed. I would rather not say "underlying set" here, but "underlying type". The category of types can do what it likes, but the category of sets should already have coequalisers. (Some type theorists do say "set" here; I just think that it is liable to confuse category theorists.) It is the setoids which behave like the sets that we know. But what is flawed about using the underlying type of a set(oid)? Group theorists who found group theory on set theory are allowed to use the underlying set of a group. So set theorists who found set theory (as setoid theory) on type theory should be able to speak of the underlying type of a set(oid), and category theorists who found category theory on type theory should be able to speak of the underlying type of their structures. >My understanding of an arrow category is that it's objects are the >morphisms of the underlying category and since this is a setoid objects >should be represented as a setoid too. I'm not sure what you mean by "this is a setoid". If you mean that, given a category C (as formalised in type theory), the morphisms of C form a setoid, then this is not true. Given a category C and two objects x and y of C, then the morphisms of C from x to y form a setoid, nothing more. Even if they did form a setoid, what of that? In Peter May's example of the category of intermediate fields in a given field extension, the objects do form a setoid. I call such a category a "strict category": http://ncatlab.org/nlab/show/strict+category Any poset defines a strict category in which isomorphic objects are equal. More generally, any category in which any two parallel morphisms are equal may be made into such a strict category by defining equality as isomorphism. Assuming an appropriate version of the axiom of choice, any category whatsoever may be made into a strict category by defining equality as isomorphism and making some choices to match up hom-sets. The fact that strict categories exist does not invalidate the perspective from which categories are not inherently strict, any more than the existence of monoidal categories invalidates ordinary category theory. Even assuming the axiom of choice, that we can make any category into a strict category is like our ability to make any monoidal category into a strict monoidal category; the theory of weak categories and weak monoidal categories stands. (Incidentally, any strict monoidal category must be a strict category, while a weak monoidal category need not be.) >You may say that we are only interested in objects upto isomorphism. But >what does this mean precisely? What it means is that, whenever anyone refers to equality of objects, I interpret it as being a statement in strict category theory, with all other statements being in ordinary (weak) category theory. It is an empirical claim that the basic results of category theory as it is normally understood do not refer to equality of objects. It is conjecture in metamathematics that any such statement, if a theorem, has a proof that never refers to equality of objects. (Whether this conjecture is true or false can depend on exactly what your foundations of mathematics are. You also have to take care to identify defined concepts that implicitly make reference to equality of objects.) --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ]