[Agda] Parametricity is inconsistent with classical logic

[Danko Ilik]

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. I don't know about type theory, but if added to intuitionistic predicate logic it preserves disjunction and existence properties, so is in this sense constructive.

> It's not entirely obvious to me whether you can derive a contradiction
> to parametricity from this, but in the intended kind of classical
> model, this type is inhabited iff ((X : Set) → X ∨ ¬ X) is, so even if
> this were consistent with parametricity it wouldn't have the right
> semantics...

What exactly is parametricity? Could you write it in one line of Agda? I am unable to get consistent answers from Google.

Cheers,
Danko