# Homotopy Type Theory coherent dagger 2-poset > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

## Idea

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

## Definition

A coherent dagger 2-poset is a dagger 2-poset $C$ such that

• There is an object $0:Ob(C)$ such that for each object $A:Ob(C)$, there is a functional dagger monomorphism $i_{0,A}:Hom(0,A)$ such that for each object $B:Ob(C)$ with a functional dagger monomorphism $i_{B,A}:Hom(B,A)$, there is a functional dagger monomorphism $i_{0,B}:Hom(0,B)$ such that $i_{B,A} \circ i_{0,B} = i_{0,A}$.

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

• For each object $A:Ob(C)$ , the identity function 1_A:Hom(A,A) B:Ob(C) , is a functional dagger monomorphism, and for each object B:Ob(C) E:Ob(C) with a functional dagger monomorphism monomorphisms$i_{B,A}:Hom(B,A)$ , there is trivially the same functional dagger monomorphism i_{B,A}:Hom(B,A) i_{E,A}:Hom(E,A) , such there that is an object 1_A B \circ \cap i_{B,A} E:Ob(C) = i_{B,A} 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}$.

• For each object $A:Ob(C)$, $B:Ob(C)$,  E:Ob(C) D:Ob(C) , with functional dagger monomorphisms i_{B,A}:Hom(B,A) E:Ob(C) , with functional dagger monomorphisms i_{E,A}:Hom(E,A) i_{B,A}:Hom(B,A) , there is an object B i_{D,A}:Hom(D,A) \cap E:Ob(C) , with functional dagger monomorphisms i_{A,B i_{E,A}:Hom(E,A) \cap E}:Hom(A,B \cap E) , there is a$i_{B \cap E,B}:Hom(B \cap E,B)$unitary isomorphism, $i_{B \cap E,E}:Hom(B \cap E,E)$, such that 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)$, there is a functional dagger monomorphism $i_{D,B \cup E}:Hom(D,B \cup E)$.

$j_{B,C,E}:E \cap (B \cup C) \cong^\dagger (E \cap B) \cup (E \cap C)$
• For each object $A:Ob(C)$, $B:Ob(C)$, $D:Ob(C)$, $E:Ob(C)$ with functional dagger monomorphisms $i_{B,A}:Hom(B,A)$, $i_{D,A}:Hom(D,A)$, $i_{E,A}:Hom(E,A)$, there is a unitary isomorphism

$j_{B,C,E}:E \cap (B \cup C) \cong^\dagger (E \cap B) \cup (E \cap C)$

## Properties

• Theunitary isomorphisms

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

classes of functional dagger monomorphisms into every object$A$ is a distributive lattice. Since every functional dagger monomorphism is a map, the category of maps is a coherent category?.
• The unitary isomorphisms classes of functional dagger monomorphisms into every object $A$ is a distributive lattice. Since every functional dagger monomorphism is a map, the category of maps is a coherent category?.

## Examples

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

## See also

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