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

Idea

A dagger 2-poset whose category of maps is a cartesian monoidal category?.

Definition

A cartesian dagger 2-poset is a unital dagger 2-poset $C$ such that for every object $A:Ob(C)$ and $B:Ob(C)$, $Hom(A, B)$ is a meet-semilattice with top morphism $\top_{A,B}$ and meet operation $\wedge_{A,B}$, and there is an object $A \otimes B:Ob(C)$ such that there exist maps $p_A:A \otimes B \to A$ and $p_B:B \otimes B \to B$ such that $p_B^\dagger \circ p_A = \top_{A,B}$ and $u_B \circ p_B = u_A \circ p_A$, for every onto morphism $u_A:A \to \mathbb{1}$ and $u_B:A \to \mathbb{1}$.

Examples

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