[[!redirects braided monoidal dagger categories]] #Contents# * table of contents {:toc} ## Definition ## A **braided monoidal dagger category** is a [[monoidal dagger category]] $C$ with * a natural unitary isomorphism type family $$\beta: (-)\otimes(-) \cong^\dagger (-)\otimes(-)$$ called the **braiding**, with dependent terms $$\beta_{A,B}: A\otimes B \cong^\dagger B\otimes A$$ for $A:C$ and $B:C$. * a type family $$\eta^1: \alpha_{(-),(-),(-)} \circ \beta_{(-), (-) \otimes (-)} \circ \alpha_{(-),(-),(-)} = (id \otimes \beta_{(-), (-)}) \circ \alpha_{(-),(-),(-)} \circ (\beta_{(-), (-)} \otimes id)$$ called the **first hexagon identity**, with dependent terms $$\eta^1_{D, E, F}: \alpha_{E,F,D} \circ \beta_{D, E \otimes F} \circ \alpha_{D,E,F} = (id \otimes \beta_{D,F}) \circ \alpha_{E,D,F} \circ (\beta_{D, E} \otimes id)$$ for $D:C$, $E:C$, and $F:C$. * a type family $$\eta^2: \alpha^{-1}_{(-),(-),(-)} \circ \beta_{(-) \otimes (-), (-)} \circ \alpha^{-1}_{(-),(-),(-)} = (\beta_{(-), (-)} \otimes id) \circ \alpha^{-1}_{(-),(-),(-)} \circ (id \otimes \beta_{(-), (-)})$$ called the **second hexagon identity**, with dependent terms $$\eta^2_{D,E,F}: \alpha_{F,D,E}^{-1} \circ \beta_{D \otimes E, F} \circ \alpha^{-1}_{D,E,F} = (\beta_{D, F} \otimes id) \circ \alpha^{-1}_{D,F,E} \circ (id \otimes \beta_{E, F})$$ for $D:C$, $E:C$, and $F:C$. ## Examples ## * [[symmetric monoidal dagger category]] * [[compact closed dagger category]] ## See also ## * [[Category theory]] * [[dagger category]]