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) |
= | (Yanking) | |
= | (Naturality of Tr) | |
= | (Naturality of symm) | |
= | (Functoriality of ) | |
= | (Symmetry sliding) | |
= | (Naturality of symm) | |
= | (Naturality of Tr) | |
= | (Yanking) |