The Coq mailing list

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

Hi Paul,

I have no doubt that Hugo will give his usual reply to this usual question.
If you can make sense of his reply, please enlighten us.



On Sat, Mar 27, 2010 at 6:04 AM, Muad Dib 
<muad.dib.space AT gmail.com>
 wrote:
> Hi coq-club,
>
> I am trying to write out some category theory definitions into Coq,
> and I had got quite far before I realized that I was using the
> identity equality rather than setoid! When I try to change it I am
> having seemingly impossible difficultly because of this universe
> inconsistency:
>
> Record setoid : Type := { carrier : Type }.
> Record Category : Type := { Ob : setoid }.
> Definition category : setoid := Build_setoid Category.
>
> If we make: Record setoid' : Type := { carrier' : Type }. and define
> category : setoid' instead -- it is allowed. but in that case I could
> not use (small) categories as the objects of a category. So my
> question is how could this be resolved? What I am also wondering about
> is that if we had quotient types in Coq, maybe this would be a lot
> easier.. but I am not sure what sort of theoretical difficulty there
> is with quotients compared to setoids.
>
> Thanks in advance!
>