let C, C1, C2, D, E 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

for Q1 being Functor of E,C1

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

D ~= E

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

for Q1 being Functor of E,C1

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

D ~= E

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

for P2 being Functor of D,C2

for Q1 being Functor of E,C1

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

D ~= E

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

for Q1 being Functor of E,C1

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

D ~= E

let P2 be Functor of D,C2; :: thesis: for Q1 being Functor of E,C1

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

D ~= E

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

D ~= E

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

assume A1: ( F1 is covariant & F2 is covariant ) ; :: thesis: ( not P1 is covariant or not P2 is covariant or not Q1 is covariant or not Q2 is covariant or not D,P1,P2 is_pullback_of F1,F2 or not E,Q1,Q2 is_pullback_of F1,F2 or D ~= E )

assume A2: ( P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant ) ; :: thesis: ( not D,P1,P2 is_pullback_of F1,F2 or not E,Q1,Q2 is_pullback_of F1,F2 or D ~= E )

assume A3: D,P1,P2 is_pullback_of F1,F2 ; :: thesis: ( not E,Q1,Q2 is_pullback_of F1,F2 or D ~= E )

assume A4: E,Q1,Q2 is_pullback_of F1,F2 ; :: thesis: D ~= E

ex FF being Functor of D,E ex GG being Functor of E,D st

( FF is covariant & GG is covariant & GG (*) FF = id D & FF (*) GG = id E )

for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2

for Q1 being Functor of E,C1

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

D ~= E

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

for Q1 being Functor of E,C1

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

D ~= E

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

for P2 being Functor of D,C2

for Q1 being Functor of E,C1

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

D ~= E

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

for Q1 being Functor of E,C1

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

D ~= E

let P2 be Functor of D,C2; :: thesis: for Q1 being Functor of E,C1

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

D ~= E

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

D ~= E

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

assume A1: ( F1 is covariant & F2 is covariant ) ; :: thesis: ( not P1 is covariant or not P2 is covariant or not Q1 is covariant or not Q2 is covariant or not D,P1,P2 is_pullback_of F1,F2 or not E,Q1,Q2 is_pullback_of F1,F2 or D ~= E )

assume A2: ( P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant ) ; :: thesis: ( not D,P1,P2 is_pullback_of F1,F2 or not E,Q1,Q2 is_pullback_of F1,F2 or D ~= E )

assume A3: D,P1,P2 is_pullback_of F1,F2 ; :: thesis: ( not E,Q1,Q2 is_pullback_of F1,F2 or D ~= E )

assume A4: E,Q1,Q2 is_pullback_of F1,F2 ; :: thesis: D ~= E

ex FF being Functor of D,E ex GG being Functor of E,D st

( FF is covariant & GG is covariant & GG (*) FF = id D & FF (*) GG = id E )

proof

hence
D ~= E
by CAT_6:def 28; :: thesis: verum
A5:
( F1 (*) P1 = F2 (*) P2 & ( for D0 being category

for G1 being Functor of D0,C1

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

ex H being Functor of D0,D st

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

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

A6: ( F1 (*) Q1 = F2 (*) Q2 & ( for D0 being category

for G1 being Functor of D0,C1

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

ex H being Functor of D0,E st

( H is covariant & Q1 (*) H = G1 & Q2 (*) H = G2 & ( for H1 being Functor of D0,E st H1 is covariant & Q1 (*) H1 = G1 & Q2 (*) H1 = G2 holds

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

consider FF being Functor of D,E such that

A7: ( FF is covariant & Q1 (*) FF = P1 & Q2 (*) FF = P2 & ( for H1 being Functor of D,E st H1 is covariant & Q1 (*) H1 = P1 & Q2 (*) H1 = P2 holds

FF = H1 ) ) by A2, A5, A1, A4, Def20;

consider GG being Functor of E,D such that

A8: ( GG is covariant & P1 (*) GG = Q1 & P2 (*) GG = Q2 & ( for H1 being Functor of E,D st H1 is covariant & P1 (*) H1 = Q1 & P2 (*) H1 = Q2 holds

GG = H1 ) ) by A2, A6, A1, A3, Def20;

take FF ; :: thesis: ex GG being Functor of E,D st

( FF is covariant & GG is covariant & GG (*) FF = id D & FF (*) GG = id E )

take GG ; :: thesis: ( FF is covariant & GG is covariant & GG (*) FF = id D & FF (*) GG = id E )

thus ( FF is covariant & GG is covariant ) by A7, A8; :: thesis: ( GG (*) FF = id D & FF (*) GG = id E )

set G11 = Q1 (*) FF;

set G12 = Q2 (*) FF;

consider H1 being Functor of D,D such that

A9: ( H1 is covariant & P1 (*) H1 = Q1 (*) FF & P2 (*) H1 = Q2 (*) FF & ( for H being Functor of D,D st H is covariant & P1 (*) H = Q1 (*) FF & P2 (*) H = Q2 (*) FF holds

H1 = H ) ) by A2, A5, A7;

A10: P1 (*) (GG (*) FF) = Q1 (*) FF by A2, A7, A8, Th10;

A11: P2 (*) (GG (*) FF) = Q2 (*) FF by A2, A7, A8, Th10;

A12: P1 (*) (id D) = Q1 (*) FF by A2, A7, Th11;

A13: P2 (*) (id D) = Q2 (*) FF by A2, A7, Th11;

thus GG (*) FF = H1 by A9, A10, A11, A7, A8, CAT_6:35

.= id D by A9, A12, A13 ; :: thesis: FF (*) GG = id E

set G21 = P1 (*) GG;

set G22 = P2 (*) GG;

consider H2 being Functor of E,E such that

A14: ( H2 is covariant & Q1 (*) H2 = P1 (*) GG & Q2 (*) H2 = P2 (*) GG & ( for H being Functor of E,E st H is covariant & Q1 (*) H = P1 (*) GG & Q2 (*) H = P2 (*) GG holds

H2 = H ) ) by A2, A6, A8;

A15: Q1 (*) (FF (*) GG) = P1 (*) GG by A2, A7, A8, Th10;

A16: Q2 (*) (FF (*) GG) = P2 (*) GG by A2, A7, A8, Th10;

A17: Q1 (*) (id E) = P1 (*) GG by A2, A8, Th11;

A18: Q2 (*) (id E) = P2 (*) GG by A2, A8, Th11;

thus FF (*) GG = H2 by A14, A15, A16, A7, A8, CAT_6:35

.= id E by A14, A17, A18 ; :: thesis: verum

end;for G1 being Functor of D0,C1

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

ex H being Functor of D0,D st

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

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

A6: ( F1 (*) Q1 = F2 (*) Q2 & ( for D0 being category

for G1 being Functor of D0,C1

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

ex H being Functor of D0,E st

( H is covariant & Q1 (*) H = G1 & Q2 (*) H = G2 & ( for H1 being Functor of D0,E st H1 is covariant & Q1 (*) H1 = G1 & Q2 (*) H1 = G2 holds

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

consider FF being Functor of D,E such that

A7: ( FF is covariant & Q1 (*) FF = P1 & Q2 (*) FF = P2 & ( for H1 being Functor of D,E st H1 is covariant & Q1 (*) H1 = P1 & Q2 (*) H1 = P2 holds

FF = H1 ) ) by A2, A5, A1, A4, Def20;

consider GG being Functor of E,D such that

A8: ( GG is covariant & P1 (*) GG = Q1 & P2 (*) GG = Q2 & ( for H1 being Functor of E,D st H1 is covariant & P1 (*) H1 = Q1 & P2 (*) H1 = Q2 holds

GG = H1 ) ) by A2, A6, A1, A3, Def20;

take FF ; :: thesis: ex GG being Functor of E,D st

( FF is covariant & GG is covariant & GG (*) FF = id D & FF (*) GG = id E )

take GG ; :: thesis: ( FF is covariant & GG is covariant & GG (*) FF = id D & FF (*) GG = id E )

thus ( FF is covariant & GG is covariant ) by A7, A8; :: thesis: ( GG (*) FF = id D & FF (*) GG = id E )

set G11 = Q1 (*) FF;

set G12 = Q2 (*) FF;

consider H1 being Functor of D,D such that

A9: ( H1 is covariant & P1 (*) H1 = Q1 (*) FF & P2 (*) H1 = Q2 (*) FF & ( for H being Functor of D,D st H is covariant & P1 (*) H = Q1 (*) FF & P2 (*) H = Q2 (*) FF holds

H1 = H ) ) by A2, A5, A7;

A10: P1 (*) (GG (*) FF) = Q1 (*) FF by A2, A7, A8, Th10;

A11: P2 (*) (GG (*) FF) = Q2 (*) FF by A2, A7, A8, Th10;

A12: P1 (*) (id D) = Q1 (*) FF by A2, A7, Th11;

A13: P2 (*) (id D) = Q2 (*) FF by A2, A7, Th11;

thus GG (*) FF = H1 by A9, A10, A11, A7, A8, CAT_6:35

.= id D by A9, A12, A13 ; :: thesis: FF (*) GG = id E

set G21 = P1 (*) GG;

set G22 = P2 (*) GG;

consider H2 being Functor of E,E such that

A14: ( H2 is covariant & Q1 (*) H2 = P1 (*) GG & Q2 (*) H2 = P2 (*) GG & ( for H being Functor of E,E st H is covariant & Q1 (*) H = P1 (*) GG & Q2 (*) H = P2 (*) GG holds

H2 = H ) ) by A2, A6, A8;

A15: Q1 (*) (FF (*) GG) = P1 (*) GG by A2, A7, A8, Th10;

A16: Q2 (*) (FF (*) GG) = P2 (*) GG by A2, A7, A8, Th10;

A17: Q1 (*) (id E) = P1 (*) GG by A2, A8, Th11;

A18: Q2 (*) (id E) = P2 (*) GG by A2, A8, Th11;

thus FF (*) GG = H2 by A14, A15, A16, A7, A8, CAT_6:35

.= id E by A14, A17, A18 ; :: thesis: verum