## Definition ## A morphism $f:hom_A(a,b)$ of a [[dagger precategory]] $A$ is a **unitary isomorphism** or **dagger isomorphism** if $f^\dagger \circ f=1_a$ and $f \circ f^\dagger =1_b$. We write $a \cong^\dagger b$ for the type of unitary isomorphisms. ## Properties ## For any $f : hom_A(a,b)$ the type "$f$ is a unitary isomorphism" is a [[proposition]]. Therefore, for any $a,b:A$ the type $a \cong^\dagger b$ is a set. For $a,b:A$, if $p:(a = b)$, then $idtoiso(p)$ (as defined in [[precategory]]) is a unitary isomorphism. ## See also ## [[Category theory]] ## References ## * [[HoTT Book]] * Chris Heunen, Andre Kornell, Axioms for the category of Hilbert spaces ([arXiv:2109.07418](https://arxiv.org/abs/2109.07418)) category: category theory