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 Xcannot 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.

13 Responses to Parametricity and excluded middle

  1. 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.

  2. Andrej Bauer says:

    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?

  3. Mike Shulman says:

    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.

  4. 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:

      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:

        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:

        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.

  5. Pingback: Parametricity, automorphisms of the universe, and excluded middle | Homotopy Type Theory

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s