Homotopy Type Theory unitary isomorphism in a dagger precategory > history (Rev #1)

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.