KTH/SU Mathematics Colloquium
05-04-06
Per Martin-Löf, Stockholm University
Zermelo's axiom of choice: what was the problem with it?
An analysis of Zermelo's axiom of choice in constructive
type theory reveals that the problem with it is not the existence of
the choice function but the extensionality of it, which is not visible
in an extensional framework where all functions are by definition
extensional.