[Agda] Parametricity is inconsistent with classical logic

[Jean-Philippe Bernardy]

On Fri, Apr 20, 2012 at 12:46 PM, Arseniy Alekseyev
> Is this a known fact?

In a draft paper, M. Lasson and C. Keller prove that parametricity of
Peirce's law is contradictory,
as an example of their tactic for parametricity.

http://perso.ens-lyon.fr/marc.lasson/coqparam-draft.pdf
(very last section of the appendix).

Cheers,
JP.