From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5525 Path: news.gmane.org!not-for-mail From: Peter LeFanu Lumsdaine Newsgroups: gmane.science.mathematics.categories Subject: Re: A challenge to all Date: Wed, 13 Jan 2010 18:43:49 -0500 Message-ID: References: Reply-To: Peter LeFanu Lumsdaine NNTP-Posting-Host: lo.gmane.org Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1263478676 4570 80.91.229.12 (14 Jan 2010 14:17:56 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Thu, 14 Jan 2010 14:17:56 +0000 (UTC) To: categories@mta.ca Original-X-From: categories@mta.ca Thu Jan 14 15:17:48 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.50) id 1NVQWB-00040B-M3 for gsmc-categories@m.gmane.org; Thu, 14 Jan 2010 15:17:47 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1NVPyx-0002JN-RC for categories-list@mta.ca; Thu, 14 Jan 2010 09:43:28 -0400 In-Reply-To: Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5525 Archived-At: On 12 Jan 2010, at 11:24, Andr=E9 Joyal wrote: >=20 > I would like to propose a test for verifying if the=20 > notion of category can be freed from the equality relation > on its set of objects. The equality relation on an ordinary=20 > set S is defined by the diagonal S-->S times S. Your test is addressed in more detail in other replies, but to pull out = one idea that comes up in several: --- the diagonal embedding is not always the equality relation. I don't think I've seen anyone propose how to define a notion of = category in the absence of some kind of diagonal embedding, but Francois = Larmarche and others nicely describe various situations (topological = spaces, higher categories, intensional type theories...) where the = diagonal embedding isn't a well-behaved equality relation, and certainly = isn't the one we want. For example, one such situation is explored by Gambino and Garner in = "The identity type weak factorisation system". Roughly: you can have = logical categories where a predicate S ---> A on an object means not a = monic, but rather a _fibration_, for some wfs (or similar structure). = The diagonal embedding A >--> AxA may fail to be a fibration; then the = equality predicate E comes from the factorisation of this map as a left = map (think "cofibrant weak equivalence") followed by a fibration: A >--> E ---> AxA. The groupoid case is a nice example of this situation, as described in = that paper. So the notions of "diagonal embedding" and "equality relation" can = certainly diverge (even in situations where both exist); and I think the = insight of Mike Shulman and co. here is that "diagonal embedding" is the = one which (if either) is wanted in the definition of a category. -p. --=20 Peter LeFanu Lumsdaine Carnegie Mellon University [For admin and other information see: http://www.mta.ca/~cat-dist/ ]