Parametricity and excluded middle

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 $\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 may seem: LEM only gives us $P+\neg P$ if $P$ is a (mere) 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 univalent foundations, this means that a proof that $f$ 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 $f:\Pi_{X:\mathcal U}X\to X$ with $f_\mathbf2\neq\mathsf{id}_\mathbf2,$ then LEM holds.

Proof idea

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 proposition. Then we want to achieve $P+\neg P,$ to prove LEM.

We will consider a type with three points, where we identify two points depending on whether $P$ holds. In other words, we consider 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 proposition here.)

Notice that if $P$ holds, then $\mathbf{3}_P\simeq\mathbf{2},$ and also $(\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$

(where $\mathsf{ide_{\mathbf3_P}}$ is the equivalence given by the identity function on $\mathbf3_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 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 $\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 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.

This entry was posted in Foundations. Bookmark the permalink.

14 Responses to Parametricity and excluded middle

jacquescarette says:

24 February 2016 at 12:12

From reading the Agda proof (thanks for linking to it!), it seems that this result can be informally stated as

If you have enough introspection power into polynomorphic types to create a non-identity type (at 2), then you have enough power to decide all (mere) propositions.

In other words, this tells you a lot about syntactic codes for Universes, aka reflection. If you build in sufficient reflection that you can pattern-match on your types, you’ve already built in LEM. Which is a very cool result.

- Auke Booij says:
  
  25 February 2016 at 09:00
  
  That is a nice way of looking at it, thanks.
  
Andrej Bauer says:

24 February 2016 at 13:14

What can be said if there is $f : \prod_{X : \mathsf{Type}} X \to X$ , and an inhabited type $Y$ with $a \neq b$ and such that $f_Y$ has no fixed points: $\prod_{y : Y} f_Y y \neq y$ ?

Mike Shulman says:

24 February 2016 at 13:19
Very cool!

One thought that may be worth mentioning: I think that if $f:\prod_{X:\mathcal{U}} X\to X$ , then in fact $f_{\mathbf{2}}$ must be an equivalence. For there are only four functions $\mathbf{2}\to \mathbf{2}$ , and the two that are not equivalences (the constant functions) are not preserved by $\mathrm{transport}^{\lambda X. X\to X}(\mathsf{ua}(\mathsf{flip}),-):(\mathbf{2}\to \mathbf{2}) \to (\mathbf{2}\to \mathbf{2})$ . Thus, if $f_{\mathbf{2}}$ is not the identity, then it is $\mathsf{flip}$ , and so we necessarily have both $f_{\mathbf{2}}(0_{\mathbf{2}}) \neq 0_{\mathbf{2}}$ and $f_{\mathbf{2}}(1_{\mathbf{2}}) \neq 1_{\mathbf{2}}$ .

Also, I wonder whether your case analyses could be simplified by starting with $\Sigma P$ instead of $\mathbf{1}$ ? The crucial ingredients seem to be
1. If $P$ , then $g$ is not the identity. Therefore, if $g$ maps anything in one summand of $\mathbf{3}_P$ to the same summand, assuming $P$ leads us to conclude that $g$ is the identity; hence $\neg P$ .
2. If $\mathsf{N}=\mathsf{S}$ , then $P$ .
Now consider $g(\mathsf{inl}(\mathsf{N}))$ and $g(\mathsf{inl}(\mathsf{S}))$ . If either of them lands in $\Sigma P$ , then $\neg P$ by the first observation above. Thus it remains to consider the case when both land in $\mathbf{1}$ ; but then since $g$ is an equivalence, $\mathsf{N}=\mathsf{S}$ and hence $P$ .

I haven’t tried to formalize this, though, so I could have missed something.
Martin Escardo says:

26 February 2016 at 19:44

I agree the result is very cool! And I agree with Andrej that there are more questions to be answered.

When Auke conjectured the result, I was a bit skeptical, but at the same time hopeful. He found a proof in a few days after his conjecture, which was very nice and impressive.

The essence of Auke’s argument is to construct a space whose number of points depends on a given proposition $P$ , being $2$ if $P$ holds, but something else otherwise, forcing $f$ to rely on a conundrum that can only be solved by an oracle for excluded middle.

Given this analysis of his construction/argument, the space $1+P$ also fits the bill: It has two points if $P$ holds, and one point if it doesn’t. So in general we can’t know how many points it has. In particular, this gives a difficult time to the function $f$ which wants $f(2)$ to be the flip function.

To see this, consider $f(1+P)(inl(*)) : 1+P$ .

Again like Auke did, we check whether this lands on the right or the left:

* If it lands on the left, we conclude that $P$ can’t hold, because if it
did then $1+P$ would be $2$ , by univalence, which means that $f(1+P)$ would
also need to flip, like $f(2)$ , landing on the right, which contradicts
the hypothesis that we landed on the left.

* If it lands on the right, we conclude directly that $P$ holds.

Hence $\neg P+P$ , as required.

We have used the same ingredients and ideas as in Auke’s original proof.

But we managed to get rid of quotients. We can get rid of univalence, as already emphasized by Auke himself, by just requiring that $f$ be invariant under equivalences, which can be regarded as an extensionality requirement.

In this way, we get Auke’s Theorem in the following generality: in intensional MLTT, if there is a polymorphic, extensional $f$ as above that flips the booleans, then excluded middle holds.

- Mike Shulman says:
  
  26 February 2016 at 23:59
  
  Very nice. Here is I think a further generalization. Suppose $f$ is polymorphic and extensional, and that there is a type $Y=1+X$ such that $f_Y(\mathsf{inl}(*))\neq \mathsf{inl}(*)$ . Now for any proposition $P$ , let $Y' = 1 + P\times X$ and consider $f_{Y'}(\mathsf{inl}(*))$ . If it is $\mathsf{inl}(*)$ , then $Y'$ cannot be equivalent to $Y$ by an equivalence that preserves the coproduct decompositions; hence $\neg P$ . But if it is $\mathsf{inr}((p,x))$ then $p:P$ .
  
  In other words, we get LEM as soon as a polymorphic extensional function has a detachable non-fixed-point.
  
  - Auke Booij says:
    
    27 February 2016 at 02:44
    
    It seems one cannot learn about this proof without learning this generalization, as Martin and I also both found this.
    
    There are also a couple of immediate results with boolean-valued polymorphic extensional functions $f_X:X\to\mathbf 2$ : for example, it is easy to prove that for a homogeneous type $Y$ (that is, a type such that for $a,b:Y$ , there is an automorphism of $Y$ that swaps $a$ and $b$ ), if $f_Y:Y \to \mathbf 2$ is non-constant, then bottom (rather than merely a taboo).
    
  - Mike Shulman says:
    
    28 February 2016 at 12:37
    
    I think we can probably generalize further by replacing $1$ by any inhabited type. That is, suppose $Y=A+B$ and $a:A$ such that $f_Y(\mathsf{inl}(a)) = \mathsf{inr}(b)$ for some $b$ . Then put $Y'=A+P\times B$ and consider $f_{Y'}(\mathsf{inl}(a))$ and argue similarly.
    
Pingback: Parametricity, automorphisms of the universe, and excluded middle | Homotopy Type Theory
Pingback: Model of the circle without HITs – Math Solution