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

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

~~
~~# Contents

~~
~~~~
~~## Definition

~~
~~A **symmetric monoidal dagger category** is a braided monoidal dagger category $C$ with a type family

~~
~~$\sigma: \beta_{(-),(-)} \circ \beta_{(-), (-)} = \Iota_{(-),(-)}$

~~
~~with dependent terms

~~
~~$\sigma_{A,B}: \beta_{A,B} \circ \beta_{B, A} = \Iota_{A,B}$

~~
~~for $A:C$ and $B: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.