nLab
choice function

Idea

Given a set $A$, a choice function for $A$ chooses an element of every subset of $A$, except for the empty subset, of course.

Definition

Let $A$ be a set. Let ${𝒫}^{+}A$ be the collection of inhabited subsets of $A$. (So if $𝒫A$ is the power set of $A$, then ${𝒫}^{+}A$ is contained in $𝒫A$, and $𝒫A\setminus {𝒫}^{+}A=\{\varnothing \}$.)

A choice function for $A$ is a function $c$ from ${𝒫}^{+}A$ to $A$ such that $c(x)\in x$ (for every inhabited subset $x$).

Properties

$A$ is a choice set if it has a choice function. (The choice function need not be unique, and rarely is.)

The axiom of choice states that every set has a choice function.

Internalisation

In any topos, the definition above can be internalised; we get the notion of a choice morphism.