for A, B being Category holds IdCat [:A,B:] = [:(IdCat A),(IdCat B):]