:: deftheorem defines is_naturally_transformable_to FUNCTOR2:def 6 :
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B holds
( F1 is_naturally_transformable_to F2 iff ( F1 is_transformable_to F2 & ex t being transformation of F1,F2 st
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F1 . f) = (F2 . f) * (t ! a) ) );