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

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

## 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 monic map dagger monomorphisms$i_{B,A}:Hom(B,A)$ , i_{B,A}:Hom(B,A) i_{E,A}:Hom(E,A) , there is an object i_{E,A}:Hom(E,A) B \cap E:Ob(C) , there with is monic an maps object B i_{B \cap E:Ob(C) E,A}:Hom(B \cap E,A) , with functional dagger monomorphisms i_{B \cap E,A}:Hom(B E,B}:Hom(B \cap E,A) E,B),  i_{B \cap E,B}:Hom(B E,E}:Hom(B \cap E,B) E,E) , such that i_{B,A} \circ i_{B \cap E,E}:Hom(B E,B} = i_{B \cap E,E) E,A} , such and that i_{B,A} i_{E,A} \circ i_{B \cap E,B} E,E} = i_{B \cap E,A} , and for every object i_{E,A} D:Ob(C) \circ i_{B \cap E,E} = i_{B \cap E,A} , and with for monic every maps object D:Ob(C) i_{D,A}:Hom(D,A) with functional dagger monomorphisms i_{D,A}:Hom(D,A) i_{D,B}:Hom(D,B) , i_{D,B}:Hom(D,B) i_{D,E}:Hom(D,E) , such that i_{D,E}:Hom(D,E) i_{B,A} \circ i_{D,B} = i_{D,A} such and that i_{B,A} i_{E,A} \circ i_{D,B} i_{D,E} = i_{D,A} , and there is a monic map i_{E,A} i_{D,B \circ \cap i_{D,E} E}:Hom(D,B = \cap i_{D,A} E) , there such is that a functional dagger monomorphism i_{B \cap E,A} \circ i_{D,B \cap E}:Hom(D,B E} \cap = E) i_{D,A} 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 monic dagger map, monomorphism, and for each object$B:Ob(C)$ with a functional monic dagger map monomorphism$i_{B,A}:Hom(B,A)$, $1_A \circ i_{B,A} = i_{B,A}$.

• The unitary isomorphism classes of functional monic dagger maps 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

Revision on April 25, 2022 at 14:40:18 by Anonymous?. See the history of this page for a list of all contributions to it.