[Haskell-cafe] Re: [Coq-Club] An encoding of parametricity in Agda

[Taral]

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."
    -- Unknown