The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 07.02.2014 15:27, schrieb Kirill Taran:
> Hello,
>
> Why we need impredicativity of Prop?
> Also, is there difference in expressivity between Coq and Agda due 
> difference in predicativity of Prop (in Agda everything is predicative)?

Hi Kirill,

Impredicativity means, informally, that if you create a proposition that 
talks about all propositions, it also talks about itself.

In Coq this is implemented by the (informal...) typing rule

  A : U         x : A => B : Prop
-----------------------------------
      forall x : A , B : Prop


In particular, if  A = Prop (and U = Type_0), you get:

(forall x : Prop ,  B) : Prop

Thus, you could instantiate x with (forall x : Prop ,  B).

For types this doesn't work, as the term would automatically have type U 
(or higher). For the formal typing rules, refer to: 
http://coq.inria.fr/doc/Reference-Manual006.html#sec167

Kind regards, jonas