let C, D be initial category; C ~= D
ex F being Functor of C,D ex G being Functor of D,C st
( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D )
proof
consider F being
Functor of
C,
D such that A1:
(
F is
covariant & ( for
F1 being
Functor of
C,
D st
F1 is
covariant holds
F = F1 ) )
by Def8;
consider G being
Functor of
D,
C such that A2:
(
G is
covariant & ( for
G1 being
Functor of
D,
C st
G1 is
covariant holds
G = G1 ) )
by Def8;
take
F
;
ex G being Functor of D,C st
( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D )
take
G
;
( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D )
thus
(
F is
covariant &
G is
covariant )
by A1, A2;
( G (*) F = id C & F (*) G = id D )
consider F1 being
Functor of
C,
C such that A3:
(
F1 is
covariant & ( for
F2 being
Functor of
C,
C st
F2 is
covariant holds
F1 = F2 ) )
by Def8;
thus G (*) F =
F1
by A1, A2, A3, CAT_6:35
.=
id C
by A3
;
F (*) G = id D
consider G1 being
Functor of
D,
D such that A4:
(
G1 is
covariant & ( for
G2 being
Functor of
D,
D st
G2 is
covariant holds
G1 = G2 ) )
by Def8;
thus F (*) G =
G1
by A1, A2, A4, CAT_6:35
.=
id D
by A4
;
verum
end;
hence
C ~= D
by CAT_6:def 28; verum