for C being Category
for a being Object of (C opp) holds opp (id a) = id (opp a)