It is known that
impredicativity + large eliminations + excluded middle is inconsistent. Prop is impredicative and consistent with excluded middle, but does not allow large eliminations (except when constructing witnesses whose type lives in Prop). Set and Type(i) allow large eliminations and are consistent with excluded middle, but are predicative. If we use the
-impredicative-set flag, then Set is impredicative, but does not allow large eliminations for large inductive types.
Is there a universe in Coq which is impredicative, allows large eliminations on any inductive type that lives in it, but is consistent in the absence of the axiom of excluded middle?