Hacker News new | past | comments | ask | show | jobs | submit login

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!

I don't know, normalizing at least seems reasonable constructively, sorry about the handwavyness in my reply as well!

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.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact