The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I strongly suspect it has quotient sets, contrary to what Andrej says about impossibility to define a quotient set in type theory.

 

In my ZornsLemma contribution, I construct quotient types using the usual construction as the set of equivalence classes.  Certainly, you need to assume Extensionality_Ensembles to prove the quotient projection map collapses R to strict equality; and you need to use constructive_definite_description to construct induced functions on a quotient type.  So yes, it's probably useless if you need things to be computable at the end.  But if what you're doing is pure mathematical formalization, I don't see any drawbacks to using this construction.
--
Daniel Schepler