The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 11/28/2011 05:32 PM, Dan Doel wrote:
> 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?

Maybe this is implicit in what you are saying but let me just emphasize 
that only *big* impredicative sums (i.e. with at least one constructor 
argument type not in Prop, like in your example) are inconsistent.
Small impredicative sums like { x:nat | P x } could have unrestricted 
eliminations (be aware that this contradicts proof-irrelevance and 
excluded-middle). This can be experimented with by mapping all Prop 
notions to their Set counterpart (ex -> sig, or -> sum, etc.) and using 
Coq with the -impredicative-set option.

The consistency of Coq with -impredicative-set and just one (and a half) 
universe is proved in Benjamin Werner's PhD. Don't know of any extension 
of this result to the full Type hierarchy, but it is believed to hold.

Bruno.

--
Bruno Barras                    Typical team - INRIA Saclay
LIX - Ecole Polytechnique       91128 Palaiseau Cedex - France
Tel: +33 1 69 33 40 57          Fax: +33 1 69 33 30 14