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

Contents

Definition

A division dagger 2-poset is a dagger 2-poset $C$ such that for every object $A:Ob(C)$, $B:Ob(C)$, and $C:Ob(C)$ and morphisms $f:Hom(A, B)$ and $g:Hom(A, C)$ there is a morphism $g/f:Hom(B, C)$ such that for every morphism $h:Hom(B, C)$, $(h \leq g/f) \iff (h \circ g = f)$.

Examples

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

See also

• dagger 2-poset