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

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