nLab epic map in a dagger 2-poset

Redirected from "injective map in a dagger 2-poset".
Note: monic map in a dagger 2-poset and epic map in a dagger 2-poset both redirect for "injective map in a dagger 2-poset".

Definition

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

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

EpiMap(a, b) \coloneqq \sum_{f:Hom_A(a,b)} isOnto(f) \times isMap(f)