let C, C1, C2, D, E be category; 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; 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; 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; 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; 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; 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; ( 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 )
; ( 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 )
; ( 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
; ( not E,Q1,Q2 is_pullback_of F1,F2 or D ~= E )
assume A4:
E,Q1,Q2 is_pullback_of F1,F2
; 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
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
;
ex GG being Functor of E,D st
( FF is covariant & GG is covariant & GG (*) FF = id D & FF (*) GG = id E )
take
GG
;
( FF is covariant & GG is covariant & GG (*) FF = id D & FF (*) GG = id E )
thus
(
FF is
covariant &
GG is
covariant )
by A7, A8;
( 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
;
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
;
verum
end;
hence
D ~= E
by CAT_6:def 28; verum