theorem Th51:
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 )