coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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!
- [Coq-Club] Can this universe inconsistency be resolved?, Muad Dib
- <Possible follow-ups>
- Re: [Coq-Club] Can this universe inconsistency be resolved?, David Leduc
Archive powered by MhonArc 2.6.16.