g is a partial inverse to f (an injective but not necessarily surjective function) if g y = some x implies f x = y, and g y = none implies that y is not in the range of f.

We can use choice to construct explicitly a partial inverse for a given injective function f.

Construct the inverse for a function f on domain s.

The inverse of a function (which is a left inverse if f is injective and a right inverse if f is surjective).

The inverse of a surjective function. (Unlike inv_fun, this does not require α to be inhabited.)

A function is involutive, if f ∘ f = id.