definition. section, choice [leinster2016basic, sec. 3.1] [tt-003E]
definition. section, choice [leinster2016basic, sec. 3.1] [tt-003E]
Let \(f: X \to Y\) be an arrow in a category \({\cal C}\). A section (or right inverse) of \(f\) is an arrow \(i: Y \to X\) in \({\cal C}\) such that \(i \mathbin {\bullet } f = \mathit {1}_X\).
In \(\mathbf {Set}\), any arrow with a section is certainly surjective. The converse statement is called the axiom of choice:
Every surjection has a section.
It is called choice because specifying a section of \(f: X \to Y\) amounts to choosing, for each \(y \in Y\), an element of the nonempty set \(\{x \in X \mid f(x)=y\}\).
It's closely related to § [tt-004T], need to figure out how to incooperate.