Given sets $A$ and $B$ and a function $f\colon A \to B$, the inverse function of $f$ (if it exists) is the function $f^{-1}\colon B \to A$ such that both composite functions $f \circ f^{-1}$ and $f^{-1} \circ f$ are identity functions. Note that $f$ has an inverse function if and only if $f$ is a bijection, in which case this inverse function is unique.

In type theory

In type theory, given types $A$ and $B$ and a function $f:A \to B$, the inverse function of $f$ (if it exists) is the function $f^{-1}:B \to A$ such that $f^{-1}$ is a retraction of $f$, and for each element $b:B$, $f^{-1}(b)$ is the center of contraction of the fiber of $f$ at $b$.

Equivalently, the inverse function of $f$ (if it exists) is the function $f^{-1}:B \to A$ such that $f^{-1}$ is a retraction of $f$ and for each element $a:A$ and $b:B$, there is a function $r(a, b):(f(a) = b) \to (a = f^{-1}(b))$.