for C1, C2 being composable with_identities CategoryStr st C1 ~= C2 holds
RelOb C1, RelOb C2 are_isomorphic