Proof of trace respecting double symmetry

Proposition (Trace respects double symmetry) (for f : V W and g : X U A Y U A in C):

=
TrX Y A (g) f = Tr(X V) (Y W) A ((idX symmV U(A)); (g f); (idY symmU(A) W))

Proof.

= (Acyclic graph iso)
= (Strength of Tr)
= (Naturality of Tr)
= (Acyclic graph iso)

Back