Aren't quotients non-constructive? Univalence is probably also relevant to this issue, given that it generalizes the treatment of 'equality' in a broadly similar direction to the one needed for quotients. Groupoids are after all a fairly natural generalization of setoids.
I can't, perhaps lean's definition of quotient isn't constructive (I hadn't looked or noticed that),
But there is at least this construction of quotients in NuPRL.
I think quotients are not typical of constructive objects in that if you construct some object, and then project it into the quotient, then you have the quotient, but you cannot project that object back out. You get subtly less, that the resulting quotient satisfies some equivalence relation.
Under a specific set of assumptions, you may very well be able to construct the quotient... but under a different set of assumptions (including the assumption of the quotient), Perhaps in these differing sets of assumptions, you have the quotient, but lack the assumptions necessary to construct it yourself.
Anyhow, the argument that they are non-constructive in a humpty dumpty sense you cannot
put it together -> take it apart -> put it back together again.
Where it seems reasonable to consider the "put it together" phase as not entirely incompatible with constructivity?
thanks for the reply! i'm gonna need some time to mull it over...
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!
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.
