for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t )