An essentially conjunctive algebraic dagger 2-poset is a dagger 2-poset whose internal logic of thecategory of maps is consists a only syntactic of category conjunction foressentially algebraic theories? . “Cartesian” is a very overloaded term and has true a different meaning for bicategories, and “finitely complete” dagger 2-posets understood in category-theoretic terms are simplysemiadditive dagger 2-posets . , or equivalently, whosecategory of maps has all pullback?s of monic maps.
Definition
An essentially conjunctive 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 a essentially conjunctive algebraic dagger 2-poset.