The Coq mailing list

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

On Mon, Nov 28, 2011 at 11:51 AM, Bruno Barras 
<bruno.barras AT inria.fr>
 wrote:
> 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.

Yes. That doesn't really even register as impredicative to me. I
suppose it may be technically with nat : Type, but that organizational
decision is about proof irrelevance, not about size or self-reference,
as you say.

-- Dan