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

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

Contents

Definition

A symmetric monoidal dagger category is a braided monoidal dagger category CC with a type family

σ:β (),()β (),()=Ι (),()\sigma: \beta_{(-),(-)} \circ \beta_{(-), (-)} = \Iota_{(-),(-)}

with dependent terms

σ A,B:β A,Bβ B,A=Ι A,B\sigma_{A,B}: \beta_{A,B} \circ \beta_{B, A} = \Iota_{A,B}

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

Examples

See also

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