Parametricity, automorphisms of the universe, and excluded middle

This is an announcement of a paper in the area of type theory and parametricity.

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 the Homotopy Type Theory 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 published in the post-proceedings of TYPES 2016 (see also the preprint on arXiv).