:: deftheorem defines are_naturally_equivalent NATTRA_1:def 11 :
for A, B being Category
for F1, F2 being Functor of A,B holds
( F1,F2 are_naturally_equivalent iff ( F1 is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2 st t is invertible ) );