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