[[!redirects compact closed dagger categories]] #Contents# * table of contents {:toc} ## 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]]