The Coq mailing list

[ben <benedikt.ahrens AT gmx.net>]

hi,

you should give the carrier as a parameter to the setoid

Record Setoid (T:Type) := {
      rel: relation T;
      rel_equiv: equivalence rel
}.

which is more or less how it is done in coq.
(try
Require Export Classes.SetoidClass.
Print Setoid.
)

do the same for the definition of 'category', see for example matthieu's
development at
http://mattam.org/research/coq/classes.en.html
where he defines a category of categories, afair (or better, a
categorical structure on categories).

btw, you might want to use the built-in setoids of coq instead of
redoing all the work.

greetings
ben



Muad Dib 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!