Author Archives: Auke Booij

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

Posted in Foundations | 7 Comments

Parametricity and excluded middle

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

Posted in Foundations | 13 Comments