# Contents

## Definition

A monoidal dagger category is a dagger category $C$ with

• a functor $(-)\otimes(-): (C \times C) \to C$ from the product dagger category of $C$ to $C$ itself called the tensor product.

• an object $\Iota: Ob(C)$ called the tensor unit.

• a natural unitary isomorphism type family

$\alpha: ((-)\otimes(-))\otimes(-) \cong^\dagger (-)\otimes((-)\otimes(-))$

called the associator, with dependent terms

$\alpha_{A_1, A_2, A_3}: (A_1\otimes A_2)\otimes A_3 \cong^\dagger A_1\otimes(A_2\otimes A_3)$
• a natural unitary isomorphism type family
$\lambda: \Iota\otimes(-) \cong^\dagger (-)$

called the left unitor, with dependent terms

$\lambda_{A}: \Iota\otimes A \equiv^\dagger A$
• a natural unitary isomorphism type family
$\rho: (-)\otimes\Iota \cong^\dagger (-)$

called the right unitor, with dependent terms

$\rho_{A}: A\otimes\Iota \equiv^\dagger A$
• a type family
$\tau: \rho_{(-)} \otimes \Iota_{(-)} = (\Iota_{(-)} \otimes \rho_{(-)}) \circ \alpha_{{(-)}, \Iota, {(-)}}$

called the triangle identity, with dependent terms

$\tau_{A, B}: \rho_A \otimes \Iota_B = (1_A \otimes \rho_B) \circ \alpha_{A, \Iota, B}$
• a type family
$\pi: \alpha_{(-), (-), (-) \otimes (-)} \circ \alpha_{(-) \otimes (-), (-), (-)} = (id_{(-)} \otimes \alpha_{(-), (-), (-)}) \circ \alpha_{(-), (-) \otimes (-), (-)} \circ (\alpha_{(-), (-), (-)} \otimes id_{(-)})$

called the pentagon identity, with dependent terms

$\pi_{D,E,F,G}: \alpha_{D, E, F \otimes G} \circ \alpha_{D \otimes E, F, G} = (id_D \otimes \alpha_{E, F, G}) \circ \alpha_{D, E \otimes F, G} \circ (\alpha_{D, E, F} \otimes id_G)$