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{Tr}^U_{X,Y}:\mathbf{C}(X\otimes U,Y\otimes U)\to\mathbf{C}(X,Y)

called a trace, satisfying the following conditions:

\mathrm{Tr}^U_{X,Y}(f)g=\mathrm{Tr}^U_{X',Y}(f(g\otimes U))
Naturality in X
g\mathrm{Tr}^U_{X,Y}(f)=\mathrm{Tr}^U_{X,Y'}((g\otimes U)f)
Naturality in Y
\mathrm{Tr}^U_{X,Y}((Y\otimes g)f)=\mathrm{Tr}^{U'}_{X,Y}(f(X\otimes g))
Dinaturality in U
\mathrm{Tr}^I_{X,Y}(f)=f
Vanishing I
\mathrm{Tr}^{U\otimes V}_{X,Y}(f)=\mathrm{Tr}^U_{X,Y}(\mathrm{Tr}^V_{X\otimes U,Y\otimes U}(f))
Vanishing II
g\otimes \mathrm{Tr}^U_{X,Y}(f)=\mathrm{Tr}^U_{W\otimes X,Z\otimes Y}(g\otimes f)
Superposing
\mathrm{Tr}^X_{X,X}(\gamma_{X,X})=X

(where \gamma is the symmetry of the monoidal category).

Yanking

Properties

References