Homotopy Type Theory braided monoidal dagger category > history (Rev #1, changes)

Showing changes from revision #0 to #1: Added | ~~Removed~~ | ~~Chan~~ged

Definition

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

\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$ .

\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$ .

\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$ .