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