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 ) )

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 ;

( 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 )

given F being Functor of C,D such that A3:
( F is covariant & F is bijective )
; :: thesis: C ~= D( 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;( 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

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 = {} )
;

end;

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

f1 = f2

G . g is identity

A19: for f being morphism of C holds G . (F . f) = f

( G . g1 |> G . g2 & G . (g1 (*) g2) = (G . g1) (*) (G . g2) )

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;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

A13:
for f1, f2 being morphism of C st F . f1 = F . f2 holds
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;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

f1 = f2

proof

for g being morphism of D st g is identity holds
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;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

G . g is identity

proof

then A18:
G is identity-preserving
by CAT_6:def 22;
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

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;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

then
G . g is left_identity
by CAT_6:def 4;
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;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

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

A19: for f being morphism of C holds G . (F . f) = f

proof

for g1, g2 being morphism of D st g1 |> g2 holds
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;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

( G . g1 |> G . g2 & G . (g1 (*) g2) = (G . g1) (*) (G . g2) )

proof

then A27:
G is covariant
by A18, CAT_6:def 23, CAT_6:def 25;
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;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

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

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;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