# Inverse Morphism is Unique

## Theorem

Let $\mathbf C$ be a metacategory.

Let $f: C \to D$ be an isomorphism of $\mathbf C$.

Then $f$ admits a unique inverse morphism $g: D \to C$.

## Proof

Since $f$ is an isomorphism, it admits at least one inverse morphism.

Now let $g, g': D \to C$ be two inverse morphisms for $f$.

Then:

 $\displaystyle g$ $=$ $\displaystyle g \circ \operatorname{id}_D$ $\quad$ Axiom $(C2)$ for metacategories $\quad$ $\displaystyle$ $=$ $\displaystyle g \circ \left({f \circ g'}\right)$ $\quad$ $g'$ is an inverse morphism for $f$ $\quad$ $\displaystyle$ $=$ $\displaystyle \left({g \circ f}\right) \circ g'$ $\quad$ Axiom $(C3)$ for metacategories $\quad$ $\displaystyle$ $=$ $\displaystyle {\operatorname{id}_C} \circ g'$ $\quad$ $g$ is an inverse morphism for $f$ $\quad$ $\displaystyle$ $=$ $\displaystyle g'$ $\quad$ Axiom $(C2)$ for metacategories $\quad$

In conclusion, $g = g'$.

Hence the result.

$\blacksquare$