Exercise 6.9 of the HoTT book tells us that, and assuming LEM, we can exhibit a function such that is a non-identity function . I have proved the converse of this. Like in exercise 6.9, we assume univalence.
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 must be the identity function for every type ) cannot exist: exercise 6.9 of the HoTT book tells us that, assuming LEM, we can exhibit a function such that is . (Notice that the proof of this is not quite as trivial as it looks: LEM only gives us if is a proposition (a.k.a. subsingleton). Hence, simple case analysis on 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 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 , such that , we can prove the law of excluded middle.
Extensionality here means is invariant under equivalences. More precisely, its evaluation can be transported along equivalences on the input type , satisfying appropriate computation rules. In particular, full univalence is sufficient.
If , then by simply trying both elements , we can find an explicit boolean such that . Without loss of generality, we can assume .
For the remainder of this analysis, let be an arbitrary subsingleton. Then we want to achieve , to prove LEM.
We will consider a type with three points, where we identify two points depending on whether holds. Formally, this is the quotient of a three-element type, where the relation between two of those points is the proposition .
I will call this space , and it can be defined as , where is the suspension of . 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 is a subsingleton here.)
Notice that if holds, then , hence .
We will consider at the type (not itself!).
Now the proof continues by defining
and doing case analysis on , and if necessary also on for some elements . 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 (which would already give us , which is exactly what we are trying to prove).
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.