[Agda] Parametricity is inconsistent with classical logic

[Nils Anders Danielsson]

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

-- 
/NAD