Categorical models of parametricity
Unary parametricity versus binary parametricity
The definition of “relation” and “identity relation” in parametricity is actually a bit up for grabs, and this freedom is actually essential if you want to support fancy types like higher kinds or dependent types, or wish to work with fancier semantic structures.