let C, D be composable with_identities CategoryStr ; :: thesis: ( C ~= D iff ex F being Functor of C,D st
( F is covariant & F is bijective ) )

hereby :: thesis: ( ex F being Functor of C,D st
( F is covariant & F is bijective ) implies C ~= D )

assume C ~= D ; :: thesis: ex F being Functor of C,D st
( F is covariant & F is bijective )
then consider F being Functor of C,D, G being Functor of D,C such that
A1: ( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D ) by CAT_6:def 28;
take F = F; :: thesis: ( F is covariant & F is bijective )
thus F is covariant by A1; :: thesis: F is bijective
F * G = id C by A1, CAT_6:def 27
.= id the carrier of C by STRUCT_0:def 4 ;
then A2: F is one-to-one by FUNCT_2:23;
G * F = id D by A1, CAT_6:def 27
.= id the carrier of D by STRUCT_0:def 4 ;
then F is onto by FUNCT_2:23;
hence F is bijective by A2; :: thesis: verum

end;

given F being Functor of C,D such that A3: ( F is covariant & F is bijective ) ; :: thesis: C ~= D
A4: rng F = the carrier of D by A3, FUNCT_2:def 3;
then reconsider G = F " as Function of the carrier of D, the carrier of C by A3, FUNCT_2:25;
reconsider G = G as Functor of D,C ;

per cases ( the carrier of D <> {} or the carrier of D = {} ) ;

suppose A5: the carrier of D <> {} ; :: thesis: C ~= D

then A6: ( G * F = id the carrier of D & F * G = id the carrier of C ) by A3, A4, FUNCT_2:29;
A7: not D is empty by A5;
A8: not C is empty by A4, A5;
A9: ( F is identity-preserving & F is multiplicative ) by A3, CAT_6:def 25;
A10: for g being morphism of D holds F . (G . g) = g

proof

let g be morphism of D; :: thesis: F . (G . g) = g
reconsider x1 = G . g, x2 = g as object ;
g in Mor D by A7, SUBSET_1:def 1;
then A11: g in the carrier of D by CAT_6:def 1;
then A12: x2 in dom G by A8, FUNCT_2:def 1;
thus F . (G . g) = F . x1 by A8, CAT_6:def 21
.= F . (G . x2) by A7, CAT_6:def 21
.= (id the carrier of D) . x2 by A6, A12, FUNCT_1:13
.= g by A11, FUNCT_1:18 ; :: thesis: verum

end;

A13: for f1, f2 being morphism of C st F . f1 = F . f2 holds
f1 = f2

proof

let f1, f2 be morphism of C; :: thesis: ( F . f1 = F . f2 implies f1 = f2 )
assume A14: F . f1 = F . f2 ; :: thesis: f1 = f2
reconsider x1 = f1, x2 = f2 as object ;
( f1 in Mor C & f2 in Mor C ) by A8, SUBSET_1:def 1;
then ( f1 in the carrier of C & f2 in the carrier of C ) by CAT_6:def 1;
then A15: ( x1 in dom F & x2 in dom F ) by A5, FUNCT_2:def 1;
F . x1 = F . f1 by A8, CAT_6:def 21
.= F . x2 by A14, A8, CAT_6:def 21 ;
hence f1 = f2 by A3, A15, FUNCT_1:def 4; :: thesis: verum

end;

for g being morphism of D st g is identity holds
G . g is identity

proof

let g be morphism of D; :: thesis: ( g is identity implies G . g is identity )
assume g is identity ; :: thesis: G . g is identity
then A16: for g1 being morphism of D st g |> g1 holds
g (*) g1 = g1 by CAT_6:def 4, CAT_6:def 14;
A17: for f1 being morphism of C st G . g |> f1 holds
(G . g) (*) f1 = f1

proof

let f1 be morphism of C; :: thesis: ( G . g |> f1 implies (G . g) (*) f1 = f1 )
assume G . g |> f1 ; :: thesis: (G . g) (*) f1 = f1
then ( F . (G . g) |> F . f1 & F . ((G . g) (*) f1) = (F . (G . g)) (*) (F . f1) ) by A9, CAT_6:def 23;
then ( g |> F . f1 & F . ((G . g) (*) f1) = g (*) (F . f1) ) by A10;
hence (G . g) (*) f1 = f1 by A16, A13; :: thesis: verum

end;

then G . g is left_identity by CAT_6:def 4;
then G . g is right_identity by CAT_6:9;
hence G . g is identity by A17, CAT_6:def 4, CAT_6:def 14; :: thesis: verum

end;

then A18: G is identity-preserving by CAT_6:def 22;
A19: for f being morphism of C holds G . (F . f) = f

proof

let f be morphism of C; :: thesis: G . (F . f) = f
reconsider x1 = F . f, x2 = f as object ;
f in Mor C by A8, SUBSET_1:def 1;
then A20: f in the carrier of C by CAT_6:def 1;
then A21: x2 in dom F by A5, FUNCT_2:def 1;
thus G . (F . f) = G . x1 by A7, CAT_6:def 21
.= G . (F . x2) by A8, CAT_6:def 21
.= (id the carrier of C) . x2 by A6, A21, FUNCT_1:13
.= f by A20, FUNCT_1:18 ; :: thesis: verum

end;

for g1, g2 being morphism of D st g1 |> g2 holds
( G . g1 |> G . g2 & G . (g1 (*) g2) = (G . g1) (*) (G . g2) )

proof

let g1, g2 be morphism of D; :: thesis: ( g1 |> g2 implies ( G . g1 |> G . g2 & G . (g1 (*) g2) = (G . g1) (*) (G . g2) ) )
assume A22: g1 |> g2 ; :: thesis: ( G . g1 |> G . g2 & G . (g1 (*) g2) = (G . g1) (*) (G . g2) )
reconsider f1 = G . g1, f2 = G . g2 as morphism of C ;
A23: ( g1 = F . (G . g1) & g2 = F . (G . g2) ) by A10;
A24: dom (F . f1) = cod (F . f2) by A22, A23, A7, Th5;
not Ob C is empty by A8;
then ( dom f1 in Ob C & cod f2 in Ob C ) ;
then reconsider d1 = dom f1, c2 = cod f2 as morphism of C ;
F . d1 = F . (dom f1) by A8, CAT_6:def 21
.= dom (F . f1) by A7, A8, A3, CAT_6:32
.= F . (cod f2) by A24, A7, A8, A3, CAT_6:32
.= F . c2 by A8, CAT_6:def 21 ;
hence A25: G . g1 |> G . g2 by A13, A8, Th5; :: thesis: G . (g1 (*) g2) = (G . g1) (*) (G . g2)
A26: F is multiplicative by A3, CAT_6:def 25;
g1 (*) g2 = F . ((G . g1) (*) (G . g2)) by A23, A26, A25, CAT_6:def 23;
hence G . (g1 (*) g2) = (G . g1) (*) (G . g2) by A19; :: thesis: verum

end;

then A27: G is covariant by A18, CAT_6:def 23, CAT_6:def 25;
then ( G * F = F (*) G & F * G = G (*) F ) by A3, CAT_6:def 27;
then ( G (*) F = id C & F (*) G = id D ) by A6, STRUCT_0:def 4;
hence C ~= D by A3, A27, CAT_6:def 28; :: thesis: verum

end;

suppose A28: the carrier of D = {} ; :: thesis: C ~= D

then A29: D is empty ;
then A30: C is empty by A3, CAT_6:31;
for g being morphism of D st g is identity holds
G . g is identity by A30, CAT_6:10;
then A31: G is identity-preserving by CAT_6:def 22;
for g1, g2 being morphism of D st g1 |> g2 holds
( G . g1 |> G . g2 & G . (g1 (*) g2) = (G . g1) (*) (G . g2) ) by A29, CAT_6:1;
then A32: G is covariant by A31, CAT_6:def 23, CAT_6:def 25;
( G (*) F = id C & F (*) G = id D ) by A30, A28;
hence C ~= D by A3, A32, CAT_6:def 28; :: thesis: verum

end;

end;