for C being Category holds IdMap C = IdMap (C opp) by Lm2;