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 X: for every and ,
- naturality in Y: for every and ,
- dinaturality in U: for every and
- vanishing I: for every ,
- vanishing II: for every
- superposing: for every and ,
is the symmetry of the monoidal category).
- 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.