[Agda] Parametricity is inconsistent with classical logic

[Jean-Philippe Bernardy]

> What exactly is parametricity? Could you write it in one line of Agda? I am unable to get consistent answers from Google.

I humbly recommend reading sec. II B and II C of this paper:

http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=153094

In sum, parametricity imposes that terms satisfy the constraints
imposed by the type-system, expressed as logical relations. It is
called "parametricity" because the types of types are usually
abstract, and in that case the condition imposes parametric behaviour
to polymorphic functions.

Cheers,
JP.