Homotopy Type Theory coherent dagger 2-poset > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Contents

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 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 functional dagger monomorphism 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 functional dagger monomorphism i B,A:Hom(B,A)i_{B,A}:Hom(B,A), there is a functional dagger monomorphism 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), B:Ob(C)B:Ob(C), E:Ob(C)E:Ob(C) with functional dagger monomorphisms 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 \cup E:Ob(C) with functional dagger monomorphisms i BE,A:Hom(BE,A)i_{B \cup E,A}:Hom(B \cup E,A), i B,BE:Hom(B,BE)i_{B,B \cup E}:Hom(B,B \cup E), i E,BE:Hom(E,BE)i_{E,B \cup E}:Hom(E,B \cup E) , such that for every objectDi BE,A :Obi B,BE ( =Ci B,A) D:Ob(C) i_{B \cap E,A} \circ i_{B,B \cap E} = i_{B,A} with and functional dagger monomorphismsi D BE,A :Homi E,BE ( =Di E,A,A) i_{D,A}:Hom(D,A) i_{B \cap E,A} \circ i_{E,B \cap E} = i_{E,A} ,and for every objecti B,DD: Hom Ob( B C,D) i_{B,D}:Hom(B,D) D:Ob(C) , with functional dagger monomorphismsi E,D,A:Hom(E,D,A) i_{E,D}:Hom(E,D) i_{D,A}:Hom(D,A) , there is a functional dagger monomorphismi BE,D:Hom(BE,D) i_{B i_{B,D}:Hom(B,D) \cup E,D}:Hom(B \cup E,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 functional dagger monomorphism i BE,D:Hom(BE,D)i_{B \cup E,D}:Hom(B \cup E,D) such that i D,Ai BE,D=i BE,Ai_{D,A} \circ i_{B \cup E,D} = i_{B \cup E,A}

  • For each object A:Ob(C)A:Ob(C) , the identity function1 AB: Hom Ob( A C,A) 1_A:Hom(A,A) B:Ob(C) , is a functional dagger monomorphism, and for each object B E:Ob(C) B:Ob(C) E:Ob(C) with a functional dagger monomorphism monomorphismsi B,A:Hom(B,A)i_{B,A}:Hom(B,A) , there is trivially the same functional dagger monomorphismi B E,A:Hom( B E,A) i_{B,A}:Hom(B,A) i_{E,A}:Hom(E,A) , such there that is an object1 ABi B,AE = :i B,AOb(C) 1_A B \circ \cap i_{B,A} E:Ob(C) = i_{B,A} with functional dagger monomorphisms 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 functional dagger monomorphisms 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 functional dagger monomorphism 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), B:Ob(C)B:Ob(C), E D:Ob(C) E:Ob(C) D:Ob(C) , with functional dagger monomorphismsi B,AE: Hom Ob( B C,A) i_{B,A}:Hom(B,A) E:Ob(C) , with functional dagger monomorphismsi E B,A:Hom( E B,A) i_{E,A}:Hom(E,A) i_{B,A}:Hom(B,A) , there is an objectBi D,AE: Ob Hom( C D,A) B i_{D,A}:Hom(D,A) \cap E:Ob(C) , with functional dagger monomorphismsi A,BE,A:Hom(A,BE,A) i_{A,B i_{E,A}:Hom(E,A) \cap E}:Hom(A,B \cap E) , there is ai BE,B:Hom(BE,B)i_{B \cap E,B}:Hom(B \cap E,B)unitary isomorphism, i BE,E:Hom(BE,E)i_{B \cap E,E}:Hom(B \cap E,E), such that for every object D:Ob(C)D:Ob(C) with functional dagger monomorphisms 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), there is a functional dagger monomorphism i D,BE:Hom(D,BE)i_{D,B \cup E}:Hom(D,B \cup E).

    j B,C,E:E(BC) (EB)(EC)j_{B,C,E}:E \cap (B \cup C) \cong^\dagger (E \cap B) \cup (E \cap C)
  • For each object A:Ob(C)A:Ob(C), B:Ob(C)B:Ob(C), D:Ob(C)D:Ob(C), E:Ob(C)E:Ob(C) with functional dagger monomorphisms i B,A:Hom(B,A)i_{B,A}:Hom(B,A), i D,A:Hom(D,A)i_{D,A}:Hom(D,A), i E,A:Hom(E,A)i_{E,A}:Hom(E,A), there is a unitary isomorphism

    j B,C,E:E(BC) (EB)(EC)j_{B,C,E}:E \cap (B \cup C) \cong^\dagger (E \cap B) \cup (E \cap C)

Properties

  • Theunitary isomorphisms

    For each object A:Ob(C)A:Ob(C), the identity function 1 A:Hom(A,A)1_A:Hom(A,A) is a functional dagger monomorphism, and for each object B:Ob(C)B:Ob(C) with a functional dagger monomorphism 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}.

    classes of functional dagger monomorphisms into every objectAA is a distributive lattice. Since every functional dagger monomorphism is a map, the category of maps is a coherent category?.
  • The unitary isomorphisms classes of functional dagger monomorphisms into every object AA 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

Revision on April 21, 2022 at 11:00:04 by Anonymous?. See the history of this page for a list of all contributions to it.