[Agda] Parametricity is inconsistent with classical logic

[Peter Hancock]

>>>> ((x : X) → ¬ ¬ F x) → ¬ ¬ ((x : X) → F x)

I just wanted to say that DNS in this form resembles the
extensionality axiom in Voevodsky's form.

    ((x : X)-> isContr(F x)) -> isContr((x : X)-> F x)

A double negation seems to be a crude way of turning an
inhabited set into a singleton.

Or is that nonsense?  It looks like an extensionality axiom.

Hank