Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Can this universe inconsistency be resolved?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Can this universe inconsistency be resolved?


chronological Thread 
  • From: Muad Dib <muad.dib.space AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Can this universe inconsistency be resolved?
  • Date: Fri, 26 Mar 2010 21:04:25 +0000
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=VbMqtYSBMX8/dfTTCn1okwz9xfZIeSW/bs8QJJfl0rTVekDIzN3e04RGmCxpe4ZTlh TWdJIYe4hbFkuA9W2zKiuuwG6tJvzuAZXiARpMk7eHQFvHM/88Sv6PBl9+HYTwQTzlEp V+go6fQ3ORoGKrwUhXwzOIIX4xGwYS/NRI6Ns=

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!



Archive powered by MhonArc 2.6.16.

Top of Page