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

for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 holds

D,P2,P1 is_pullback_of F2,F1

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

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 holds

D,P2,P1 is_pullback_of F2,F1

let F2 be Functor of C2,C; :: thesis: for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 holds

D,P2,P1 is_pullback_of F2,F1

let P1 be Functor of D,C1; :: thesis: for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 holds

D,P2,P1 is_pullback_of F2,F1

let P2 be Functor of D,C2; :: thesis: ( F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 implies D,P2,P1 is_pullback_of F2,F1 )

assume A1: ( F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant ) ; :: thesis: ( not D,P1,P2 is_pullback_of F1,F2 or D,P2,P1 is_pullback_of F2,F1 )

assume A2: D,P1,P2 is_pullback_of F1,F2 ; :: thesis: D,P2,P1 is_pullback_of F2,F1

then A3: ( 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 ) ) ) ) by A1, Def20;

for D1 being category

for G1 being Functor of D1,C2

for G2 being Functor of D1,C1 st G1 is covariant & G2 is covariant & F2 (*) G1 = F1 (*) G2 holds

ex H being Functor of D1,D st

( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1 ) )

for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 holds

D,P2,P1 is_pullback_of F2,F1

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

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 holds

D,P2,P1 is_pullback_of F2,F1

let F2 be Functor of C2,C; :: thesis: for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 holds

D,P2,P1 is_pullback_of F2,F1

let P1 be Functor of D,C1; :: thesis: for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 holds

D,P2,P1 is_pullback_of F2,F1

let P2 be Functor of D,C2; :: thesis: ( F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 implies D,P2,P1 is_pullback_of F2,F1 )

assume A1: ( F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant ) ; :: thesis: ( not D,P1,P2 is_pullback_of F1,F2 or D,P2,P1 is_pullback_of F2,F1 )

assume A2: D,P1,P2 is_pullback_of F1,F2 ; :: thesis: D,P2,P1 is_pullback_of F2,F1

then A3: ( 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 ) ) ) ) by A1, Def20;

for D1 being category

for G1 being Functor of D1,C2

for G2 being Functor of D1,C1 st G1 is covariant & G2 is covariant & F2 (*) G1 = F1 (*) G2 holds

ex H being Functor of D1,D st

( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1 ) )

proof

hence
D,P2,P1 is_pullback_of F2,F1
by A3, A1, Def20; :: thesis: verum
let D1 be category; :: thesis: for G1 being Functor of D1,C2

for G2 being Functor of D1,C1 st G1 is covariant & G2 is covariant & F2 (*) G1 = F1 (*) G2 holds

ex H being Functor of D1,D st

( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1 ) )

let G1 be Functor of D1,C2; :: thesis: for G2 being Functor of D1,C1 st G1 is covariant & G2 is covariant & F2 (*) G1 = F1 (*) G2 holds

ex H being Functor of D1,D st

( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1 ) )

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

( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1 ) ) )

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

( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1 ) )

consider H being Functor of D1,D such that

A5: ( H is covariant & P1 (*) H = G2 & P2 (*) H = G1 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G2 & P2 (*) H1 = G1 holds

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

take H ; :: thesis: ( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1 ) )

thus ( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 ) by A5; :: thesis: for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1

let H1 be Functor of D1,D; :: thesis: ( H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 implies H = H1 )

assume ( H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 ) ; :: thesis: H = H1

hence H = H1 by A5; :: thesis: verum

end;for G2 being Functor of D1,C1 st G1 is covariant & G2 is covariant & F2 (*) G1 = F1 (*) G2 holds

ex H being Functor of D1,D st

( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1 ) )

let G1 be Functor of D1,C2; :: thesis: for G2 being Functor of D1,C1 st G1 is covariant & G2 is covariant & F2 (*) G1 = F1 (*) G2 holds

ex H being Functor of D1,D st

( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1 ) )

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

( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1 ) ) )

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

( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1 ) )

consider H being Functor of D1,D such that

A5: ( H is covariant & P1 (*) H = G2 & P2 (*) H = G1 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G2 & P2 (*) H1 = G1 holds

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

take H ; :: thesis: ( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1 ) )

thus ( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 ) by A5; :: thesis: for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds

H = H1

let H1 be Functor of D1,D; :: thesis: ( H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 implies H = H1 )

assume ( H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 ) ; :: thesis: H = H1

hence H = H1 by A5; :: thesis: verum