choose tactic

Stream: new members

[abaaba]

image.png
I couldn't see how this do with axiom of choice ... neither can I understand its meaning ....

[Mario Carneiro]

tactic#choose is probably easier to read

[Mario Carneiro]

If you have a theorem h saying that for all x : A, there exists y : B such that P x y, then choose h with f h' produces f : A -> B and h' saying that P x (f x). That's the axiom of choice

[Mario Carneiro]

here f is the set of choices, one y for each x

[abaaba]

I think it would make sense to me if A is restricted to Set X, and y is of type X. But how does it generalize to other types?

[Mario Carneiro]

This is maybe not exactly the version of the axiom of choice that you are thinking of. Here's the version from wikipedia that gets pretty close to the type theory version:

In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that a Cartesian product of a collection of non-empty sets is non-empty. Informally put, the axiom of choice says that given any collection of bins, each containing at least one object, it is possible to make a selection of exactly one object from each bin, even if the collection is infinite. Formally, it states that for every indexed family $(S_{i})_{i\in I}$ of nonempty sets there exists an indexed family $(x_{i})_{i\in I}$ of elements such that $x_{i}\in S_{i}$ for every $i\in I$.

[Mario Carneiro]

To map this to the version I just said, let $I$ be A, and let $S_i$ be {y : B // P i y}

[Mario Carneiro]

The family λ x, {y : B // P x y} is a family of nonempty sets, because for every x there exists y such that P x y, and the resulting indexed family $(x_i)_{i\in I}$ is f, or more precisely λ x, ⟨f x, h' x⟩; for each x, f x : B and h' x : P x (f x) so ⟨f x, h' x⟩ : {y : B // P x y} as desired.