let C, C1, C2 be category; 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; 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; ( 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 )
; ( 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
thus A6:
pr1 (
F1,
F2) is
covariant
by A2, A5, A4, A1, Def23;
( 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;
( 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
;
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;
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;
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;
( 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 )
;
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
;
( 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;
( (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
;
( (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
;
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|];
( 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 )
;
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;
verum
end;
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; verum