title: Traced monoidal category
text: # 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} _{X,Y}^{U}:\mathbf {C} (X\otimes U,Y\otimes U)\to \mathbf {C} (X,Y)$
  
  called a trace, satisfying the following conditions:
  
         $\mathrm {Tr} _{X',Y}^{U}(f\circ (g\otimes \mathrm {id} _{U}))=\mathrm {Tr} _{X,Y}^{U}(f)\circ g$
         $\mathrm {Tr} _{X,Y'}^{U}((g\otimes \mathrm {id} _{U})\circ f)=g\circ \mathrm {Tr} _{X,Y}^{U}(f)$
         $\mathrm {Tr} _{X,Y}^{U}((\mathrm {id} _{Y}\otimes g)\circ f)=\mathrm {Tr} _{X,Y}^{U'}(f\circ (\mathrm {id} _{X}\otimes g))$
         $\mathrm {Tr} _{X,Y}^{I}(f)=\rho _{Y}\circ f\circ \rho _{X}^{-1}$
         $\mathrm {Tr} _{X,Y}^{U}(\mathrm {Tr} _{X\otimes U,Y\otimes U}^{V}(f))=\mathrm {Tr} _{X,Y}^{U\otimes V}(f)$
         $g\otimes \mathrm {Tr} _{X,Y}^{U}(f)=\mathrm {Tr} _{W\otimes X,Z\otimes Y}^{U}(g\otimes f)$
         $\mathrm {Tr} _{X,X}^{X}(\gamma _{X,X})=\mathrm {id} _{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.
  