How much does this leak into typical math-related proofs?
If someone would create LeanQ where quotient types are built in nicely, how much work would it be to port the Fermat project from Lean to LeanQ?
AIUI, this cannot lead to inconsistency or a "wrong" proof. So if a proof checks out in Lean that's good enough, you might not even need a separate LeanQ.
Does this mean that most of the proofs in Lean and LeanQ would look exactly the same, it's just that the proofs of some technical low-level lemmas around quotient types (which I guess mathematicians are not really interested in anyway) look different?
For example, if I want to prove that a+b=b+a, I wouldn't care if I'm directly in peano arithmetic or just have a construction of the peano axioms in ZFC, as in both cases the proofs would be identical (some axioms in PA would be lemmas in ZFC).
If that's the case with quotients, I wonder why it's such a big deal for some.
AFAICT, this issue only comes up if you form the quotient of a proposition by a relation. But there is no point in doing that (all the proofs of a proposition are already equal!) so it's not an issue in practice and it wouldn't be difficult to fix.
However, Lean's SR is broken in other ways which do show up in practice: definitional proof irrelevance is incompatible with Lean's computation rule for Acc. That one is much harder to fix.
