# nLab monic map in a dagger 2-poset

### Context

#### Higher category theory

higher category theory

## 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)$