3 ms·
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 mak
by jmgrosen 7y ago
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 https://github.com/coq/coq/pull/10390#issuecomment-554316311
- SkySkimmer 7y agoThe normalization issue is not about quotients at all. It's https://arxiv.org/abs/1911.08174 https://arxiv.org/abs/1911.08174 "Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality"
- jmgrosen 7y agoWell, 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.