Re: A challenge to all

[Peter LeFanu Lumsdaine <plumsdai@andrew.cmu.edu>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1861 bytes --]

On 12 Jan 2010, at 11:24, André Joyal wrote:
> 
> I would like to propose a test for verifying if the 
> notion of category can be freed from the equality relation
> on its set of objects. The equality relation on an ordinary 
> 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.


-- 
Peter LeFanu Lumsdaine
Carnegie Mellon University



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]