Isomorphism

Collection

 context $A,B\in\mathrm{Ob}_{\bf C}$ definiendum $f$ in $A\cong B$ inclusion $f:{\bf C}[A,B]$ exists $f^{-1}:{\bf C}[B,A]$ postulate $f^{-1}\circ f=\mathrm{id}_A$ postulate $f\circ f^{-1}=\mathrm{id}_B$