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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
