:: deftheorem defines rho CAT_4:def 13 :
for C being Cartesian_category
for a being Object of C holds rho a = pr1 (a,([1] C));