@Trebor: I think I have a better understanding of the issue of impredicative Prop, and I'd like to tell you what I think and hear your view on it. I think whether or not there is a problem with impredicative Prop depends on what we intend it to mean. In the PDF on CIC that I had quoted above, it seems that they would like to interpret "Π(x:A) . B" as a 'finished' type, and so the rule ( ( Γ ⊢ A : Type[i] ) ; ( Γ , x : A ⊢ B : Prop ) ⊢ ( Γ ⊢ Π(x:A) . B : Prop ) ) is indeed problematic.

In particular, if we imagine each universe as being constructed (by an abstract generative process) based on the lower universes, then we have to finish Prop before we can construct Type[1], but the impredicative rule essentially breaks that. In particular, if every type is intended to be some kind of collection/set, then "Π(x:A) . B" may never be finished if A = Type[1], simply because Type[1] may never be finished.

To evade an outright problem, one might think of the universes as being generated not necessarily in order of their hierarchy. But then one must accept that any type T may never be finished at any point; its membership may never stabilize. This applies even if ( T : Prop ) simply because of the impredicative rule. This implies that we cannot view membership in T classically, and so LEM would be completely unjustifiable.

So basically, impredicative Prop plus LEM would be as bad as the impredicativity in full ZFC, because the situation is analogous there where set membership is boolean and hence the cumulative hierarchy cannot be used to justify full specification or full replacement. However, this argument does not imply any problem with plain CoC with impredicative Prop, as long as one is careful to never view a type as a fixed collection.

What do you think?

Hmm I think that's about right. But I can't be sure for ZFC, because apart from beginner facts I don't know a lot.

Oh I think I do know what you mean. It's probably correct.

@Trebor Oh okay thanks for your feedback!

In case you want to read what I wrote specifically about ZFC, it's in this MO post:

On the other hand, if we think that propositions can only be differentiated by its truth/falsity, then there ever is only two propositions: True and False. So if you only have impredicative Prop you can probably justify it with some tricks ...(?)

Cool, I'll take a look. But now I've got to sleep. Early class tomorrow morning :(

@Trebor No I wouldn't believe that just like that, because even if Prop has (as the meta observation) only 2 members, it does not mean that there is a uniform internal 'mapping' from each x of type T to the truth-value of Q(x) even if we deduce ( x : T ⊢ Q(x) : Prop ).

Lack of a uniform 'mapping' would imply that we can't internally 'obtain' the truth-value of the quanfied statement ∀x∈T ( Q(x) ), so we wouldn't be able to justify LEM for that.

But we could still justify LEM for predicative Prop.