[Agda] Proving Parametricity?

[Jean-Philippe Bernardy]

On Wed, Jan 19, 2011 at 5:07 PM, Brandon Moore
<brandon_m_moore at yahoo.com> wrote:
> I've written the following code based on Adam Chlipala's paper on
> "Parametric Higher Order Abstract Syntax". I'm wondering if there's
> any way to prove the parammetricity assumption at the end.
> It's taken as an axiom in the Coq development.

In do not think that you can prove this statement in Agda any more that you can
in Coq.

Incidentally, I am currently investigating the possibility to (safely)
extend Agda/Coq with
the axiom of parametricity, making the statement provable. Here is a
link to a draft
paper where one avenue is explored:

https://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=135303

Cheers,
JP.