:: deftheorem defines eval CAT_8:def 33 :
for C being non empty with_binary_products with_exponential_objects category
for a, b being Object of C holds eval (a,b) = the categorical_exponent of a,b `2 ;