From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5638 Path: news.gmane.org!not-for-mail From: David Leduc Newsgroups: gmane.science.mathematics.categories Subject: Re: equality is beautiful Date: Sun, 14 Mar 2010 08:51:23 +0000 Message-ID: Reply-To: David Leduc NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: dough.gmane.org 1268651192 17301 80.91.229.12 (15 Mar 2010 11:06:32 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Mon, 15 Mar 2010 11:06:32 +0000 (UTC) Cc: categories@mta.ca To: Richard Garner Original-X-From: categories@mta.ca Mon Mar 15 12:06:28 2010 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 1Nr87v-0005gF-Lr for gsmc-categories@m.gmane.org; Mon, 15 Mar 2010 12:06:27 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Nr7TS-00057n-2e for categories-list@mta.ca; Mon, 15 Mar 2010 07:24:38 -0300 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5638 Archived-At: Dear Richard, On Mon, Jan 11, 2010 at 11:26 AM, Richard Garner wrote: > Instead one takes a category internal to the type theory to be given by a > type of objects O, together with an OxO indexed family of hom-setoids > O(x,y), composition and identities which are maps of setoids, and > associativity and unitality witnessed by elements of the hom-setoid > equality. In this setting, we may not talk of equality of objects (since O > is not a setoid but only a type) but may talk of the equality of any pair of > parallel arrows. What about the characterization of limits in terms of products and equalizers? It states that the limit of a functor F:J->C is constructed by products indexed by the set(oid) of objects and the set(oid) of arrows of J. But if you don't allow equality on objects in J, you only have a preset of object, not a set(oid). David [For admin and other information see: http://www.mta.ca/~cat-dist/ ]