how to create a polymorphe couple such as "( a : type A, b : type B ) " in lambda-calculus

Question

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.

Answer 1

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.