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

Showing changes from revision #1 to #2: Added | Removed | Changed


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 June 6, 2022 at 23:27:58 by Anonymous?. See the history of this page for a list of all contributions to it.