In , 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 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).
Every 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.
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.