Parametricity and excluded middle

Exercise 6.9 of the HoTT book tells us that, and assuming LEM, we can exhibit a function f:\Pi_{X:\mathcal{U}}(X\to X) such that f_\mathbf{2} is a non-identity function \mathsf{flip}:\mathbf{2}\to\mathbf{2}. I have proved the converse of this. Like in exercise 6.9, we assume univalence.

Parametricity

In a typical functional programming career, at some point one encounters the notions of parametricity and free theorems.

Parametricity can be used to answer questions such as: is every function

f : forall x. x -> x

equal to the identity function? Parametricity tells us that this is true for System F.

However, this is a metatheoretical statement. Parametricity gives properties about the terms of a language, rather than proving internally that certain elements satisfy some properties.

So what can we prove internally about a polymorphic function f:\Pi_{X:\mathcal{U}}X\to X?

In particular, we can see that internal proofs (claiming that f must be the identity function for every type Xcannot exist: exercise 6.9 of the HoTT book tells us that, assuming LEM, we can exhibit a function f:\Pi_{X:\mathcal{U}}(X\to X) such that f_\mathbf{2} is \mathsf{flip}:\mathbf{2}\to\mathbf{2}. (Notice that the proof of this is not quite as trivial as it looks: LEM only gives us P+\neg P if P is a proposition (a.k.a. subsingleton). Hence, simple case analysis on X\simeq\mathbf{2} does not work, because this is not necessarily a proposition.)

And given the fact that LEM is consistent with intensional type theory, this means that the internal proof that f is the identity function cannot exist.

I have proved that LEM is exactly what you need to get a polymorphic function that is not the identity on the booleans.

Theorem. Given an extensional function f:\Pi_{X:\mathcal U}X\to X, such that f_\mathbf2\neq\mathsf{id}_\mathbf2, we can prove the law of excluded middle.

Extensionality here means f is invariant under equivalences. More precisely, its evaluation can be transported along equivalences on the input type X:\mathcal U, satisfying appropriate computation rules. In particular, full univalence is sufficient.

If f_\mathbf2\neq\mathsf{id}_\mathbf2, then by simply trying both elements 0_\mathbf2,1_\mathbf2:\mathbf2, we can find an explicit boolean b:\mathbf2 such that f_\mathbf2(b)\neq b. Without loss of generality, we can assume f_\mathbf2(0_\mathbf2)\neq 0_\mathbf2.

For the remainder of this analysis, let P be an arbitrary subsingleton. Then we want to achieve P+\neg P, to prove LEM.

Proof idea

We will consider a type with three points, where we identify two points depending on whether P holds. Formally, this is the quotient of a three-element type, where the relation between two of those points is the proposition P.

I will call this space \mathbf{3}_P, and it can be defined as \Sigma P+\mathbf{1}, where \Sigma P is the suspension of P. This particular way of defining the quotient, which is equivalent to a quotient of a three-point set, will make case analysis simpler to set up. (Note that suspensions are not generally quotients: we use the fact that P is a subsingleton here.)

Notice that if P holds, then \mathbf{3}_P\simeq\mathbf{2}, hence (\mathbf{3}_P\simeq\mathbf{3}_P)\simeq\mathbf{2}.

We will consider f at the type (\mathbf{3}_P\simeq\mathbf{3}_P) (not \mathbf{3}_P itself!).

Now the proof continues by defining

g:=f_{\mathbf{3}_P\simeq\mathbf{3}_P}(\mathsf{ide}_{\mathbf{3}_P}):\mathbf{3}_P\simeq\mathbf{3}_P

and doing case analysis on g(\mathsf{inr}(*)), and if necessary also on g(\mathsf{inl}(x)) for some elements x:\Sigma P. I do not believe it is very instructive to spell out all cases explicitly here. I wrote a more detailed note that does contain them, so if you are interested you can find a more explicit proof here.

Notice that doing case analysis here is simply an instance of the induction principle for +. In particular, we do not require decidable equality of \mathbf3_P (which would already give us P+\neg P, which is exactly what we are trying to prove).

For the sake of illustration, here is one case:

  • g(\mathsf{inr}(*))= \mathsf{inr}(*): Assume P holds. Then since (\mathbf{3}_P\simeq\mathbf{3}_P)\simeq\mathbf{2}, then by transporting along an appropriate equivalence (namely the one that identifies 0_\mathbf2 with \mathsf{ide}_{\mathbf3_P}), we get f_{\mathbf{3}_P\simeq\mathbf{3}_P}(\mathsf{ide}_{\mathbf{3}_P})\neq\mathsf{ide}_{\mathbf{3}_P}. But since g is an equivalence for which \mathsf{inr}(*) is a fixed point, g must be the identity everywhere, that is, g=\mathsf{ide}_{\mathbf{3}_P}, which is a contradiction.

I formalized this proof here in Agda using the HoTT-Agda library

Acknowledgements

Thanks to Martín Escardó, my supervisor, for his support. Thanks to Uday Reddy for giving the talk on parametricity that inspired me to think about this.

Parametricity and excluded middle