Contents

Definition

A compact closed dagger category is a symmetric monoidal dagger category $C$ with

• an object $A^*$ called the dual for every object $A:Ob(C)$

• for every object $A:Ob(C)$, a morphism $\iota^R_A: \Iota \to A \otimes A^*$ called the right unit

• for every object $A:Ob(C)$, a morphism $\iota^L_A: \Iota \to A^* \otimes A$ called the left unit

• for every object $A:Ob(C)$, a morphism $\eta^L_A: A \otimes A^* \to \Iota$ called the left counit

• for every object $A:Ob(C)$, a morphism $\eta^R_A: A^* \otimes A \to \Iota$ called the right counit

• a type family $r: {\iota^R_{(-)}}^\dagger = \eta^L_{(-)}$ with dependent terms $r_A: {\iota^R_A}^\dagger = \eta^L_A$ for $A:C$

• a type family $l: {\iota^L_{(-)}}^\dagger = \eta^R_{(-)}$ with dependent terms $l_A: {\iota^L_A}^\dagger = \eta^R_A$ for $A:C$

• a type family $\tau^1:\iota^L_{(-)}(-) \circ (-)\eta^L_{(-)}$ with dependent terms $\tau^1_A:\iota^L_{A}A \circ A\eta^L_{A}$ for $A:C$

• a type family $\tau^2:\iota^R_{(-)^*}(-)^* \circ (-)^*\eta^R_{(-)^*}$ with dependent terms $\tau^2_A:\iota^R_{A^*}A^* \circ A\eta^R_{A^*}$ for $A:C$

• a type family $\tau^3:(-)\iota^R_{(-)} \circ \eta^R_{(-)}(-)$ with dependent terms $\tau^3_A:A\iota^R_{A} \circ \eta^R_{A}A$ for $A:C$

• a type family $\tau^4:(-)^*\iota^R_{(-)^*} \circ \eta^R_{(-)^*}(-)^*$ with dependent terms $\tau^4_A:A^*\iota^R_{A^*} \circ \eta^R_{A^*}A^*$ for $A:C$

Examples

(…)

See also

• Category theory
• dagger category