Add some comments

Author: Taneb

src/Categories/Category/Monoidal/Traced.agda

@@ -23,7 +23,7 @@ private
 -- Def from Traced monoidal categories (Joyal, Street, & Verity, 1996)
 --
 -- A symmetric monoidal category (C,⊗,1,b) (where b is the symmetry) is
--- said to be traced if it is equipped with a natural family of functions
+-- said to be traced if it is equipped with a natural family* of functions
 --
 -- TrXA,B:C(A⊗X,B⊗X)→C(A,B)
 -- satisfying three axioms:
@@ -34,6 +34,8 @@ private
 -- Superposing: TrXC⊗A,C⊗B(idC⊗f)=idC⊗TrXA,B(f) (for all f:A⊗X→B⊗X)
 --
 -- Yanking: TrXX,X(bX,X)=idX
+--
+-- (*) this means the family needs to be "natural" in A, B, and X!
 
 -- Traced monoidal category
 --  is a symmetric monoidal category with a trace operation
@@ -50,7 +52,9 @@ record Traced : Set (levelOfTerm M) where
     trace : ∀ {X A B} → A ⊗₀ X ⇒ B ⊗₀ X → A ⇒ B
     trace-resp-≈ : f ≈ g → trace f ≈ trace g
 
+    -- dinaturality in X
     slide : trace (f ∘ id ⊗₁ g) ≈ trace (id ⊗₁ g ∘ f)
+    -- naturality in A and B
     tightenₗ : trace (f ⊗₁ id ∘ g) ≈ f ∘ trace g
     tightenᵣ : trace (f ∘ g ⊗₁ id) ≈ trace f ∘ g