Bijective iff it has a two-sided inverse

Statement

Let $f \colon A \to B$ be a function. Then $f$ is bijective if and only if there is a function $g \colon B \to A$ with $g \circ f = \mathrm{id}_A$ and $f \circ g = \mathrm{id}_B$.

Remarks

The function $g$ is then unique. It is the inverse function $f^{-1}$. This statement does not need the axiom of choice: for a bijection, $g(b)$ is the unique $a$ with $f(a) = b$. If $f$ has a left inverse $g$ and a right inverse $h$, then $g = h$.

Explanations

L1 human

A bijection can be undone in both directions. Going from $A$ to $B$ and back gives the start point, and going from $B$ to $A$ and back gives the start point too.