nLab monic map in a dagger 2-poset

Definition

A morphism $f \in Hom_A(a,b)$ of a dagger 2-poset $A$ is a monic map if it is an injective map.

The type of all monic maps in $Hom_A(a,b)$ is defined as

$$MonoMap(a, b) \coloneqq \sum_{f:Hom_A(a,b)} isInjective(f) \times isMap(f)$$

See also

• injective morphism in a dagger 2-poset
• map in a dagger 2-poset
• category of monic maps