Some simple polymorphic functions (V8)

For each of the following spécifications, check that its type has sort Type, then give some function which realizes this specification :

   id : forall A:Set, A->A
   diag : forall A B:Set, (A->A->B)->A->B
   permute : forall A B C :Set,(A->B->C)->B->A->C
   f_nat_Z : forall A:Set, (nat->A)->Z->A

Solution

Look at this file