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

Showing changes from revision #4 to #5: Added | Removed | Changed

Contents

Idea

An essentially conjunctive algebraic dagger 2-poset is a dagger 2-poset whose internal logic of thecategory of maps is consists a only syntactic of category conjunction foressentially algebraic theories?\wedge . “Cartesian” is a very overloaded term and has true a different meaning for bicategories, and “finitely complete” dagger 2-posets understood in category-theoretic terms are simplysemiadditive dagger 2-posets\top . , or equivalently, whosecategory of maps has all pullback?s of monic maps.

Definition

An essentially conjunctive algebraic 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 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 \cap E:Ob(C) 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}.

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 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}.

  • The unitary isomorphism classes of functional dagger monomorphisms into every object AA is a meet-semilattice. Since every functional dagger monomorphism is a map, the category of maps is a finitely complete category?.

Examples

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

See also

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