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

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 *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

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.