4 ms·
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 buil
by perthmad 7y ago
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.html https://sympa.inria.fr/sympa/arc/coq-club/2020-01/msg00006.h....
- jmgrosen 7y agoMy 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.