[[!redirects Boolean dagger 2-posets]] ## Contents ## * table of contents {:toc} ## Idea ## A Boolean dagger 2-poset is a dagger 2-poset whose [[category of maps]] is an [[Boolean category]]. ## Definition ## A **Boolean dagger 2-poset** $C$ is a [[Heyting dagger 2-poset]] where for each objects $A:Ob(C)$, $B:Ob(C)$ and functional dagger monomorphism $i_{B,A}:Hom(B,A)$, there is a [[unitary isomorphism in a dagger precategory|unitary isomorphism]] $j_{B,A}:A \cong^\dagger B \cup (B \Rightarrow 0)$. ## Properties ## * The [[unitary isomorphism in a dagger precategory|unitary isomorphism]] classes of functional dagger monomorphisms into every object $A$ is a [[Boolean algebra]]. Since every functional dagger monomorphism is a map, the [[category of maps]] is a [[Boolean category]]. ## Examples ## The dagger 2-poset of [[decidable set]]s and relations is an Boolean dagger 2-poset. ## See also ## * [[dagger 2-poset]] * [[conjunctive dagger 2-poset]] * [[coherent dagger 2-poset]] * [[Heyting dagger 2-poset]] * [[Boolean dagger 2-poset]] * [[Boolean topical dagger 2-poset]]