coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Defining types from equivalence relations.

From: quanta AT sdf.lonestar.org
To: coq-club AT inria.fr
Subject: [Coq-Club] Defining types from equivalence relations.
Date: Tue, 14 Dec 2010 01:22:45 +0100

I have a type T : Set and equivalence relation R : T -> T -> Prop and I would
like to form the new type T/R : Set. I could not find any way to form this new
type. I need this type to define a lot of objects, but one example is
fractions. Thank you for any advice on this topic possible.

[Coq-Club] Defining types from equivalence relations., quanta
- Re: [Coq-Club] Defining types from equivalence relations., Adam Chlipala
- <Possible follow-ups>
- Re: Re: [Coq-Club] Defining types from equivalence relations., quanta