- You get a nice (the nicest?) representation of binders using existential types, for example, to implement lambda calculus using native functions
- You become incompatible with the choice and excluded-middle axioms
- You become incompatible with the choice and excluded-middle axioms
Comments
But it opens as many doors as it closes, and we do not need these axioms for program reasoning! 💥