Re: equality is beautiful

[David Leduc <david.leduc6@googlemail.com>]

Dear Richard,

On Mon, Jan 11, 2010 at 11:26 AM, Richard Garner <rhgg2@hermes.cam.ac.uk> 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/ ]