The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

On Wed, Nov 9, 2011 at 07:46,  
<roconnor AT theorem.ca>
 wrote:
> The problem with quotients done properly is that you can never escape from
> them to choose a representative.  Now you might think that this is exactly
> the point of using quotients; however such strict adherence to quotients
> severely limits your ability to compute.

I think this is a very interesting question.  I can definitely see the
point being made here about computation.

On the other hand, as far as I can tell, there are also reasons to
want to use quotients rather than setoids, depending on what goals one
has in mind.  In particular, one might be interested in type theory as
an internal language for categories (such as toposes).  In this case,
if the category is suitably exact, quotients will exist -- whereas
working with setoids amounts to not actually working in the original
category at all, but rather in some interesting hybrid of the category
and its free exact completion.

However, if this impression is wrong, I would be happy to be corrected.

Mike