[Agda] Parametricity is inconsistent with classical logic

Jean-Philippe Bernardy bernardy at chalmers.se
Fri Apr 27 13:51:16 CEST 2012

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.

(very last section of the appendix).


More information about the Agda mailing list