Homotopy Type Theory conjunctive dagger 2-poset > history (Rev #8, changes)

Showing changes from revision #7 to #8: Added | Removed | Changed

Contents

Idea

An conjunctive dagger 2-poset is a dagger 2-poset whose internal logic of the category of maps consists only of conjunction \wedge and true \top, or equivalently, whose category of maps has all pullback?s of monic maps.

Definition

An conjunctive dagger 2-poset is a dagger 2-poset CC such that

  • For each object A:Ob(C)A:Ob(C), B:Ob(C)B:Ob(C), E:Ob(C)E:Ob(C) with monic map 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}.

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 isomorphism classes of monic maps into every object AA is a meet-semilattice.

Examples

The dagger 2-poset of sets and relations is a conjunctive dagger 2-poset.

See also

Revision on June 7, 2022 at 02:42:41 by Anonymous?. See the history of this page for a list of all contributions to it.