theorem :: NATTRA_1:47

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