The Coq mailing list

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

On 11/28/2011 08:44 PM, Dan Doel wrote:
> 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 should have said "small sum in an impredicative sort". It's not always 
clear what the impredicative word applies to: is it each feature that is 
considered impredicative or not, or is it the whole theory ?

What is clear to me is that the impredicative product types of Set have 
a global impact on the theory. For instance it is incompatible with 
interpreting each predicative product (in Type) as the set of 
set-theoretic functions (that's the Chicli-Pottier-Simpson paradox).

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