Author Archives: Auke Booij

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 … Continue reading →

Exercise 6.9 of the HoTT book tells us that, and assuming LEM, we can exhibit a function  such that is a non-identity function  I have proved the converse of this. Like in exercise 6.9, we assume univalence. Parametricity In a … Continue reading →