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

Contents

Definition

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

Examples

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

See also

• unital dagger 2-poset