for C being Category
for c being Object of C holds (c opp) opp = c ;