for A, B being category
for F being covariant Functor of A,B st F is bijective holds
A,B are_isomorphic_under F