Parametricity and excluded middle

Posted on 2016-02-24

In univalent foundations, it is known that the law of excluded middle allows one to define a family of functions fX:XXf_X : X \to X that is not the identity function on the booleans. We show that the converse holds as well: given such a function, we derive the law of excluded middle.