[Haskell-cafe] Re: [Coq-Club] An encoding of parametricity in Agda
taralx at gmail.com
Wed Sep 23 12:21:00 EDT 2009
On Wed, Sep 23, 2009 at 6:46 AM, Eugene Kirpichov <ekirpichov at gmail.com> wrote:
> It contains an ingenious (to my mind) encoding of parametricity in
> Agda that makes the Free Theorems a trivial consequence.
Perhaps I don't understand Agda very well, but I don't see
parametricity here. For one, there's no attempt to prove that:
forall (P Q : forall a, a -> a), P = Q.
which is what parametricity means to me.
Taral <taralx at gmail.com>
"Please let me know if there's any further trouble I can give you."
More information about the Haskell-Cafe