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

[Benja Fallenstein]

Hi Taral, Eugene,

[Taral]
>> 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.

[Eugene]
> Under parametricity, I mean the Reynolds Abstraction Theorem, from
> which free theorems follow.

Would it help to say that the Abstraction Theorem states that every
*definable* function is parametric, whereas Taral's formula states
that *every* function of that type is parametric?

(Both concepts are useful; Agda presumably has models where Taral's
formula does not hold (if it's consistent, i.e. has models at all), so
that formula presumably isn't provable in Agda without additional
axioms.)

All the best,
- Benja