Exercise 6.9 of the HoTT book tells us that, and assuming LEM, we can exhibit a function

## 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 *cannot* exist: exercise 6.9 of the HoTT book tells us that, assuming LEM, we can exhibit a function

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

## Proof idea

If

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 *suspension* of

Notice that if

We will consider *not*

(where

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.

I formalized this proof 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.