[Haskell-cafe] An encoding of parametricity in Agda

[Eugene Kirpichov]

Hi,

I've discovered the following post on the internets:
http://gelisam.blogspot.com/2009/09/samuels-really-straightforward-proof-of.html

It contains an ingenious (to my mind) encoding of parametricity in
Agda that makes the Free Theorems a trivial consequence.

I've tried to formalize it in Coq, but, as of now, with no success.

-- 
Eugene Kirpichov
Web IR developer, market.yandex.ru