Homotopy Type Theory unital dagger 2-poset > history (Rev #1)

Contents

Definition

A unital dagger 2-poset is a dagger 2-poset $C$ with an object $\mathbb{1}:Ob(C)$ such that for every morphism $f:Hom(\mathbb{1}, \mathbb{1})$, $f \leq 1_\mathbb{1}$, and for every object $A:Ob(C)$, there is a morphism $u:A \to \mathbb{1}$ such that $1_A \leq u \circ u^\dagger$.

Examples

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

See also

• dagger 2-poset
• well-pointed dagger 2-poset