Parametricity, automorphisms of the universe, and excluded middle

Specific violations of parametricity, or existence of non-identity automorphisms of the universe, can be used to prove classical axioms. The former was previously featured on this blog, and the latter is part of a discussion on the HoTT mailing list. In a cooperation between Martín Escardó, Peter Lumsdaine, Mike Shulman, and myself, we have strengthened these results and recorded them in a paper that is now on arXiv.

In this blog post, we work with the full repertoire of HoTT axioms, including univalence, propositional truncations, and pushouts. For the paper, we have carefully analysed which assumptions are used in which theorem, if any.

Parametricity

Parametricity is a property of terms of a language. If your language only has parametric terms, then polymorphic functions have to be invariant under the type parameter. So in MLTT, the only term inhabiting the type $\prod_{X:\mathcal{U}}X \to X$ of polymorphic endomaps is the polymorphic identity $\lambda (X:\mathcal{U}). \mathsf{id}_X$ .

In univalent foundations, we cannot prove internally that every term is parametric. This is because excluded middle is not parametric (exercise 6.9 of the HoTT book tells us that, assuming LEM, we can define a polymorphic endomap that flips the booleans), but there exist classical models of univalent foundations. So if we could prove this internally, excluded middle would be false, and thus the classical models would be invalid.

In the abovementioned blog post, we observed that exercise 6.9 of the HoTT book has a converse: if $f:\prod_{X:\mathcal{U}}X\to X$ is the flip map on the type of booleans, then excluded middle holds. In the paper on arXiv, we have a stronger result:

Theorem. There exist $f:\prod_{X:\mathcal{U}}X\to X$ and a type $X$ and a point $x:X$ with $f_X(x)\neq x$ if and only if excluded middle holds.

Notice that there are no requirements on the type $X$ or the point $x$ . We have also applied the technique used for this theorem in other scenarios, for example:

Theorem. There exist $f:\prod_{X:\mathcal{U}}X\to \mathbf{2}$ and types $X, Y$ and points $x:X, y:Y$ with $f_X(x)\neq f_Y(y)$ if and only if weak excluded middle holds.

The results in the paper illustrate that different violations of parametricity have different proof-theoretic strength: some violations are impossible, while others imply varying amounts of excluded middle.

Automorphisms of the universe

In contrast to parametricity, which proves that terms of some language necessarily have some properties, it is currently unknown if non-identity automorphisms of the universe are definable in univalent foundations. But some believe that this may not be the case.

In the presence of excluded middle, we can define non-identity automorphisms of the universe. Given a type $X$ , we use excluded middle to decide if $X$ is a proposition. If it is, we map $X$ to $\neg X$ , and otherwise we map $X$ to itself. Assuming excluded middle, we have $\neg\neg X=X$ for any proposition, so this is an automorphism.

The above automorphism swaps the empty type $\mathbf{0}$ with the unit type $\mathbf{1}$ and leaves all other types unchanged. More generally, assuming excluded middle we can swap any two types with equivalent automorphism ∞-groups, since in that case the corresponding connected components of the universe are equivalent. Still more generally, we can permute arbitrarily any family of types all having the same automorphism ∞-group.

The simplest case of this is when all the types are rigid, i.e. have trivial automorphism ∞-group. The types $\mathbf{0}$ and $\mathbf{1}$ are both rigid, and at least with excluded middle no other sets are; but there can be rigid higher types. For instance, if $G$ is a group that is a set (i.e. a 1-group), then its Eilenberg-Mac Lane space $B G$ is a 1-type, and its automorphism ∞-group is a 1-type whose $\pi_0$ is the outer automorphisms of $G$ and whose $\pi_1$ is the center of $G$ . Thus, if $G$ has trivial outer automorphism group and trivial center, then $BG$ is rigid. Such groups are not uncommon, including for instance the symmetric group $S_n$ for any $n\neq 2,6$ . Thus, assuming excluded middle we can permute these $BS_n$ arbitrarily, producing uncountably many automorphisms of the universe.

In the converse direction, we recorded the following.

Theorem. If there is an automorphism of the universe that maps some inhabited type to the empty type, then excluded middle holds.

Corollary. If there is an automorphism $g:\mathcal{U}\to\mathcal{U}$ of the universe with $g(\mathbf{0})\neq\mathbf{0}$ , then the double negation

$\neg\neg\prod_{P:\mathcal{U}}\mathsf{isProp}(P)\to P+\neg P$

of the law of excluded middle holds.

This corollary relates to an unclaimed prize: if from an arbitrary equivalence $f:\mathcal{U}\to\mathcal{U}$ such that $f(X) \neq X$ for a particular $X:\mathcal{U}$ you get a non-provable consequence of excluded middle, then you get $X$ -many beers. So this corollary wins you 0 beers. Although perhaps sober, we think this is an achievement worth recording.

Using this corollary, in turn, we can win $\mathsf{LEM}_\mathcal{U}$ -many beers, where $\mathsf{LEM}_\mathcal{U}$ is excluded middle for propositions in the universe $\mathcal{U}$ . If $\mathcal{U} :\mathcal{V}$ we have $\mathsf{LEM}_\mathcal{U}:\mathcal{V}$ . Suppose $g$ is an automorphism of $\mathcal{V}$ with $g(\mathsf{LEM}_\mathcal{U})\neq\mathsf{LEM}_\mathcal{U}$ , then $\neg\neg\mathsf{LEM}_\mathcal{U}$ . For suppose that $\neg\mathsf{LEM}_\mathcal{U}$ , and hence $\mathsf{LEM}_\mathcal{U}=\mathbf{0}$ . So by the corollary, we obtain $\neg\neg\mathsf{LEM}_\mathcal{V}$ . But $\mathsf{LEM}_\mathcal{V}$ implies $\mathsf{LEM}_\mathcal{U}$ by cumulativity, so $\neg\neg\mathsf{LEM}_\mathcal{U}$ also holds, contradicting our assumption that $\neg\mathsf{LEM}_\mathcal{U}$ .

To date no one has been able to win 1 beer.

7 Responses to Parametricity, automorphisms of the universe, and excluded middle

Ulrik Buchholtz says:

27 January 2017 at 05:26

It’s a nice paper! Here’s a tiny positive observation regarding automorphisms of the universe: if we have an equivalence $f_0 : \mathcal U \to \mathcal U$ together with $f_1 : \Pi_{X,Y : \mathcal U}. (X \to Y) \simeq (f_0 X \to f_0 Y)$ , then $f_0$ is the identity. Indeed, plugging $f_0^{-1}1$ and $1$ into $f_1$ , we get $f_0 1 \simeq 1$ , and then plugging $1$ and an arbitrary $X : \mathcal U$ , we get $X \simeq (1 \to X) \simeq (1 \to f_0 X) \simeq f_0 X$ . Presumably, having more and more components of an automorphism of the universe as an $\infty$ -category, will entail that more and more of these components are those of the identity automorphism. So the first question is: how much do we need to add to ensure that also $f_1$ is the identity?

Mike Shulman says:

27 January 2017 at 06:48

Egbert’s recent arxiv post about the join construction, in which he shows that the propositions are precisely the “canonical” idempotents for the join, now has me wondering: how many idempotents are there on the universe?

Of course, any constant function is idempotent, as is the identity. And if P is any proposition, then $X\mapsto P\times X$ and $X\mapsto P*X$ are both idempotent. If $P=\mathbf{0}$ , then the former is constant at 0 and the latter is the identity; while if $P=\mathbf{1}$ , then the former is the identity and the latter is constant at 1. Of course, with excluded middle we can construct other idempotents, like sending X to 0 if it is empty and to 1 if it is inhabited. Can we construct any nonidentity, nonconstant idempotents on the universe without using classical axioms? Can we derive a taboo from the assumption of a nonidentity, nonconstant idempotent on the universe?

- Martin Escardo says:
  
  27 January 2017 at 11:39
  
  Consider any type $A$ with an identity $A \times A = A$ , such as the natural numbers. Then $X \mapsto A \times X$ and $X \mapsto (A \to X)$ are examples of non-identity, non-constant idempotents. In the case when $A$ is the natural numbers, we also have the example $X \mapsto A + X$ as we have an identity $A+A=A$ as well.
  
- Martin Escardo says:
  
  27 January 2017 at 15:16
  
  You must have had something else in mind. Another class of examples are n-truncations. In a similar vein, the double negation of a type is an idempotent.
  
- Martin Escardo says:
  
  27 January 2017 at 15:25
  
  But I have a similar question: can we define a non-trivial embedding of the universe into itself without using (a consequence of) excluded middle?
  
- Mike Shulman says:
  
  27 January 2017 at 15:38
  
  You must have had something else in mind.
  
  That’s a very kind way of saying “your brain must have been turned off”. (-:O
  
  - Martin Escardo says:
    
    27 January 2017 at 18:12
    
    I am sure I have said things in the internet with my brain switched off, too. And I am sure I have said silly things with my brain switched on, in the internet and otherwise. 🙂