Section s.

Variables sigma, tau, delta : Set.

Definition  K_SigmaTau := [x:sigma][y:tau] x.

Definition  S_SigmaTauDelta := [x:sigma->tau->delta][y:sigma->tau][a:sigma](x a (y a)). 

Print K_SigmaTau.
Print S_SigmaTauDelta.

End s.

Print K_SigmaTau.
Print S_SigmaTauDelta.

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

Variables A, B : Set.

Definition exp1 := [x:A][y:B][C:Set][p:A->B->C] (p x y).
Definition exp2 := [A:Set][x:A][P:A->Set][y:(P x)] y.
Definition exp3 := [p:A->(C:Set)C][C:Set][a:A] (p a C).


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

Definition N := (C:Set)C->(C->C)->C.

Definition Z := [A:Set][z:A][s:A->A] z. 
Definition S := [a:N][A:Set][z:A][s:A->A] (s (a A z s)).

Definition soma := [b:N][a:N][A:Set][z:A][s:A->A] ((b A) (a A z s) s).


Check N.
Check Z.
Check S.
Check soma.

Eval Compute in (S Z).
Eval Compute in (S (S Z)).
Eval Compute in (soma (S Z)(S (S Z))).


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