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

Showing changes from revision #1 to #2: Added | Removed | Changed

Contents

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