"First" in this case was just getting the first element of the iterator, it wasn't related to choosing a value from the set. The Axiom of Choice is equivalent

"First" in this case was just getting the first element of the iterator, it wasn't related to choosing a value from the set. The Axiom of Choice is equivalent to the following: 1) "For any set A, there exists a function from non-empty elements of the power set of A to elements of A." Which is equivalent to: 2) "There exists a function that takes a non-empty set as input, and returns an element of that set" 2 -> 1, since we can take the function 2 defines, and use it to define the function from 1. 1 -> 2 since we can define 2 as such: For a set A, take the power set of A. Then take the function that 1 claims exists. Use that function to get an element of A, since A is an element of its power set. But back to your core point: But I agree that Iterator is a bad fit for the axiom of choice, since we have an (uncountable) number of sets to pick from. Here's a way to phrase it programmatically that allows for uncountable sets-of-sets: The axiom of choice claims that given a set of non-empty sets, you can construct a new set which contains an element from each of the sets. pickOneFromEach :: Set (NonEmptySet a) -> NonEmptySet a If you have a function: choose :: NonEmptySet a -> a And a function: map :: (a -> b) -> Set a -> Set b then you can define pickOneFromEach as follows: pickOneFromEach setOfSets = map choose setOfSets