[[!redirects geometric dagger 2-posets]] ## Contents ## * table of contents {:toc} ## Idea ## A geometric dagger 2-poset is a dagger 2-poset whose [[category of maps]] is a geometric category. ## Definition ## A **geometric 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 [[monic map in a dagger 2-poset|monic map]] $i_{0,A}:Hom(0,A)$ such that for each object $B:Ob(C)$ with a monic map $i_{B,A}:Hom(B,A)$, there is a monic map $i_{0,B}:Hom(0,B)$ such that $i_{B,A} \circ i_{0,B} = i_{0,A}$. * For each object $A:Ob(C)$, type $T$, and family of objects $B:T \to Ob(C)$, with monic maps $$t:T \vdash i_{B(t),A}:Hom(B(t),A)$$ there is an object $$\bigcup_{t:T} B(t):Ob(C)$$ with monic maps $$i_{\bigcup_{t:T} B(t),A}:Hom(\bigcup_{t:T} B(t),A)$$ $$t:T \vdash i_{B(t),\bigcup_{t:T} B(t)}:Hom(B(t),\bigcup_{t:T} B(t))$$ such that $$t:T \vdash i_{\bigcup_{t:T} B(t),A} \circ i_{B(t),\bigcup_{t:T} B(t)} = i_{B(t),A}$$ and for every object $D:Ob(C)$ with monic maps $i_{D,A}:Hom(D,A)$ $i_{B,D}:Hom(B,D)$, $i_{E,D}:Hom(E,D)$ such that $i_{D,A} \circ i_{B,D} = i_{B,A}$ and $i_{D,A} \circ i_{E,D} = i_{E,A}$, there is a monic map $$i_{\bigcup_{t:T} B(t),D}:Hom(\bigcup_{t:T} B(t),D)$$ such that $$i_{D,A} \circ i_{\bigcup_{t:T} B(t),D} = i_{\bigcup_{t:T} B(t),A}$$ * For each object $A:Ob(C)$, $B:Ob(C)$, $E:Ob(C)$ with monic maps $i_{B,A}:Hom(B,A)$, $i_{E,A}:Hom(E,A)$, there is an object $B \cap E:Ob(C)$ with monic maps $i_{B \cap E,A}:Hom(B \cap E,A)$, $i_{B \cap E,B}:Hom(B \cap E,B)$, $i_{B \cap E,E}:Hom(B \cap E,E)$, such that $i_{B,A} \circ i_{B \cap E,B} = i_{B \cap E,A}$ and $i_{E,A} \circ i_{B \cap E,E} = i_{B \cap E,A}$, and for every object $D:Ob(C)$ with monic maps $i_{D,A}:Hom(D,A)$ $i_{D,B}:Hom(D,B)$, $i_{D,E}:Hom(D,E)$ such that $i_{B,A} \circ i_{D,B} = i_{D,A}$ and $i_{E,A} \circ i_{D,E} = i_{D,A}$, there is a monic map $i_{D,B \cap E}:Hom(D,B \cap E)$ such that $i_{B \cap E,A} \circ i_{D,B \cap E} = i_{D,A}$. * For each object $A:Ob(C)$, $E:Ob(C)$, with monic maps $i_{E,A}:Hom(E,A)$ and type $T$, and family of objects $B:T \to Ob(C)$, with monic maps $$t:T \vdash i_{B(t),A}:Hom(B(t),A)$$, there is a [[unitary isomorphism in a dagger precategory|unitary isomorphism]] $$j_{B,C,E}:E \cap (\bigcup_{t:T} B(t)) \cong^\dagger \bigcup_{t:T} E \cup B(t)$$ ## Properties ## * For each object $A:Ob(C)$, the identity function $1_A:Hom(A,A)$ is a monic map, and for each object $B:Ob(C)$ with a monic map $i_{B,A}:Hom(B,A)$, $1_A \circ i_{B,A} = i_{B,A}$. * The [[unitary isomorphism in a dagger precategory|unitary isomorphisms]] classes of monic maps into every object $A$ is a [[frame]]. Since every monic map is a map, the [[category of maps]] is a [[geometric category]]. ## Examples ## The dagger 2-poset of sets and relations is a coherent dagger 2-poset. ## See also ## * [[dagger 2-poset]] * [[conjunctive dagger 2-poset]] * [[coherent dagger 2-poset]] * [[geometric dagger 2-poset]] * [[Heyting dagger 2-poset]] * [[Boolean dagger 2-poset]] * [[elementarily topical dagger 2-poset]]