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