Homotopy Type Theory monic map in a dagger 2-poset > history (Rev #1)


A morphism f:hom A(a,b)f:hom_A(a,b) of a dagger 2-poset AA is a monic map if it is a functional dagger monomorphism.

The type of all monic maps in hom A(a,b)hom_A(a,b) is defined as

Inj(a,b) f:hom A(a,b)isFunctional(f)×isMonic(f)Inj(a, b) \coloneqq \sum_{f:hom_A(a,b)} isFunctional(f) \times isMonic(f)

See also

category: category theory

Revision on April 25, 2022 at 14:11:52 by Anonymous?. See the history of this page for a list of all contributions to it.