Monthly Archives: February 2016

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 →