:: deftheorem defines are_isomorphic FUNCTOR0:def 39 :
for A, B being non empty transitive with_units AltCatStr holds
( A,B are_isomorphic iff ex F being Functor of A,B st
( F is bijective & F is covariant ) );