# 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$.