The Coq mailing list

[Yasuaki Kudo <yasu AT yasuaki.com>]

Hi,

 

I have a question regarding the section of Existential Quantification on Page 101 of Interactive Theorem Proving and Program Development (Coq’Art)

 

I hope this is not too nitpicking but because I am self-studying, I want to ensure that I understand the foundation correctly.

 

On Page 78 (4.1.1.6), the book says:

Types for the logical connectives and operator like prod are constructed thanks to the following rule, yet another extension of Prod.  The types that are formed in this way are called higher-order types.

 

 

E, G |-  A:Type

E, G |-  B:Type

------------------------------------------ Prod-sup

E, G |-  A->B : Type

 

 

On Page 101 (4.3.5.1):

The type of the constant ex has the sort Type; the formation of this type is summarized by the following sequence of judgements (only the third and the forth ones use the rule for building higher-order types):

 

[A:Type] |- Prop : Type

[A:Type] |- A-> Prop : Type

[A:Type] |- (A -> Prop) -> Prop : Type

|- ∀A:Type, (A -> Prop) -> Prop : Type

 

On contrary to the note in parenthesis (only the third and the forth…), it seems that the second example IS an example of the formation above where the first argument is A and the second being B?   Am I wrong?

 

In addition, what does Prod-sup mean?  I have seen terms like dependent product in the book but I don’t know what product means.

 

Regards,

Yasuaki

Tokyo