You can't have two impredicative universes. You can't have
Type: Type. You can't have impredicative strong pairs. You can't have large elimination of an impredicative universe. You can't have positive datatypes when you have an impredicative universe. You can't this, you can't that. When will it end?
Interesting to note is that the only reason you can't eliminate something in Prop to something in a larger type in Coq is because they allow any inductive definition to be in Prop
If you restrict what kind of inductive definitions are allowed to be in Prop (in the same way Def. Proof Irrel. w/o K does*), then you can do large elimination of Props, because there's nothing meaningful you can eliminate it to in a larger universe
* i.e. constructors are orthogonal, non-forced arguments are in Prop, something something about termination
Coq actually has this "you can eliminate Props if it has no constructors or only a singleton constructor with Prop arguments" exception to eliminating Props that's basically a subset of the larger conditions from Def. Proof Irrel.
It doesn't seem to cover the termination thing but I'm not sure if that'll lead to an inconsistency or if it's just a decidable type checking thing
Thinking about this again. Type: Type gives you Girard's paradox, and so does arbitrary large elimination of something in an impredicative universe, since that lets you squish something from a bigger universe to a smaller universe, which is basically the effect of Type: Type
You can't have negative datatypes because you can prove false pretty easily, and you can't have non-strictly-positive datatypes with impredicativity because... why? I did it once in Coq but I don't understand what it is I did
And finally I don't know you can't have strong impredicative pairs but I suspect it's along the same lines as large elimination of impredicative universes
@ionchy I am convinced non-normalization does not mean inconsistency (proof: otherwise my PhD work in Lean would be worthless and we can't have that!)
But yes, since consistency doesn't necessarily imply normalization, the contrapositive (non-normalizing implies inconstency) also doesn't hold.
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.