let C, C1, C2 be category; :: thesis: for F1 being Functor of C1,C

for F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds

( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 )

let F1 be Functor of C1,C; :: thesis: for F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds

( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 )

let F2 be Functor of C2,C; :: thesis: ( F1 is covariant & F2 is covariant implies ( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 ) )

assume A1: ( F1 is covariant & F2 is covariant ) ; :: thesis: ( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 )

set T = the pullback of F1,F2;

consider D0 being strict category, P01 being Functor of D0,C1, P02 being Functor of D0,C2 such that

A2: ( the pullback of F1,F2 = [D0,P01,P02] & P01 is covariant & P02 is covariant & D0,P01,P02 is_pullback_of F1,F2 ) by A1, Def21;

A3: ( F1 (*) P01 = F2 (*) P02 & ( 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,D0 st

( H is covariant & P01 (*) H = G1 & P02 (*) H = G2 & ( for H1 being Functor of D1,D0 st H1 is covariant & P01 (*) H1 = G1 & P02 (*) H1 = G2 holds

H = H1 ) ) ) ) by A1, A2, Def20;

A4: ( [D0,P01,P02] `1_3 = D0 & [D0,P01,P02] `2_3 = P01 & [D0,P01,P02] `3_3 = P02 ) ;

then A5: D0 = [|F1,F2|] by A1, A2, Def22;

reconsider P1 = P01 as Functor of [|F1,F2|],C1 by A5;

reconsider P2 = P02 as Functor of [|F1,F2|],C2 by A5;

( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & F1 (*) (pr1 (F1,F2)) = F2 (*) (pr2 (F1,F2)) & ( 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,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) ) ) )

for F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds

( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 )

let F1 be Functor of C1,C; :: thesis: for F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds

( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 )

let F2 be Functor of C2,C; :: thesis: ( F1 is covariant & F2 is covariant implies ( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 ) )

assume A1: ( F1 is covariant & F2 is covariant ) ; :: thesis: ( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 )

set T = the pullback of F1,F2;

consider D0 being strict category, P01 being Functor of D0,C1, P02 being Functor of D0,C2 such that

A2: ( the pullback of F1,F2 = [D0,P01,P02] & P01 is covariant & P02 is covariant & D0,P01,P02 is_pullback_of F1,F2 ) by A1, Def21;

A3: ( F1 (*) P01 = F2 (*) P02 & ( 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,D0 st

( H is covariant & P01 (*) H = G1 & P02 (*) H = G2 & ( for H1 being Functor of D1,D0 st H1 is covariant & P01 (*) H1 = G1 & P02 (*) H1 = G2 holds

H = H1 ) ) ) ) by A1, A2, Def20;

A4: ( [D0,P01,P02] `1_3 = D0 & [D0,P01,P02] `2_3 = P01 & [D0,P01,P02] `3_3 = P02 ) ;

then A5: D0 = [|F1,F2|] by A1, A2, Def22;

reconsider P1 = P01 as Functor of [|F1,F2|],C1 by A5;

reconsider P2 = P02 as Functor of [|F1,F2|],C2 by A5;

( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & F1 (*) (pr1 (F1,F2)) = F2 (*) (pr2 (F1,F2)) & ( 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,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) ) ) )

proof

hence
( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 )
by A1, Def20; :: thesis: verum
thus A6:
pr1 (F1,F2) is covariant
by A2, A5, A4, A1, Def23; :: thesis: ( pr2 (F1,F2) is covariant & F1 (*) (pr1 (F1,F2)) = F2 (*) (pr2 (F1,F2)) & ( 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,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) ) ) )

thus A7: pr2 (F1,F2) is covariant by A2, A5, A4, A1, Def24; :: thesis: ( F1 (*) (pr1 (F1,F2)) = F2 (*) (pr2 (F1,F2)) & ( 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,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) ) ) )

thus F1 (*) (pr1 (F1,F2)) = (pr1 (F1,F2)) * F1 by A6, A1, CAT_6:def 27

.= P01 * F1 by A4, A2, A1, Def23

.= F1 (*) P01 by A2, A1, CAT_6:def 27

.= P02 * F2 by A2, A1, A3, CAT_6:def 27

.= (pr2 (F1,F2)) * F2 by A4, A2, A1, Def24

.= F2 (*) (pr2 (F1,F2)) by A7, A1, CAT_6:def 27 ; :: thesis: 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,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

let D1 be category; :: thesis: 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,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

let G1 be Functor of D1,C1; :: thesis: 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,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

let G2 be Functor of D1,C2; :: thesis: ( G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 implies ex H being Functor of D1,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) ) )

assume ( G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 ) ; :: thesis: ex H being Functor of D1,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

then consider H0 being Functor of D1,D0 such that

A8: ( H0 is covariant & P01 (*) H0 = G1 & P02 (*) H0 = G2 & ( for H1 being Functor of D1,D0 st H1 is covariant & P01 (*) H1 = G1 & P02 (*) H1 = G2 holds

H0 = H1 ) ) by A1, A2, Def20;

reconsider H = H0 as Functor of D1,[|F1,F2|] by A5;

take H ; :: thesis: ( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

thus H is covariant by A5, A8; :: thesis: ( (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

thus (pr1 (F1,F2)) (*) H = H * (pr1 (F1,F2)) by A5, A8, A6, CAT_6:def 27

.= H0 * P01 by A4, A2, A1, Def23

.= G1 by A2, A8, CAT_6:def 27 ; :: thesis: ( (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

thus (pr2 (F1,F2)) (*) H = H * (pr2 (F1,F2)) by A5, A8, A7, CAT_6:def 27

.= H0 * P02 by A4, A2, A1, Def24

.= G2 by A2, A8, CAT_6:def 27 ; :: thesis: for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1

let H1 be Functor of D1,[|F1,F2|]; :: thesis: ( H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 implies H = H1 )

assume A9: ( H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 ) ; :: thesis: H = H1

reconsider H01 = H1 as Functor of D1,D0 by A5;

A10: P01 (*) H01 = H01 * P01 by A2, A9, A5, CAT_6:def 27

.= H1 * (pr1 (F1,F2)) by A4, A2, A1, Def23

.= G1 by A9, A6, CAT_6:def 27 ;

P02 (*) H01 = H01 * P02 by A2, A9, A5, CAT_6:def 27

.= H1 * (pr2 (F1,F2)) by A4, A2, A1, Def24

.= G2 by A9, A7, CAT_6:def 27 ;

hence H = H1 by A8, A9, A5, A10; :: thesis: verum

end;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,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) ) ) )

thus A7: pr2 (F1,F2) is covariant by A2, A5, A4, A1, Def24; :: thesis: ( F1 (*) (pr1 (F1,F2)) = F2 (*) (pr2 (F1,F2)) & ( 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,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) ) ) )

thus F1 (*) (pr1 (F1,F2)) = (pr1 (F1,F2)) * F1 by A6, A1, CAT_6:def 27

.= P01 * F1 by A4, A2, A1, Def23

.= F1 (*) P01 by A2, A1, CAT_6:def 27

.= P02 * F2 by A2, A1, A3, CAT_6:def 27

.= (pr2 (F1,F2)) * F2 by A4, A2, A1, Def24

.= F2 (*) (pr2 (F1,F2)) by A7, A1, CAT_6:def 27 ; :: thesis: 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,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

let D1 be category; :: thesis: 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,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

let G1 be Functor of D1,C1; :: thesis: 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,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

let G2 be Functor of D1,C2; :: thesis: ( G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 implies ex H being Functor of D1,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) ) )

assume ( G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 ) ; :: thesis: ex H being Functor of D1,[|F1,F2|] st

( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

then consider H0 being Functor of D1,D0 such that

A8: ( H0 is covariant & P01 (*) H0 = G1 & P02 (*) H0 = G2 & ( for H1 being Functor of D1,D0 st H1 is covariant & P01 (*) H1 = G1 & P02 (*) H1 = G2 holds

H0 = H1 ) ) by A1, A2, Def20;

reconsider H = H0 as Functor of D1,[|F1,F2|] by A5;

take H ; :: thesis: ( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

thus H is covariant by A5, A8; :: thesis: ( (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

thus (pr1 (F1,F2)) (*) H = H * (pr1 (F1,F2)) by A5, A8, A6, CAT_6:def 27

.= H0 * P01 by A4, A2, A1, Def23

.= G1 by A2, A8, CAT_6:def 27 ; :: thesis: ( (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1 ) )

thus (pr2 (F1,F2)) (*) H = H * (pr2 (F1,F2)) by A5, A8, A7, CAT_6:def 27

.= H0 * P02 by A4, A2, A1, Def24

.= G2 by A2, A8, CAT_6:def 27 ; :: thesis: for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds

H = H1

let H1 be Functor of D1,[|F1,F2|]; :: thesis: ( H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 implies H = H1 )

assume A9: ( H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 ) ; :: thesis: H = H1

reconsider H01 = H1 as Functor of D1,D0 by A5;

A10: P01 (*) H01 = H01 * P01 by A2, A9, A5, CAT_6:def 27

.= H1 * (pr1 (F1,F2)) by A4, A2, A1, Def23

.= G1 by A9, A6, CAT_6:def 27 ;

P02 (*) H01 = H01 * P02 by A2, A9, A5, CAT_6:def 27

.= H1 * (pr2 (F1,F2)) by A4, A2, A1, Def24

.= G2 by A9, A7, CAT_6:def 27 ;

hence H = H1 by A8, A9, A5, A10; :: thesis: verum