:: deftheorem Def23 defines pr1 CAT_7:def 23 :
for C, C1, C2 being category
for F1 being Functor of C1,C st F1 is covariant holds
for F2 being Functor of C2,C st F2 is covariant holds
pr1 (F1,F2) = the pullback of F1,F2 `2_3 ;