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

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

# Contents

## Definition

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

• a morphism $i_A: hom(A,A + B)$ for $A:C$ and $B:C$.
• a morphism $i_B: hom(B,A + B)$ for $A:C$ and $B:C$.
• a morphism $d_{A + B}: hom(A + 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 + B} \circ 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 + B} \circ i_B = d_B$ for an object $D:C$ and morphisms $d_A: hom(A,D)$ and $d_B: hom(B,D)$
• a morphism $0_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.