book
book copied to clipboard
Mention global choice in chapter 10
It was suggested some time ago that it would be good to mention somewhere in chapter 10 that unlike the ordinary axiom of choice, the axiom of global choice, at least in the obvious form "forall X:Set, ||X|| -> X", is incompatible with univalence. This is basically exercise 3.11, but it might be good to recall it in chapter 10. However, I'm not sure where?