:: deftheorem Def13 defines natural_equivalence NATTRA_1:def 14 :
for A, B being Category
for F1, F2 being Functor of A,B st F1,F2 are_naturally_equivalent holds
for b₅ being natural_transformation of F1,F2 holds
( b₅ is natural_equivalence of F1,F2 iff b₅ is invertible );