## Definition ## A morphism $f:hom_A(a,b)$ of a [[precategory]] $A$ is an **isomorphism** if there is a morphism $g:hom_A(b,a)$ such that $g \circ f = 1_a$ and $f\circ g = 1_b$. We write $a \cong b$ for the type of such isomorphisms. If $f:a \cong b$, then we write $f^{-1}$ for its inverse which is uniquely determined by Lemma 9.1.3. ## Properties ## ### Lemma 9.1.3 ### For any $f : hom_A(a,b)$ the type "f is an isomorphism" is a [[proposition]]. Therefore, for any $a,b:A$ the type $a \cong b$ is a set. *Proof.* Suppose given $g:hom_A(b,a)$ and $\eta:1_a = g \circ f$ and $\epsilon : f \circ g = 1_b$, and similarly $g',\eta'$, and $\epsilon'$. We must show $(g,\eta,\epsilon)=(g',\eta', \epsilon')$. But since all hom-sets are sets , their identity types are mere propositions, so it suffices to show $g=g'$. For this we have $ g' = 1_{a} \circ g'= (g \circ f) \circ g' = g \circ (f \circ g') = g \circ 1_{b}= g \square$ ## See also ## [[Category theory]] ## References ## [[HoTT Book]] category: category theory