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}$ .