Proposition (Trace respects tensor) (for f : U(B) U(C) U(A) and g : X U(A) Y U(B) U(C) in C):
= | ||
TrX Y A (g; idY f) | = | TrX Y C (TrX Y B ((idX f); g)) |
= | (Yanking) | |
= | (Naturality of Tr) | |
= | (Acyclic graph iso) | |
= | (Symmetry sliding) | |
= | (Parameterized dinaturality) | |
= | (Symmetry sliding) |