[Agda] Parametricity is inconsistent with classical logic

[Martin Escardo]

Indeed, Spector's DNS is for X the natural numbers.

The postulate below not only generalizes this to X non-discrete, but 
also to X large. With X large, this allows you to prove the double 
negation of the principle of excluded middle, which is fairly classical 
(and also incompatible with continuity). But you already get into 
constructive trouble with X small and non-discrete (and again also an 
incompatibility with continuity).

Martin

On 09/05/12 10:27, Nils Anders Danielsson wrote:
> On 2012-05-09 08:44, Danko Ilik wrote:
>> On Wed, May 02, 2012 at 11:23:10AM +0200, Benja Fallenstein wrote:
>>> On the other hand, if you add the classical axiom of choice -- my own
>>> prefered version of writing it would be
>>>
>>>> postulate choice : {k l : Level} → {X : Set k} → {F : X → Set l} →
>>>> ((x : X) → ¬ ¬ F x) → ¬ ¬ ((x : X) → F x)
>>
>> This corresponds to Spector's Double Negation Shift principle.
>
> Not for arbitrary types X, right? See the following message:
>
> Martin Escardo
> Re: Agda with excluded middle is inconsistent
> http://thread.gmane.org/gmane.comp.lang.agda/1367/focus=1407
>