nLab injective morphism in a dagger 2-poset

Context

Higher category theory

higher category theory

Idea

A morphism similar to how injective relations are defined in Rel

Definition

A morphism $f:hom_A(a,b)$ of a dagger 2-poset $A$ is an injective morphism if $f^\dagger \circ f \leq 1_a$.