Homotopy Type Theory well-pointed dagger 2-poset > history (Rev #2, changes)

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



A well-pointed dagger 2-poset is a unital dagger 2-poset CC such that for every object A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) and maps f:Hom(A,B)f:Hom(A, B), g:Hom(A,B)g:Hom(A, B) and x:Hom(𝟙,A)x:Hom(\mathbb{1}, A), fx=gxf \circ x = g \circ x implies f=gf = g.


The dagger 2-poset of sets and relations is a well-pointed dagger 2-poset.

See also

Revision on June 7, 2022 at 02:05:38 by Anonymous?. See the history of this page for a list of all contributions to it.