Homotopy Type Theory category of maps > history (Rev #3)


Given a dagger 2-poset AA, the category of maps Map(A)Map(A) is the sub-2-poset whose objects are the objects of AA and whose morphisms are the maps of AA. In every dagger 2-poset, given two maps f:hom A(a,b)f:hom_A(a,b) and g:hom A(a,b)g:hom_A(a,b), if fgf \leq g, then f=gf = g. This means that the sub-2-poset Map(A)Map(A) is a category and trivially a 2-poset.


  • For the dagger 2-poset of sets and relations RelRel, the category of maps Map(Rel)Map(Rel) is equivalent to the category of sets and functions SetSet.

See also

category: category theory

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