:: deftheorem Def21 defines pullback CAT_7:def 21 :
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
for b₆ being triple object holds
( b₆ is pullback of F1,F2 iff ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st
( b₆ = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 ) );