An essentially algebraic dagger 2-poset is a dagger 2-poset whose category of maps is a syntactic category for essentially algebraic theories?. “Cartesian” is a very overloaded term and has a different meaning for bicategories, and “finitely complete” dagger 2-posets understood in category-theoretic terms are simply semiadditive dagger 2-posets.
Definition
An essentially algebraic dagger 2-poset is a dagger 2-poset such that
For each object , , with functionaldagger monomorphisms , , there is an object with functional dagger monomorphisms , , , such that and , and for every object with functional dagger monomorphisms , such that and , there is a functional dagger monomorphism such that .
Properties
For each object , the identity function is a functional dagger monomorphism, and for each object with a functional dagger monomorphism , .
The unitary isomorphism classes of functional dagger monomorphisms into every object is a meet-semilattice. Since every functional dagger monomorphism is a map, the category of maps is a finitely complete category?.
Examples
The dagger 2-poset of sets and relations is an essentially algebraic dagger 2-poset.