[TYPES] Impredicative Set and large elimination

[Jonathan Chan]

Hello all, 

I'm trying to find some references for what is and isn't allowed with
what's known as an impredicative Set universe in Coq.
There's several references and explanations such as this issue [1] that
say that an impredicative Prop universe combined with unrestricted
elimination and excluded middle yields a contradiction.
I've also found this [2] saying that in Coq, "large" inductives in an
impredicative Set with constructors with arguments in larger universes
have elimination restricted to Prop and Set only,
presumably to also allow postulating an excluded middle axiom. 

Suppose I had a large inductive in impredicative Set and I do not
postulate excluded middle (or double negation elimination, or choice, or
indefinite description, etc.):
can I eliminate my inductive into large universes, i.e. Type, while
maintaining consistency?
Are there any references that discuss the consequences of having an
impredicative Set and other inconsistencies I should watch out for?
I will not be postulating any axioms that aren't part of CIC, but I am
wondering about whether I can have an impredicative Prop subtype an
impredicative Set,
and whether making the theory extensional (with equality reflection)
would at all interfere with consistency. 

Regards,
Jonathan 

[1] https://github.com/FStarLang/FStar/issues/360
[2] http://adam.chlipala.net/cpdt/html/Universes.html#lab80