[Agda] Parametricity is inconsistent with classical logic

[Benja Fallenstein]

On Wed, May 2, 2012 at 11:23 AM, Benja Fallenstein
<benja.fallenstein at gmail.com> wrote:
> [Given classical choice,] you can prove
>
>> tnd : (X : Set) → X ∨ ¬ X
>
> and using choice, you get
>
>> bad : ¬ ¬ ((X : Set) → X ∨ ¬ X)

Ah, this was supposed to read

>> bad : ¬ ¬ ((X : Set) → Either X (¬ X))

of course. Sorry!

- Benja