for C, D being composable with_identities CategoryStr holds
( C ~= D iff ex F being Functor of C,D st
( F is covariant & F is bijective ) )