Dear Toby, Thank you for your reply. Of course I am aware of this construction. 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. 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. You may say that we are only interested in objects upto isomorphism. But what does this mean precisely? Cheers, Thorsten On 30 May 2010, at 21:51, Toby Bartels <toby +categories@ugcs.caltech.edu> wrote:
Thorsten Altenkirch wrote:
Toby Bartels wrote:
[I suggested formalising category theory without equality of objects in intensional Martin-Löf type theory, Coq, or SEAR without equality]
I don't know any reasonable formalisation in Intensional Type Theory. People usually assume that hom sets are a setoid but objects aren't. This means that constructions like arrow categories are not available. To avoid this one would have to formalize explicitely what is a family of setoids indexed over a setoid. After this it is hard to see the category theory...
... [For admin and other information see: http://www.mta.ca/~cat-dist/ ]