From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5649 Path: news.gmane.org!not-for-mail From: Richard Garner Newsgroups: gmane.science.mathematics.categories Subject: Re: equality is beautiful Date: Sun, 21 Mar 2010 17:54:12 +0000 (GMT) Message-ID: References: Reply-To: Richard Garner NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Trace: dough.gmane.org 1269201162 18996 80.91.229.12 (21 Mar 2010 19:52:42 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Sun, 21 Mar 2010 19:52:42 +0000 (UTC) Cc: categories@mta.ca To: Michael Shulman Original-X-From: categories@mta.ca Sun Mar 21 20:52:38 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 1NtRCN-0006y6-Cr for gsmc-categories@m.gmane.org; Sun, 21 Mar 2010 20:52:35 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1NtQYt-0002ct-Gz for categories-list@mta.ca; Sun, 21 Mar 2010 16:11:47 -0300 In-Reply-To: Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5649 Archived-At: > That's a good point. However, if C is a non-strict category, then > while you can define products over its preset of objects, such a > product is no longer necessarily a particular case of a limit, since > the preset may not have any "discrete" category structure. So while > you can construct limits over arbitrary (non-strict) categories via > "products" and equalizers if you generalize the notion of "product" in > this way, the converse now fails -- having all limits doesn't seem to > guarantee that you have all "products" in this generalized sense. Yes, exactly; however, if one wishes this notion of product to become a special case of the notion of limit (a demand which seems not unreasonable) then it is enough to ask your type theory to have identity types: for then any preset A can be made into a category A# whose hom-setoids are the identity types Id_A(x,y) equipped with their propositional equality. Now limits indexed by A# correspond with products indexed by A, and so in this setting we recover the theorem that all limits <---> products and equalisers. Richard [For admin and other information see: http://www.mta.ca/~cat-dist/ ]