[perthmad]

This particular feat was triggered by Kevin Buzzard's unsubstantiated claim that "Lean was better than Coq" as a foundation for mathematics, because it had built-in quotient types. The work described above precisely shows that such types can be encoded as well using features shipped with the vanilla Coq distro. See https://sympa.inria.fr/sympa/arc/coq-club/2020-01/msg00006.h....

[jmgrosen]

My understanding is that this shows how vanilla Coq still can’t encode quotients well. This project relies on a PR [0] that breaks term normalization, which makes it highly unlikely it will be merged. My understanding is that Lean’s implementation of quotients also breaks normalization, but they don’t care as much about that as Coq devs do.

[0]: https://github.com/coq/coq/pull/10390#issuecomment-554316311

[SkySkimmer]

The normalization issue is not about quotients at all. It's https://arxiv.org/abs/1911.08174 "Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality"

[jmgrosen]

Well, I will defer to your judgment! I’m by no means a type theory person.

My understanding was that these features are how quotients are managed to be implemented. But perhaps that is wrong.