lean-choice

This development reproduces the results of my paper

J. Todd Wilson, "An Intuitionistic version of Zermelo's proof that every choice set can be well-ordered", J. Symbolic Logic, 66:3 (2001), 1121-1126.

Abstract: We give a proof, valid in any elementary topos, of the theorem of Zermelo that any set possessing a choice function for its set of inhabited subsets can be well-ordered. Our proof is considerably simpler than existing proofs in the literature and moreover can be seen as a direct generalization of Zermelo's own 1908 proof of his theorem.

Minor changes to the development have been made here in the process.