[Agda] Parametricity is inconsistent with classical logic

[Martin Escardo]

> Martin Escardo's argument is that you will not be able to use bar
> recursion to justify DNS for X≠ℕ, but it does not mean that you
> could never possible justify it.

I was thinking that Kreisel showed that classical choice over X allows
you to interpret the negative translation of comprehension, which is
rather strong.

> It seems that with control operators in logic you can do something
> (ex. http://hal.inria.fr/hal-00647389)

Sounds interesting. Will have a look.

Martin