for C, C1, C2 being category
for F1 being Functor of C1,C
for F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds
ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st
( the carrier of D = { [f1,f2] where f1 is morphism of C1, f2 is morphism of C2 : ( f1 in the carrier of C1 & f2 in the carrier of C2 & F1 . f1 = F2 . f2 ) } & the composition of D = { [[f1,f2],f3] where f1, f2, f3 is morphism of D : ( f1 in the carrier of D & f2 in the carrier of D & f3 in the carrier of D & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st f1 = [f11,f21] & f2 = [f12,f22] & f3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) } & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 )