abb538

Exercise 6.9 of the HoTT book tells us that, and assuming LEM, we can exhibit a function $f:\Pi_{X:\mathcal{U}}(X\to X)$ such that $f_\mathbf{2}$ is a non-identity function $\mathsf{flip}:\mathbf{2}\to\mathbf{2}$ . 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 $f:\Pi_{X:\mathcal{U}}X\to X$ ?

In particular, we can see that internal proofs (claiming that $f$ must be the identity function for every type $X$ ) cannot exist: exercise 6.9 of the HoTT book tells us that, assuming LEM, we can exhibit a function $f:\Pi_{X:\mathcal{U}}(X\to X)$ such that $f_\mathbf{2}$ is $\mathsf{flip}:\mathbf{2}\to\mathbf{2}$ . (Notice that the proof of this is not quite as trivial as it looks: LEM only gives us $P+\neg P$ if $P$ is a proposition (a.k.a. subsingleton). Hence, simple case analysis on $X\simeq\mathbf{2}$ 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 $f$ 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 $f:\Pi_{X:\mathcal U}X\to X$ , such that $f_\mathbf2\neq\mathsf{id}_\mathbf2$ , we can prove the law of excluded middle.

Extensionality here means $f$ is invariant under equivalences. More precisely, its evaluation can be transported along equivalences on the input type $X:\mathcal U$ , satisfying appropriate computation rules. In particular, full univalence is sufficient.

If $f_\mathbf2\neq\mathsf{id}_\mathbf2$ , then by simply trying both elements $0_\mathbf2,1_\mathbf2:\mathbf2$ , we can find an explicit boolean $b:\mathbf2$ such that $f_\mathbf2(b)\neq b$ . Without loss of generality, we can assume $f_\mathbf2(0_\mathbf2)\neq 0_\mathbf2$ .

For the remainder of this analysis, let $P$ be an arbitrary subsingleton. Then we want to achieve $P+\neg P$ , to prove LEM.

Proof idea

We will consider a type with three points, where we identify two points depending on whether $P$ holds. Formally, this is the quotient of a three-element type, where the relation between two of those points is the proposition $P$ .

I will call this space $\mathbf{3}_P$ , and it can be defined as $\Sigma P+\mathbf{1}$ , where $\Sigma P$ is the suspension of $P$ . 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 $P$ is a subsingleton here.)

Notice that if $P$ holds, then $\mathbf{3}_P\simeq\mathbf{2}$ , hence $(\mathbf{3}_P\simeq\mathbf{3}_P)\simeq\mathbf{2}$ .

We will consider $f$ at the type $(\mathbf{3}_P\simeq\mathbf{3}_P)$ (not $\mathbf{3}_P$ itself!).

Now the proof continues by defining

$g:=f_{\mathbf{3}_P\simeq\mathbf{3}_P}(\mathsf{ide}_{\mathbf{3}_P}):\mathbf{3}_P\simeq\mathbf{3}_P$

and doing case analysis on $g(\mathsf{inr}(*))$ , and if necessary also on $g(\mathsf{inl}(x))$ for some elements $x:\Sigma P$ . 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 $\mathbf3_P$ (which would already give us $P+\neg P$ , which is exactly what we are trying to prove).

For the sake of illustration, here is one case:

$g(\mathsf{inr}(*))= \mathsf{inr}(*)$ : Assume $P$ holds. Then since $(\mathbf{3}_P\simeq\mathbf{3}_P)\simeq\mathbf{2}$ , then by transporting along an appropriate equivalence (namely the one that identifies $0_\mathbf2$ with $\mathsf{ide}_{\mathbf3_P})$ , we get $f_{\mathbf{3}_P\simeq\mathbf{3}_P}(\mathsf{ide}_{\mathbf{3}_P})\neq\mathsf{ide}_{\mathbf{3}_P}$ . But since $g$ is an equivalence for which $\mathsf{inr}(*)$ is a fixed point, $g$ must be the identity everywhere, that is, $g=\mathsf{ide}_{\mathbf{3}_P}$ , 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.