# Proof of parameterized dinaturality

Proposition (Parameterized dinaturality) (for f : Z U(B) U(A) and g : X U(A) Y U(B) in C):

| = |
Tr(X Z) Y A ((idX symmZ U(A)); (g idZ); (idY (symmU(B) Z); f))) | = | Tr(X Z) Y B ((idX f); g)

Proof.

= |  | (Yanking)
= |  | (Naturality of Tr)
= |  | (Naturality of symm)
= |  | (Functoriality of )
= |  | (Symmetry sliding)
= |  | (Naturality of symm)
= |  | (Naturality of Tr)
= |  | (Yanking)

Back