The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

At 2013-09-26T17:07:06+02:00, Arnaud Spiwack wrote:

> Coq doesn't have quotients (yet?). So you cannot quite do this
> directly.
>
> The way to go is to use setoids, that is (dependent) pairs of a type
> and an equivalence relation on that type. Then you have to quantify
> on setoids rather than just types. The equality at each setoid is the
> underlying relation. And quotient is obtained just by changing the
> underlying relation of the setoid.

Thanks for the suggestion.  I'll try setoids.

> I'm not sure what reading to suggest for a more in-depth view. Maybe
> the first chapter of my thesis can be of help : http://
> pastel.archives-ouvertes.fr/docs/00/60/58/36/PDF/thesis.spiwack.pdf .

Yes, I'll look at that chapter.  Your thesis itself looks very
interesting.  It seems to discuss a lot of homological algebra in the
context of Coq.

Best regards,
Raghu.

-- 
N. Raghavendra 
<raghu AT hri.res.in>,
 http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/