traced monoidal category



Monoidal categories

monoidal categories

With symmetry

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products



Internal monoids



In higher category theory



The concept of traced monoidal category axiomatizes the structure on a monoidal category for it to have a sensible notion of trace the way it exists canonically in compact closed categories.


The original definition due to (Joyal-Street-Verity 96) is stated in the general setting of balanced monoidal categories. Here we give just the slightly simpler formulation for the case of symmetric monoidal categories (Hasegawa 1997).

A symmetric monoidal category (C,,1,b)(C,\otimes,1,b) (where bb is the symmetry) is said to be traced if it is equipped with a natural family of functions

Tr A,B X:C(AX,BX)C(A,B)Tr_{A,B}^X : C(A \otimes X, B\otimes X) \to C(A,B)

satisfying three axioms:

  • Vanishing: Tr A,B 1(f)=fTr_{A,B}^1(f) = f (for all f:ABf : A \to B) and Tr A,B XY(f)=Tr A,B X(Tr AX,BX Y(f))Tr_{A,B}^{X\otimes Y}(f) = Tr_{A,B}^X(Tr_{A\otimes X,B\otimes X}^Y(f)) (for all f:AXYBXYf : A \otimes X \otimes Y \to B \otimes X \otimes Y)

  • Superposing: Tr CA,CB X(id Cf)=id CTr A,B X(f)Tr_{C\otimes A,C\otimes B}^X(id_C \otimes f) = id_C \otimes Tr_{A,B}^X(f) (for all f:AXBXf : A \otimes X \to B \otimes X)

  • Yanking: Tr X,X X(b X,X)=id XTr_{X,X}^X(b_{X,X}) = id_X

In string diagrams, the trace Tr(f):ABTr(f) : A \to B of a morphism f:AXBXf : A \otimes X \to B \otimes X is visualized by wrapping the outgoing wire representing XX to the incoming wire representing XX, thus “tying a loop” in the diagram of ff. The three axioms above (as well as the naturality conditions) then all have natural graphical interpretations (see Joyal-Street-Verity 96 or Hasegawa 1997).


Relation to compact closed categories

Every compact closed category is equipped with a canonical trace defined by

Tr A,B X(f)=AidηAXX *fidBXX *idεB Tr_{A,B}^X(f) = A \overset{id\otimes \eta}{\to} A \otimes X \otimes X^* \overset{f \otimes id}{\to} B \otimes X \otimes X^* \overset{id \otimes \varepsilon'}{\to} B

where η\eta is a unit and ε\varepsilon' is a counit of appropriate adjunctions (note that the symmetry makes the dual X *X^* both a right and left adjoint of XX: the adjunctions are ambidextrous).

Conversely, given a traced monoidal category 𝒞\mathcal{C}, there is a free construction completion of it to a compact closed category Int(𝒞)Int(\mathcal{C}) (Joyal-Street-Verity 96):

the objects of Int(𝒞)Int(\mathcal{C}) are pairs (A +,A )(A^+, A^-) of objects of 𝒞\mathcal{C}, a morphism (A +,A )(B +,B )(A^+ , A^-) \to (B^+ , B^-) in Int(𝒞)Int(\mathcal{C}) is given by a morphism of the form A +B A B +A^+\otimes B^- \longrightarrow A^- \otimes B^+ in 𝒞\mathcal{C}, and composition of two such morphisms (A +,A )(B +,B )(A^+ , A^-) \to (B^+ , B^-) and (B +,B )(C +,C )(B^+ , B^-) \to (C^+ , C^-) is given by tracing out B B^- from the composite

A +B C f1A B +C 1gA B C +. A^+ \otimes B^- \otimes C^- \xrightarrow{f\otimes 1} A^- \otimes B^+ \otimes C^- \xrightarrow{1\otimes g} A^- \otimes B^- \otimes C^+.

Note that 𝒞\mathcal{C} embeds fully-faithfully in Int(𝒞)Int(\mathcal{C}) by sending AA to (A,I)(A,I), where II is the unit object of the monoidal structure.

Furthermore, a traced monoidal category that is *\ast-autonomous must already be compact closed; see HH13.

In cartesian monoidal categories

For a cartesian monoidal category, the existence of a trace operator is equivalent to the existence of a “parameterized” fixed point operator satisfying certain properties (Hasegawa 1997).

Adding traces

Since any full monoidal subcategory of a traced monoidal category inherits a trace, not every monoidal category can be fully embedded into a traced monoidal category, and hence also not into a compact closed category. In fact, Plotkin observed that there are monoidal categories that cannot even be faithfully mapped into a traced monoidal category. This can be seen from the fact that a traced monoidal category has the “cancellation property” that if fid XX=gid XXf\otimes id_{X\otimes X} = g \otimes id_{X\otimes X} then fid X=gid Xf\otimes id_X = g\otimes \id_X (since the latter is a trace of the former with one of the copies of XXX\otimes X transposed), but not all monoidal categories have this property.

Categorical semantics

Traced monoidal categories serve as an “operational” categorical semantics for linear logic, known as Geometry of Interactions. See there for more.

In this context the free compact closure Int(𝒞)Int(\mathcal{C}) from above is sometimes called the Geometry of Interaction construction and denoted 𝒢(𝒞)\mathcal{G}(\mathcal{C}) (Abramsky-Haghverdi-Scott 02, def. 2.6).


The concept was introduced in

A characterization of trace structures on cartesian monoidal categories is given in

  • Masahito Hasegawa, Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculi, Proc. 3rd International Conference on Typed Lambda Calculi and Applications (TLCA 1997). Springer LNCS1210, 1997 (citeseer)

The equivalence between traces and parameterized fixed point operators appears as Theorem 3.1 (the author notes that this theorem was also proved independently by Martin Hyland).

Comprehensive discussion as a source for categorical semantics of the Geometry of Interactions is in

The combination with star-autonomous structure was discussed in

  • Tamás Hajgató and Masahito Hasegawa, Traced *\ast-autonomous categories are compact closed, TAC, 2013

Last revised on November 28, 2019 at 13:31:56. See the history of this page for a list of all contributions to it.