# Natural Transformations and Parametricity

In Theorems for Free!, Wadler says that the characterization of parametricity can be re-expressed in terms of lax natural transformations and this will be the subject of a further paper. Which paper is he referring to?

The categorical approach to paramtericty I know uses dinatural transformations as in Functorial Polymorphism by Bainbridge, Freyd, Scedrov and P.J. Scott. What is the connection between lax natural transformation and dinatural transformation formulations of parametricity?

• I am almost afraid to make this comment, but I will confess that I don't understand any technical word in this question. Might it be possible to add some links to definitions for this (horribly)-non expert ? – Suresh Venkat Mar 13 '14 at 19:09
• Looks like a job for @UdayReddy. – Dave Clarke Mar 13 '14 at 19:38
• As far as I know, the paper referred to in Theorems for Free! was (sadly) never written. I'm pretty sure the current understanding of parametricity in terms of category theory is best captured by Scones and comma categories. See e.g. Mitchell & Scedrov and this n-Category Café post. – cody Mar 14 '14 at 15:59
• Suresh, sorry for not providing the relevant links. Cody, thank you for editing the post and mentioning scones and comma categories. – sonat Mar 16 '14 at 7:48

• @SonatSüer: The underlying 2-category is Rel. Recall that every poset can be regarded as a (degenerate) category with unique morphisms $x \to y$ whenever $x \leq y$. Similarly, every poset-enriched category can be regarded as a (degenerate) 2-category, with unique 2-cells $f \to g$ whenever $f \leq g$. Since Rel is a poset-enriched category with the inclusion order $R \subseteq S : \textbf{Rel}(A,B)$, it is a 2-category. – Uday Reddy Mar 17 '14 at 12:39