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 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
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
Theorem. There exist
Notice that there are no requirements on the type
Theorem. There exist
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
The above automorphism swaps the empty type
The simplest case of this is when all the types are rigid, i.e. have trivial automorphism ∞-group. The types
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
of the law of excluded middle holds.
This corollary relates to an unclaimed prize: if from an arbitrary equivalence
Using this corollary, in turn, we can win
To date no one has been able to win 1 beer.