:: deftheorem defines is_equivalent_with ISOCAT_1:def 10 :
for A, B being Category holds
( A is_equivalent_with B iff ex F being Functor of A,B ex G being Functor of B,A st
( G * F ~= id A & F * G ~= id B ) );