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
called a trace, satisfying the following conditions:
naturality in : for every and ,
naturality in : for every and ,
dinaturality in : for every and
vanishing I: for every , (with being the right unitor),
vanishing II: for every
superposing: for every and ,
yanking:
(where 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.