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.
In lean specifically there is a bit more information here: https://leanprover.github.io/theorem_proving_in_lean/axioms_...
"and quotient construction which in turn implies the principle of function extensionality"
There is also, Michael Beeson's "Extensionality and choice in constructive mathematics" https://projecteuclid.org/euclid.pjm/1102779710
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.