In a dagger category, is there a name for morphisms $f : X \rightarrow Y$ with $\mathrm{id}_X = f^\dagger \circ f$? In a dagger category, is there a name for morphisms $f : X \rightarrow Y$ with $\mathrm{id}_X = f^\dagger \circ f$? Clearly, every such arrow is a split monomorphism; further, if such an $f$ is self-adjoint, it is unitary.

An element $a$ of $C^*$-algebra is called an isometry if $a^* a = 1$. This coincides with the usual notion when applied to $B(H)$. Maybe we can just generalize this terminology to the setting of dagger categories. So call a morphism $f$ an isometry if $f^{\dagger} f = 1$. I don't know if this is standard.
