# Zulip Chat Archive

## Stream: new members

### Topic: choose tactic

#### abaaba (Oct 14 2021 at 08:24):

image.png

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

#### Mario Carneiro (Oct 14 2021 at 08:25):

tactic#choose is probably easier to read

#### Mario Carneiro (Oct 14 2021 at 08:27):

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 (Oct 14 2021 at 08:27):

here `f`

is the set of choices, one `y`

for each `x`

#### abaaba (Oct 14 2021 at 08:29):

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 (Oct 14 2021 at 08:40):

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 (Oct 14 2021 at 08:42):

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 (Oct 14 2021 at 08:44):

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.

Last updated: Dec 20 2023 at 11:08 UTC