[[!redirects monoidal dagger categories]] #Contents# * table of contents {:toc} ## 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 type family $$p: ((-) \otimes (-))^\dagger = (-)^\dagger \otimes (-)^\dagger$$ with dependent terms $$p_{f,g}: (f \otimes g)^\dagger = f^\dagger \otimes g^\dagger$$ for morphisms $f:hom(D,E)$ and $g:hom(F,G)$, * a natural unitary isomorphism type family $$\alpha: ((-)\otimes(-))\otimes(-) \cong^\dagger (-)\otimes((-)\otimes(-))$$ called the **associator**, with dependent terms $$\alpha_{D, E, F}: (D\otimes E)\otimes F \cong^\dagger D\otimes(E\otimes F)$$ for objects $D:C$, $E:C$, $F:C$. * a natural unitary isomorphism type family $$\lambda: \Iota\otimes(-) \cong^\dagger (-)$$ called the **left unitor**, with dependent terms $$\lambda_{A}: \Iota\otimes A \cong^\dagger A$$ for objects $A:C$. * a natural unitary isomorphism type family $$\rho: (-)\otimes\Iota \cong^\dagger (-)$$ called the **right unitor**, with dependent terms $$\rho_{A}: A\otimes\Iota \cong^\dagger A$$ for objects $A:C$. * 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}$$ for objects $A:C$, $B:C$. * 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)$$ for objects $D:C$, $E:C$, $F:C$, $G:C$. ## Examples ## * [[braided monoidal dagger category]] * [[symmetric monoidal dagger category]] * [[cartesian monoidal dagger category]] * [[cocartesian monoidal dagger category]] * [[semiadditive dagger category]] * [[rigid monoidal dagger category]] * [[compact closed dagger category]] ## See also ## * [[Category theory]] * [[dagger category]]