Homotopy Type Theory geometric dagger 2-poset > history (Rev #1)

Contents

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 CC such that

  • There is an object 0:Ob(C)0:Ob(C) such that for each object A:Ob(C)A:Ob(C), there is a monic map i 0,A:Hom(0,A)i_{0,A}:Hom(0,A) such that for each object B:Ob(C)B:Ob(C) with a monic map i B,A:Hom(B,A)i_{B,A}:Hom(B,A), there is a monic map i 0,B:Hom(0,B)i_{0,B}:Hom(0,B) such that i B,Ai 0,B=i 0,Ai_{B,A} \circ i_{0,B} = i_{0,A}.

  • For each object A:Ob(C)A:Ob(C), type TT, and family of objects B:TOb(C)B:T \to Ob(C), with monic maps

    t:Ti B(t),A:Hom(B(t),A)t:T \vdash i_{B(t),A}:Hom(B(t),A)

    there is an object

    t:TB(t):Ob(C)\bigcup_{t:T} B(t):Ob(C)

    with monic maps

    i t:TB(t),A:Hom( t:TB(t),A)i_{\bigcup_{t:T} B(t),A}:Hom(\bigcup_{t:T} B(t),A)
    t:Ti B(t), t:TB(t):Hom(B(t), t:TB(t))t:T \vdash i_{B(t),\bigcup_{t:T} B(t)}:Hom(B(t),\bigcup_{t:T} B(t))

    such that

    t:Ti t:TB(t),Ai B(t), t:TB(t)=i B(t),At: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)D:Ob(C) with monic maps i D,A:Hom(D,A)i_{D,A}:Hom(D,A) i B,D:Hom(B,D)i_{B,D}:Hom(B,D), i E,D:Hom(E,D)i_{E,D}:Hom(E,D) such that i D,Ai B,D=i B,Ai_{D,A} \circ i_{B,D} = i_{B,A} and i D,Ai E,D=i E,Ai_{D,A} \circ i_{E,D} = i_{E,A}, there is a monic map

    i t:TB(t),D:Hom( t:TB(t),D)i_{\bigcup_{t:T} B(t),D}:Hom(\bigcup_{t:T} B(t),D)

    such that

    i D,Ai t:TB(t),D=i t:TB(t),Ai_{D,A} \circ i_{\bigcup_{t:T} B(t),D} = i_{\bigcup_{t:T} B(t),A}
  • For each object A:Ob(C)A:Ob(C), B:Ob(C)B:Ob(C), E:Ob(C)E:Ob(C) with monic maps i B,A:Hom(B,A)i_{B,A}:Hom(B,A), i E,A:Hom(E,A)i_{E,A}:Hom(E,A), there is an object BE:Ob(C)B \cap E:Ob(C) with monic maps i BE,A:Hom(BE,A)i_{B \cap E,A}:Hom(B \cap E,A), i BE,B:Hom(BE,B)i_{B \cap E,B}:Hom(B \cap E,B), i BE,E:Hom(BE,E)i_{B \cap E,E}:Hom(B \cap E,E), such that i B,Ai BE,B=i BE,Ai_{B,A} \circ i_{B \cap E,B} = i_{B \cap E,A} and i E,Ai BE,E=i BE,Ai_{E,A} \circ i_{B \cap E,E} = i_{B \cap E,A}, and for every object D:Ob(C)D:Ob(C) with monic maps i D,A:Hom(D,A)i_{D,A}:Hom(D,A) i D,B:Hom(D,B)i_{D,B}:Hom(D,B), i D,E:Hom(D,E)i_{D,E}:Hom(D,E) such that i B,Ai D,B=i D,Ai_{B,A} \circ i_{D,B} = i_{D,A} and i E,Ai D,E=i D,Ai_{E,A} \circ i_{D,E} = i_{D,A}, there is a monic map i D,BE:Hom(D,BE)i_{D,B \cap E}:Hom(D,B \cap E) such that i BE,Ai D,BE=i D,Ai_{B \cap E,A} \circ i_{D,B \cap E} = i_{D,A}.

  • For each object A:Ob(C)A:Ob(C), E:Ob(C)E:Ob(C), with monic maps i E,A:Hom(E,A)i_{E,A}:Hom(E,A) and type TT, and family of objects B:TOb(C)B:T \to Ob(C), with monic maps

    t:Ti B(t),A:Hom(B(t),A)t:T \vdash i_{B(t),A}:Hom(B(t),A)

Properties

  • For each object A:Ob(C)A:Ob(C), the identity function 1 A:Hom(A,A)1_A:Hom(A,A) is a monic map, and for each object B:Ob(C)B:Ob(C) with a monic map i B,A:Hom(B,A)i_{B,A}:Hom(B,A), 1 Ai B,A=i B,A1_A \circ i_{B,A} = i_{B,A}.

  • The unitary isomorphisms classes of monic maps into every object AA 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

Revision on April 25, 2022 at 10:43:20 by Anonymous?. See the history of this page for a list of all contributions to it.