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

Contents

Definition

A 2-poset $A$ is a category $C$ such that

• For each object $A:Ob(C)$ and $B:Ob(C)$ and morphism $R:Hom(A, B)$, $S:Hom(A, B)$, a propositional binary relation $R \leq_{A, B} S$
• For each object $A:Ob(C)$ and $B:Ob(C)$ and morphism $R:Hom(A, B)$, $R \leq_{A, B} R$.
• For each object $A:Ob(C)$ and $B:Ob(C)$ and morphism $R:Hom(A, B)$, $S:Hom(A, B)$, $R \leq_{A, B} S$ and $S \leq_{A, B} R$ implies $R = S$.
• For each object $A:Ob(C)$ and $B:Ob(C)$ and morphism $R:Hom(A, B)$, $S:Hom(A, B)$, $T:Hom(A, B)$, $R \leq_{A, B} S$ and $S \leq_{A, B} T$ implies $R \leq_{A, B} T$.

See also

• category
• dagger 2-poset
• 2-preorder