Library CT.Isomorphism

Isomorphism between objects in a category. The idea is that if a morphism $f$ is an isomorphism, then there exists an inverse function such that composing it on either side yields the identity morphism. That is: Let $C$ be a category and $a, b$ be objects in C. Then a morphism $f : a \to b$ is an isomorphism if there exists another morphism $g : b \to a$ such that $g \circ f = id_a$ and $f \circ g = id_b$. In this case, $a$ and $b$ are said to be isomorphic to each other.