for C being CategoryStr
for f being morphism of C st C is with_identities holds
( f is left_identity iff f is right_identity )