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 CC with

  • a natural unitary isomorphism type family
β:()() ()()\beta: (-)\otimes(-) \cong^\dagger (-)\otimes(-)

called the braiding, with dependent terms

β A,B:AB BA\beta_{A,B}: A\otimes B \cong^\dagger B\otimes A

for A:CA:C and B:CB:C.

  • a type family
η 1:α (),(),()β (),()()α (),(),()=(idβ (),())α (),(),()(β (),()id)\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

η D,E,F 1:α E,F,Dβ D,EFα D,E,F=(idβ D,F)α E,D,F(β D,Eid)\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:CD:C, E:CE:C, and F:CF:C.

  • a type family
η 2:α (),(),() 1β ()(),()α (),(),() 1=(β (),()id)α (),(),() 1(idβ (),())\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

η D,E,F 2:α F,D,E 1β DE,Fα D,E,F 1=(β D,Fid)α D,F,E 1(idβ E,F)\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:CD:C, E:CE:C, and F:CF:C.

Examples

See also

Revision on June 7, 2022 at 11:26:54 by Anonymous?. See the history of this page for a list of all contributions to it.