Traced monoidal category

In category theory, a traced monoidal category is a category with some extra structure which gives a reasonable notion of feedback.

A traced symmetric monoidal category is a symmetric monoidal category C together with a family of functions
:$\mathrm^U_:\mathbf(X\otimes U,Y\otimes U)\to\mathbf(X,Y)$
called a ''trace'', satisfying the following conditions:

* naturality in $X$: for every $f:X\otimes U\to Y\otimes U$ and $g:X'\to X$,
::$\mathrm^U_(f \circ (g\otimes \mathrm_U)) = \mathrm^U_(f) \circ g$

* naturality in $Y$: for every $f:X\otimes U\to Y\otimes U$ and $g:Y\to Y'$,
::$\mathrm^U_((g\otimes \mathrm_U) \circ f) = g \circ \mathrm^U_(f)$

* dinaturality in $U$: for every $f:X\otimes U\to Y\otimes U'$ and $g:U'\to U$
::$\mathrm^U_((\mathrm_Y\otimes g) \circ f)=\mathrm^_(f \circ (\mathrm_X\otimes g))$

* vanishing I: for every $f:X \otimes I \to Y \otimes I$, (with $\rho_X \colon X\otimes I\cong X$ being the right unitor),
::$\mathrm^I_(f)=\rho_Y \circ f \circ \rho_X^$

* vanishing II: for every $f:X\otimes U\otimes V\to Y\otimes U\otimes V$
::$\mathrm^U_(\mathrm^V_(f)) = \mathrm^_(f)$

* superposing: for every $f:X\otimes U\to Y\otimes U$ and $g:W\to Z$,
::$g\otimes \mathrm^U_(f)=\mathrm^U_(g\otimes f)$

* yanking:
::$\mathrm^X_(\gamma_)=\mathrm_X$
(where $\gamma$ is the symmetry of the monoidal category).

Properties

* Every compact closed category admits a trace.
* Given a traced monoidal category C, the ''Int construction'' generates the free (in some bicategorical sense) compact closure Int(C) of C.

References

*

Monoidal categories

{{categorytheory-stub