NOTE: This site has just upgraded to Forester 5.x and is still having some style and functionality issues, we will fix them ASAP.

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.