as we may assume $a$ and $b$ are the same, which means $1_a:hom_A(a,a)$, which is a unitary isomorphism.

$A$ is a univalent dagger category or a saturated dagger category if for all $a,b:A$, $idtouiso_{a,b}$ is an equivalence.

The inverse of $idtouiso$ is denoted $uisotoid$.

Examples

Every univalent groupoid is a univalent dagger category with $f^\dagger = f^{-1}$.

The dagger category $Rel$ of sets and relations is a univalent dagger category with $f^\dagger$ representing the opposite relation of a relation $f$.

The dagger category $Hilb\mathbb{R}$ of Hilbert spaces over the real numbers and linear maps is a univalent dagger category with $f^\dagger$ representing the adjoint linear map of $f$.