Homotopy Type Theory symmetric monoidal dagger category > history (Rev #1)

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 February 14, 2022 at 10:20:08 by Anonymous?. See the history of this page for a list of all contributions to it.