Re: equality is beautiful

[Richard Garner <rhgg2@hermes.cam.ac.uk>]

> 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/ ]