[[!redirects coherent dagger 2-posets]] ## Contents ## * table of contents {:toc} ## Idea ## A coherent dagger 2-poset is a dagger 2-poset whose [[category of maps]] is a coherent category. ## Definition ## A **coherent dagger 2-poset** is a [[dagger 2-poset]] $C$ such that * There is an object $0:Ob(C)$ such that for each object $A:Ob(C)$, there is a [[functional dagger morphism in a dagger 2-poset|functional]] [[dagger monomorphism in a dagger precategory|dagger monomorphism]] $i_{0,A}:Hom(0,A)$ such that for each object $B:Ob(C)$ with a functional dagger monomorphism $i_{B,A}:Hom(B,A)$, there is a functional dagger monomorphism $i_{0,B}:Hom(0,B)$ such that $i_{B,A} \circ i_{0,B} = i_{0,A}$. * For each object $A:Ob(C)$, $B:Ob(C)$, $E:Ob(C)$ with functional dagger monomorphisms $i_{B,A}:Hom(B,A)$, $i_{E,A}:Hom(E,A)$, there is an object $B \cup E:Ob(C)$ with functional dagger monomorphisms $i_{B \cup E,A}:Hom(B \cup E,A)$, $i_{B,B \cup E}:Hom(B,B \cup E)$, $i_{E,B \cup E}:Hom(E,B \cup E)$, such that for every object $D:Ob(C)$ with functional dagger monomorphisms $i_{D,A}:Hom(D,A)$ $i_{B,D}:Hom(B,D)$, $i_{E,D}:Hom(E,D)$, there is a functional dagger monomorphism $i_{B \cup E,D}:Hom(B \cup E,D)$. * For each object $A:Ob(C)$, the identity function $1_A:Hom(A,A)$ is a functional dagger monomorphism, and for each object $B:Ob(C)$ with a functional dagger monomorphism $i_{B,A}:Hom(B,A)$, there is trivially the same functional dagger monomorphism $i_{B,A}:Hom(B,A)$ such that $1_A \circ i_{B,A} = i_{B,A}$. * For each object $A:Ob(C)$, $B:Ob(C)$, $E:Ob(C)$ with functional dagger monomorphisms $i_{B,A}:Hom(B,A)$, $i_{E,A}:Hom(E,A)$, there is an object $B \cap E:Ob(C)$ with functional dagger monomorphisms $i_{A,B \cap E}:Hom(A,B \cap E)$, $i_{B \cap E,B}:Hom(B \cap E,B)$, $i_{B \cap E,E}:Hom(B \cap E,E)$, such that for every object $D:Ob(C)$ with functional dagger monomorphisms $i_{D,A}:Hom(D,A)$ $i_{D,B}:Hom(D,B)$, $i_{D,E}:Hom(D,E)$, there is a functional dagger monomorphism $i_{D,B \cup E}:Hom(D,B \cup E)$. * For each object $A:Ob(C)$, $B:Ob(C)$, $D:Ob(C)$, $E:Ob(C)$ with functional dagger monomorphisms $i_{B,A}:Hom(B,A)$, $i_{D,A}:Hom(D,A)$, $i_{E,A}:Hom(E,A)$, there is a [[unitary isomorphism in a dagger precategory|unitary isomorphism]] $$j_{B,C,E}:E \cap (B \cup C) \cong^\dagger (E \cap B) \cup (E \cap C)$$ ## Properties ## * The [[unitary isomorphism in a dagger precategory|unitary isomorphisms]] classes of functional dagger monomorphisms into every object $A$ is a [[distributive lattice]]. Since every functional dagger monomorphism is a map, the [[category of maps]] is a [[coherent category]]. ## Examples ## The dagger 2-poset of sets and relations is a coherent dagger 2-poset. ## See also ## * [[dagger 2-poset]] * [[essentially algebraic dagger 2-poset]] * [[coherent dagger 2-poset]] * [[Heyting dagger 2-poset]] * [[Boolean dagger 2-poset]] * [[elementarily topical dagger 2-poset]]