[[!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 $j_{B,A}:A \cong^\dagger B \cup (B \Rightarrow 0)$. ## Examples ## The dagger 2-poset of [[decidable set]]s and relations is an Boolean dagger 2-poset. ## See also ## * [[dagger 2-poset]] * [[Heyting dagger 2-poset]] * [[Boolean topical dagger 2-poset]] * [[Choice dagger 2-poset]]