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 $\mathcal{P}^+A$ be the collection of inhabited subsets of $A$. (So if $\mathcal{P}A$ is the power set of $A$, then $\mathcal{P}^+A$ is contained in $\mathcal{P}A$, and $\mathcal{P}A \setminus \mathcal{P}^+A = \{\empty\}$.)

A choice function for $A$ is a function $c$ from $\mathcal{P}^+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 notions of choice object and choice morphism.