Rocq has this rarely known feature, and mathematicians hate it for that. (This is not clickbait 😆)
Impredicative Set allows to quantify over types of values while still being at the same level. This leads to paradox for most mathematicians but not in Rocq!
Here is what follows: 👇
Impredicative Set allows to quantify over types of values while still being at the same level. This leads to paradox for most mathematicians but not in Rocq!
Here is what follows: 👇
Comments
- You can represent existential types (like "dyn" in Rust) of arbitrary depth (cannot be emulated with universe polymorphism)
- You become incompatible with the choice and excluded-middle axioms
But it opens as many doors as it closes, and we do not need these axioms for program reasoning! 💥