let A, B, C1, C2 be category; for E1 being Functor of (C1 [x] A),B
for E2 being Functor of (C2 [x] A),B st E1 is covariant & E2 is covariant & C1,E1 is_exponent_of A,B & C2,E2 is_exponent_of A,B holds
C1 ~= C2
let E1 be Functor of (C1 [x] A),B; for E2 being Functor of (C2 [x] A),B st E1 is covariant & E2 is covariant & C1,E1 is_exponent_of A,B & C2,E2 is_exponent_of A,B holds
C1 ~= C2
let E2 be Functor of (C2 [x] A),B; ( E1 is covariant & E2 is covariant & C1,E1 is_exponent_of A,B & C2,E2 is_exponent_of A,B implies C1 ~= C2 )
assume A1:
E1 is covariant
; ( not E2 is covariant or not C1,E1 is_exponent_of A,B or not C2,E2 is_exponent_of A,B or C1 ~= C2 )
assume A2:
E2 is covariant
; ( not C1,E1 is_exponent_of A,B or not C2,E2 is_exponent_of A,B or C1 ~= C2 )
assume A3:
C1,E1 is_exponent_of A,B
; ( not C2,E2 is_exponent_of A,B or C1 ~= C2 )
assume A4:
C2,E2 is_exponent_of A,B
; C1 ~= C2
ex F being Functor of C1,C2 ex G being Functor of C2,C1 st
( F is covariant & G is covariant & G (*) F = id C1 & F (*) G = id C2 )
proof
consider F being
Functor of
C1,
C2 such that A5:
(
F is
covariant &
E1 = E2 (*) (F [x] (id A)) & ( for
H1 being
Functor of
C1,
C2 st
H1 is
covariant &
E1 = E2 (*) (H1 [x] (id A)) holds
F = H1 ) )
by A1, A2, A4, Def34;
consider G being
Functor of
C2,
C1 such that A6:
(
G is
covariant &
E2 = E1 (*) (G [x] (id A)) & ( for
H1 being
Functor of
C2,
C1 st
H1 is
covariant &
E2 = E1 (*) (H1 [x] (id A)) holds
G = H1 ) )
by A1, A2, A3, Def34;
take
F
;
ex G being Functor of C2,C1 st
( F is covariant & G is covariant & G (*) F = id C1 & F (*) G = id C2 )
take
G
;
( F is covariant & G is covariant & G (*) F = id C1 & F (*) G = id C2 )
thus
(
F is
covariant &
G is
covariant )
by A5, A6;
( G (*) F = id C1 & F (*) G = id C2 )
consider H2 being
Functor of
C1,
C1 such that A7:
(
H2 is
covariant &
E1 = E1 (*) (H2 [x] (id A)) & ( for
H1 being
Functor of
C1,
C1 st
H1 is
covariant &
E1 = E1 (*) (H1 [x] (id A)) holds
H2 = H1 ) )
by A1, A3, Def34;
A8:
G [x] (id A) is
covariant
by A6, Def22;
A9:
F [x] (id A) is
covariant
by A5, Def22;
E1 =
E1 (*) ((G [x] (id A)) (*) (F [x] (id A)))
by A5, A6, A8, A9, A1, CAT_7:10
.=
E1 (*) ((G (*) F) [x] ((id A) (*) (id A)))
by A5, A6, Th50
.=
E1 (*) ((G (*) F) [x] (id A))
by CAT_7:11
;
then A10:
G (*) F = H2
by A7, A5, A6, CAT_6:35;
E1 =
E1 (*) (id (C1 [x] A))
by A1, CAT_7:11
.=
E1 (*) ((id C1) [x] (id A))
by Th51
;
hence
G (*) F = id C1
by A7, A10;
F (*) G = id C2
consider H3 being
Functor of
C2,
C2 such that A11:
(
H3 is
covariant &
E2 = E2 (*) (H3 [x] (id A)) & ( for
H1 being
Functor of
C2,
C2 st
H1 is
covariant &
E2 = E2 (*) (H1 [x] (id A)) holds
H3 = H1 ) )
by A2, A4, Def34;
E2 =
E2 (*) ((F [x] (id A)) (*) (G [x] (id A)))
by A2, A5, A6, A8, A9, CAT_7:10
.=
E2 (*) ((F (*) G) [x] ((id A) (*) (id A)))
by A5, A6, Th50
.=
E2 (*) ((F (*) G) [x] (id A))
by CAT_7:11
;
then A12:
F (*) G = H3
by A11, A5, A6, CAT_6:35;
E2 =
E2 (*) (id (C2 [x] A))
by A2, CAT_7:11
.=
E2 (*) ((id C2) [x] (id A))
by Th51
;
hence
F (*) G = id C2
by A11, A12;
verum
end;
hence
C1,C2 are_isomorphic
by CAT_6:def 28; verum