Section lambda2.

Definition id := [alpha:Set][x:alpha] x.

Check id.
Check (alpha:Set)alpha->alpha.

Variable D:Set.
Eval Compute in (id D).
Variable d:D.
Eval Compute in (id D d).


Section l21.

Variable beta:Set.
Definition strange := [a: (alpha:Set)alpha] (a beta).
Check strange.

End l21.

Check strange.
Print strange.

End lambda2.



Section lambdaWweak.

Check [A:Set][B:Set]A.
Check Set->Set->Set.

Variable Par : Set->Set->Set.
Variable A, B : Set.

Parameter mkPair : A->B->(Par A B).
Parameter proj1 : (Par A B) -> A.
Parameter proj2 : (Par A B) -> B.
Check ( [x:(Par A B)][y:B](mkPair (proj1 x) y) ).

Parameter MkPair : (A,B:Set) A->B->(Par A B).
Check (A,B:Set) A->B->(Par A B).
Parameter Proj1 : (A,B:Set) (Par A B) -> A.
Parameter Proj2 : (A,B:Set) (Par A B) -> B.

(* ----------------------------------------- *)
(* exemplo f1 :   (1,2) |-> (1, (1,2))       *)
(* exemplo f2 :   (1,2) |-> ((1,2), 2)       *)

Definition f1 := [A:Set][p:(Par A A)](MkPair A (Par A A) (Proj1 A A p) p).
Definition f2 := [A:Set][p:(Par A A)](MkPair (Par A A) A p (Proj2 A A p)).

Check f1.
Check f2.

(* ----------------------------------------- *)

End lambdaWweak.

Check mkPair.



Restore State Initial.


Section lP.

Variable A : Set.

Check A->Set.

Variable P : A->Set.
Variable a : A.

Check (P a).
Check (P a) -> Set.
Check (P a) -> A -> Set.

Check (a:A)(P a).

Check ((P a) -> A -> Set) -> (A -> Set).
Check (P:A->Set)(a:A)(P a) -> Set.


Print A.
Print P.
Check (f:(A->Set)->(A->Set))(f P a).
Check (P:A->Set)(a:A)(P a)->(P a).

End lP.