[Agda] Parametricity is inconsistent with classical logic

[Arseniy Alekseyev]

I've noticed that parametricity postulates are inconsistent with
classical logic, that is if you postulate both parametricity and the
law of excluded middle, you can derive a contradiction. Although it is
obvious in retrospect (lem, polymorphic in A, can not possibly know
whether to produce "yes" or "no" while being parametric!), I've never
heard it before, so i'm asking:

Is this a known fact?

Arseniy.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: parametricity.agda
Type: application/octet-stream
Size: 2343 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120420/771f6024/parametricity.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: parametricity2.agda
Type: application/octet-stream
Size: 2601 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120420/771f6024/parametricity2.obj