type
type (:->) (p :: k -> k1 -> Type) (q :: k -> k1 -> Type) = forall (a :: k) (b :: k1). p a b -> q a bUsing parametricity as an approximation of a natural transformation in two arguments.