Homotopy Type Theory

Parametricity and excluded middle

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 may seem: LEM only gives us if is a (mere) 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 univalent foundations, this means that a proof that is the identity function cannot exist.

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 with then LEM holds.

Proof idea

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 proposition. 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. In other words, we consider 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 proposition here.)

Notice that if holds, then  and also

We will consider at the type  (not  itself!). Now the proof continues by defining

(where is the equivalence given by the identity function on ) 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 containing an explicit proof.

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:

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.