Exercise 6.9 of the HoTT book tells us that, and assuming LEM, we can exhibit a function
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
In particular, we can see that internal proofs (claiming that
And given the fact that LEM is consistent with univalent foundations, this means that a proof that
I have proved that LEM is exactly what is needed to get a polymorphic function that is not the identity on the booleans.
Theorem. If there is a function
For the remainder of this analysis, let
We will consider a type with three points, where we identify two points depending on whether
I will call this space
Notice that if
We will consider
Notice that doing case analysis here is simply an instance of the induction principle for
For the sake of illustration, here is one case:
Assume holds. Then since then by transporting along an appropriate equivalence (namely the one that identifies with we get But since is an equivalence for which is a fixed point, must be the identity everywhere, that is, which is a contradiction.
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.