:: deftheorem Def20 defines is_pullback_of CAT_7:def 20 :
for C, C1, C2, D 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 P1 being Functor of D,C1 st P1 is covariant holds
for P2 being Functor of D,C2 st P2 is covariant holds
( D,P1,P2 is_pullback_of F1,F2 iff ( F1 (*) P1 = F2 (*) P2 & ( for D1 being category
for G1 being Functor of D1,C1
for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D1,D st
( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds
H = H1 ) ) ) ) );