I am working on a project in Lambda-calculus and i am trying to code polymorphe couple with coqide but a have a problem coding the constructor that respect the type pprod
Definition pprod : Set -> Set -> Set := fun A B => forall T : Set , (A -> B -> T) -> T.
I have a problem with pcpl
Definition pcpl : Set -> Set -> pprod :=
fun A B T : Set => fun (a : A) (b : B) => fun k : A -> B -> T => k a b.
this is the error i get :
The term "pprod" has type "Set -> Set -> Set"
which should be Set, Prop or Type.
The problem is that you are quantifying over Set, so the resulting product type cannot be of type Set, but of a larger type Type. So your definition should look like
Definition pprod : Set -> Set -> Type := fun A B => forall T : Set , (A -> B -> T) -> T.
the constructor for products should look like
Definition pcpl (A : Set) (B : Set) : A -> B -> pprod A B :=
fun (a : A) (b : B) => fun T : Set => fun k : A -> B -> T => k a b.
An alternative way to approach this is to use the polymorphic types in Coq, namely the types in Prop:
Definition pprod : Prop -> Prop -> Prop :=
fun A B => forall T : Prop , (A -> B -> T) -> T.
Definition pcpl (A : Prop) (B : Prop) : A -> B -> pprod A B :=
fun (a : A) (b : B) => fun T : Prop => fun k : A -> B -> T => k a b.
Note the universes in Coq are a bit confusing. See What is different between Set and Type in Coq? for details.
I'm going to take this opportunity to advertise the new Proof Assistants stack exchange.