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 $gf=1_a$ and $fg=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 mere 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 f$ and $\epsilon : f 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} g'= (g f) g' = g (f g') = g 1_{b}= g \square$