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

Contents

Idea

A Heyting dagger 2-poset is a dagger 2-poset whose category of maps is a Heyting category.

Definition

A Heyting 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).

  • 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 object D:Ob(C)D:Ob(C) with functional dagger monomorphisms 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), there is a functional dagger monomorphism i BE,D:Hom(BE,D)i_{B \cup E,D}:Hom(B \cup E,D).

  • 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), there is trivially the same functional dagger monomorphism i B,A:Hom(B,A)i_{B,A}:Hom(B,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 \cap E:Ob(C) with functional dagger monomorphisms i A,BE:Hom(A,BE)i_{A,B \cap E}:Hom(A,B \cap E), 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 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).

  • For each object A:Ob(C)A:Ob(C), B:Ob(C)B:Ob(C), D:Ob(C)D: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), there is an object BD:Ob(C)B \Rightarrow D:Ob(C) with functional dagger monomorphism i D,A:Hom(D,A)i_{D,A}:Hom(D,A),

    i (BD)D,B:Hom((BD)D,B)i_{(B \Rightarrow D) \cap D, B}:Hom((B \Rightarrow D) \cap D, B)

    and

    i D,B(DB):Hom(D,B(DB))i_{D, B \Rightarrow (D \cap B)}:Hom(D, B \Rightarrow (D \cap B))

Properties

  • The unitary isomorphism classes of functional dagger monomorphisms into every object AA is a Heyting algebra. Since every functional dagger monomorphism is a map, the category of maps is a Heyting category?. As a result, Heyting dagger 2-posets are the same as division allegories and bicategories of relations.

Examples

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

See also

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