would you be able to say how "normalizing" fits into this? by "normalizing" i mean applying some function that takes each equivalence class to a representative element (think simplifying fractions). using something like that, we could round-trip a value (object -> quotient -> object), though at the end we might end up with a different value than what we put in. so yeah, a normalizing function seems like a useful thing when looking at quotients constructively. sorry for the handwavyness, i hope i managed to get my point across!
In lean specifically there is a bit more information here:
"and quotient construction which in turn implies the principle of function extensionality"
There is also, Michael Beeson's "Extensionality and choice in constructive mathematics"
So it seems at least that the definition of quotients in lean is classical, and justified by axioms, NuPRL at least seems constructive, this at least leads me to believe quotients as defined in lean aren't constructive. But i'm not sure we can take the step to "quotients aren't constructive".
Anyhow it's an interesting question, and one which I too wish I had more clarity on.