[[!redirects injective map in a dagger 2-poset]] ## Definition ## A morphism $f:hom_A(a,b)$ of a [[dagger 2-poset]] $A$ is a **monic map** if it is a [[functional dagger morphism in a dagger 2-poset|functional]] [[dagger monomorphism in a dagger precategory|dagger monomorphism]]. The type of all monic maps in $hom_A(a,b)$ is defined as $$Inj(a, b) \coloneqq \sum_{f:hom_A(a,b)} isFunctional(f) \times isMonic(f)$$ ## See also ## * [[functional dagger morphism in a dagger 2-poset]] * [[entire dagger morphism in a dagger 2-poset]] * [[map in a dagger 2-poset]] * [[category of monic maps]] category: category theory