for C1, C2, C3 being composable with_identities CategoryStr st C1 ~= C2 & C2 ~= C3 holds
C1 ~= C3