The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Hi,

On 24/07/14 14:20, Michel Levy wrote:
> I examine the differences between the and_rect and prod_rect definition 
> (with Print and_rect and Print prod_rect).
> In the and_rect definition, you have P:Type while in the prod_rect 
> definition, you have P: prod A B -> Type.
> Why is the reason of this difference ?

Do you find the fact that "prod_rect" and "and_rect" have different types 
surprising?

Isn't that just a straightforward consequence of the fact that "prod" and 
"and" themselves have different types?
That is:

        and : Prop -> Prop -> Prop
        prod : Type -> Type -> Type