On Tue, June 1, 2010 03:39, Thorsten Altenkirch wrote:
A setoid is the intensional representation of a quotient (ie coequalizer) and any construction involving it should respect this structure. To use the underlying set of a setoid to construct another set seems fundamentally flawed.
Indeed; but what we construct is not just a set, it's a category! :-) In Toby's construction \C |---> arr \C, the setoid structure of the hom-sets of \C is _not_ respected if you just look at the underlying objects of arr \C, but it _is_ respected once you look at the whole resulting category arr \C. This is surely no worse than the fact that in just about any construction on setoids X |---> F(X), if you look at the underlying set of F(X), this will not fully respect the setoid structure of X?
My understanding of an arrow category is that it's objects are the morphisms of the underlying category and since this is a setoid objects should be represented as a setoid too.
The trouble here is that the original setoid structure is not on the whole arrow-set C_1, but on the individual hom-sets C_1(a,b). The arrow category sums this up over all a,b:C_0, and so is no longer a setoid from this data alone. (A dependent sum of setoids over a set doesn't have a natural setoid structure, as far as I can see?) In our case, of course, the object-sets _are_ also naturally setoids, with their equalities given by isomorphisms of the categories. But we don't want to think of this setoid structure as primary: it's just a coarse reflection of part of the overall category structure.
You may say that we are only interested in objects upto isomorphism. But what does this mean precisely?
Going on from the above, it's an extension to the statement "we are only interested in elements of a setoid up to the given equality relation". So a more precise statement could go along the lines of: Any construction dependent on objects should respect isomorphisms. Best, -p. -- Peter LeFanu Lumsdaine Carnegie Mellon University [For admin and other information see: http://www.mta.ca/~cat-dist/ ]