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?
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.
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.