Are lax natural transformations just natural transformations without naturality?

Question

In page 4 of Theorems for free!, Philip Wadler says that parametricity can be expressed in terms of lax natural transformations. Is he referring to the fact that parametrically polymorphic functions in functional programming languages are natural transformations without a proof of their naturality? Since I haven't found an appropiate definition of lax natural transformations, this is my idea so far.

Answer 1

No, he is not. He is referring to the concept of lax natural transformation as described over at the n-lab, and discussed in this MathOverflow question.

He is referring to the fact that parametrically polymorphic functions can be seen as Functors. It is their parametricity which is seen as a lax natural transformation. Basically this is a uniform way to go from any specialization of a parametrically polymorphic function to any other. The reason it is lax is that things don't commute on the nose (i.e. apply + transport is not exactly the same as transport + apply), but they are up to a given 2-cell.