package Ex (X,Y,Z:: Type) where

 S  :: Type
    = sig{ fst:: X; snd:: X-> Y} 

 T  :: Type 
    = S -> Y
  
 P :: T
    = \(h::S) -> h.snd h.fst



 Q :: (((X -> Y)-> Z)-> Z) -> X -> (Y -> Z)-> Z
   = {! !}



 R :: ((X ->Z)-> Z) -> (((X->Y)->Z)->Z) -> (Y->Z)->Z
    = {! !}