:: deftheorem defines |^ CAT_8:def 36 :
for C1, C2 being category holds C2 |^ C1 = the categorical_exponent of C1,C2 `1 ;