Homotopy Type Theory semiadditive dagger category > history (Rev #4, changes)

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

Contents

Definition

A semiadditive dagger category is a cocartesian monoidal dagger category $(C, \oplus, 0, i_A, i_B, 0_A)$ with

• an identity $m_A: i_A^\dagger \circ i_A = id_A$ for $A:C$
• an identity $m_B: i_B^\dagger \circ i_B = id_B$ for $B:C$
• an identity $p: i_b^\dagger \circ i_A = 0_B \circ 0_A^\dagger$ for $A:C$ and $B:C$.

In a semiadditive dagger category, the coproduct is called a biproduct and the initial object is called a zero object.

(…)