Homotopy Type Theory cocartesian monoidal dagger category > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

Definition

A cocartesian monoidal dagger category is a monoidal dagger category $(C, +, 0)$ C (C, +, 0) with

a morphism $i_{A} : hom (A, A \otimes + B)$ i_A: hom(A,A ~~\otimes~~ + B) for $A:C$ and $B:C$ .
a morphism $i_{B} : hom (B, A \otimes + B)$ i_B: hom(B,A ~~\otimes~~ + B) for $A:C$ and $B:C$ .
a morphism $d_{A \otimes + B} : hom (A \otimes + B, D)$ d_{A ~~\otimes~~ + B}: hom(A ~~\otimes~~ + B,D) for an object $D:C$ and morphisms $d_A: hom(A,D)$ and $d_B: hom(B,D)$
an identity $u_{A} : d_{A \otimes + B} \circ {p i}_{A} = d_{A}$ u_A: d_{A ~~\otimes~~ + B} \circ ~~p_A~~ i_A = d_A for an object $D:C$ and morphisms $d_A: hom(A,D)$ and $d_B: hom(B,D)$
an identity $u_{B} : d_{A \otimes + B} \circ {p i}_{B} = d_{B}$ u_B: d_{A ~~\otimes~~ + B} \circ ~~p_B~~ i_B = d_B for an object $D:C$ and morphisms $d_A: hom(A,D)$ and $d_B: hom(B,D)$
a morphism $a 0_{a} : hom (Ι 0, A)$ a: 0_a: ~~hom(\Iota,A)~~ hom(0,A) for every object $A:C$

an identity

u_0: f \circ 0_A = 0_B

for for

A:C

and

B:C

and

f:hom(A,B)

In a cocartesian monoidal dagger category, the tensor product is called a coproduct and the tensor unit is called an initial object.