The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

At the least, Zhaohui Luo's book (Computation and Reasoning: A Type
Theory for Computer Science) describing ECC and UTT notes the
inconsistency of strong impredicative sums. They let you do things
like:

    { P : Prop | True } : Prop

But { P : Prop | True } is equivalent to Prop if you can project out
the first component, giving you essentially

    Prop : Prop

Which is known to cause problems.

To prevent this, you need to restrict the elimination rules for these
impredicative sums in some way. I assume that's the sort of
restriction you were referring to?

Luo's thesis (which covers just ECC) may also have the note, and it's
a little more readily available than the book. I'm unsure of any other
references.

-- Dan

On Mon, Nov 28, 2011 at 10:47 AM, Gert Smolka 
<smolka AT ps.uni-saarland.de>
 wrote:
> Is the calculus of inductive constructions with impredicative Prop and 
> without the elim restriction consistent?  What is the standard reference 
> for this question?  Thanks, Gert