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

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 $C$ such that

• For each object $A:Ob(C)$, $B:Ob(C)$, $E:Ob(C)$ with functional dagger monomorphisms $i_{B,A}:Hom(B,A)$, $i_{E,A}:Hom(E,A)$, there is an object $B \cap E:Ob(C)$ with functional dagger monomorphisms $i_{B \cap E,A}:Hom(B \cap E,A)$, $i_{B \cap E,B}:Hom(B \cap E,B)$, $i_{B \cap E,E}:Hom(B \cap E,E)$, such that $i_{B,A} \circ i_{B \cap E,B} = i_{B \cap E,A}$ and $i_{E,A} \circ i_{B \cap E,E} = i_{B \cap E,A}$, and for every object $D:Ob(C)$ with functional dagger monomorphisms $i_{D,A}:Hom(D,A)$ $i_{D,B}:Hom(D,B)$, $i_{D,E}:Hom(D,E)$ such that $i_{B,A} \circ i_{D,B} = i_{D,A}$ and $i_{E,A} \circ i_{D,E} = i_{D,A}$, there is a functional dagger monomorphism $i_{D,B \cap E}:Hom(D,B \cap E)$ such that $i_{B \cap E,A} \circ i_{D,B \cap E} = i_{D,A}$.

Properties

• For each object $A:Ob(C)$, the identity function $1_A:Hom(A,A)$ is a functional dagger monomorphism, and for each object $B:Ob(C)$ with a functional dagger monomorphism $i_{B,A}:Hom(B,A)$, $1_A \circ i_{B,A} = i_{B,A}$.

• The unitary isomorphism classes of functional dagger monomorphisms into every object $A$ is a meet-semilattice.

Examples

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

See also

• dagger 2-poset
• conjunctive dagger 2-poset
• coherent dagger 2-poset
• Heyting dagger 2-poset
• Boolean dagger 2-poset
• elementarily topical dagger 2-poset