[Agda] Parametricity is inconsistent with classical logic

Peter Hancock hancock at spamcop.net
Thu May 10 11:59:55 CEST 2012

>>>> ((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.


More information about the Agda mailing list