:: deftheorem Def4 defines are_naturally_equivalent FUNCTOR3:def 4 :
for A, B being category
for F1, F2 being covariant Functor of A,B holds
( F1,F2 are_naturally_equivalent iff ( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ex t being natural_transformation of F1,F2 st
for a being Object of A holds t ! a is iso ) );