:: deftheorem defines are_equivalent YELLOW18:def 2 :
for A, B being category holds
( A,B are_equivalent iff ex F being covariant Functor of A,B ex G being covariant Functor of B,A st
( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent ) );