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.

## 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 ?

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.

## Proof idea

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.

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.