consider F being covariant Functor of F1(),F2() such that
A7:
for a being Object of F1() holds F . a = F3(a)
and
A8:
for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F5(a,b,f)
by A1;
consider G being covariant Functor of F2(),F1() such that
A9:
for a being Object of F2() holds G . a = F4(a)
and
A10:
for a, b being Object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = F6(a,b,f)
by A2;
take
F
; YELLOW18:def 2 ex G being covariant Functor of F2(),F1() st
( G * F, id F1() are_naturally_equivalent & F * G, id F2() are_naturally_equivalent )
take
G
; ( G * F, id F1() are_naturally_equivalent & F * G, id F2() are_naturally_equivalent )
set GF = G * F;
set I = id F1();
A11:
for a being Object of F1() holds
( F7(a) in <^((G * F) . a),((id F1()) . a)^> & <^((id F1()) . a),((G * F) . a)^> <> {} & ( for f being Morphism of ((G * F) . a),((id F1()) . a) st f = F7(a) holds
f is iso ) )
proof
let a be
Object of
F1();
( F7(a) in <^((G * F) . a),((id F1()) . a)^> & <^((id F1()) . a),((G * F) . a)^> <> {} & ( for f being Morphism of ((G * F) . a),((id F1()) . a) st f = F7(a) holds
f is iso ) )
A12:
(G * F) . a =
G . (F . a)
by FUNCTOR0:33
.=
F4(
(F . a))
by A9
.=
F4(
F3(
a))
by A7
;
A13:
(id F1()) . a = a
by FUNCTOR0:29;
then A14:
F7(
a)
in <^((G * F) . a),((id F1()) . a)^>
by A3, A12;
A15:
F7(
a)
" in <^((id F1()) . a),((G * F) . a)^>
by A3, A12, A13;
F7(
a) is
one-to-one
by A3, A12;
hence
(
F7(
a)
in <^((G * F) . a),((id F1()) . a)^> &
<^((id F1()) . a),((G * F) . a)^> <> {} & ( for
f being
Morphism of
((G * F) . a),
((id F1()) . a) st
f = F7(
a) holds
f is
iso ) )
by A14, A15, Th41;
verum
end;
A16:
for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b
for g1 being Morphism of ((G * F) . a),((id F1()) . a) st g1 = F7(a) holds
for g2 being Morphism of ((G * F) . b),((id F1()) . b) st g2 = F7(b) holds
g2 * ((G * F) . f) = ((id F1()) . f) * g1
proof
let a,
b be
Object of
F1();
( <^a,b^> <> {} implies for f being Morphism of a,b
for g1 being Morphism of ((G * F) . a),((id F1()) . a) st g1 = F7(a) holds
for g2 being Morphism of ((G * F) . b),((id F1()) . b) st g2 = F7(b) holds
g2 * ((G * F) . f) = ((id F1()) . f) * g1 )
assume A17:
<^a,b^> <> {}
;
for f being Morphism of a,b
for g1 being Morphism of ((G * F) . a),((id F1()) . a) st g1 = F7(a) holds
for g2 being Morphism of ((G * F) . b),((id F1()) . b) st g2 = F7(b) holds
g2 * ((G * F) . f) = ((id F1()) . f) * g1
A18:
F7(
a)
in <^((G * F) . a),((id F1()) . a)^>
by A11;
A19:
F7(
b)
in <^((G * F) . b),((id F1()) . b)^>
by A11;
reconsider g2 =
F7(
b) as
Morphism of
((G * F) . b),
((id F1()) . b) by A11;
A20:
<^((G * F) . a),((G * F) . b)^> <> {}
by A17, FUNCTOR0:def 18;
A21:
<^((id F1()) . a),((id F1()) . b)^> <> {}
by A17, FUNCTOR0:def 18;
let f be
Morphism of
a,
b;
for g1 being Morphism of ((G * F) . a),((id F1()) . a) st g1 = F7(a) holds
for g2 being Morphism of ((G * F) . b),((id F1()) . b) st g2 = F7(b) holds
g2 * ((G * F) . f) = ((id F1()) . f) * g1
A22:
(G * F) . f = G . (F . f)
by A17, FUNCTOR3:6;
A23:
F3(
a)
= F . a
by A7;
A24:
F3(
b)
= F . b
by A7;
A25:
F5(
a,
b,
f)
= F . f
by A8, A17;
<^(F . a),(F . b)^> <> {}
by A17, FUNCTOR0:def 18;
then
F6(
F3(
a),
F3(
b),
F5(
a,
b,
f))
= (G * F) . f
by A10, A22, A23, A24, A25;
then g2 * ((G * F) . f) =
F7(
b)
* F6(
F3(
a),
F3(
b),
F5(
a,
b,
f))
by A19, A20, Th36
.=
f * F7(
a)
by A5, A17
.=
((id F1()) . f) * F7(
a)
by A17, FUNCTOR0:31
;
hence
for
g1 being
Morphism of
((G * F) . a),
((id F1()) . a) st
g1 = F7(
a) holds
for
g2 being
Morphism of
((G * F) . b),
((id F1()) . b) st
g2 = F7(
b) holds
g2 * ((G * F) . f) = ((id F1()) . f) * g1
by A18, A21, Th36;
verum
end;
ex t being natural_equivalence of G * F, id F1() st
( G * F, id F1() are_naturally_equivalent & ( for a being Object of F1() holds t ! a = F7(a) ) )
from YELLOW18:sch 15(A11, A16);
hence
G * F, id F1() are_naturally_equivalent
; F * G, id F2() are_naturally_equivalent
set I = id F2();
set FG = F * G;
A26:
for a being Object of F2() holds
( F8(a) in <^((id F2()) . a),((F * G) . a)^> & <^((F * G) . a),((id F2()) . a)^> <> {} & ( for f being Morphism of ((id F2()) . a),((F * G) . a) st f = F8(a) holds
f is iso ) )
proof
let a be
Object of
F2();
( F8(a) in <^((id F2()) . a),((F * G) . a)^> & <^((F * G) . a),((id F2()) . a)^> <> {} & ( for f being Morphism of ((id F2()) . a),((F * G) . a) st f = F8(a) holds
f is iso ) )
A27:
(F * G) . a =
F . (G . a)
by FUNCTOR0:33
.=
F3(
(G . a))
by A7
.=
F3(
F4(
a))
by A9
;
A28:
(id F2()) . a = a
by FUNCTOR0:29;
then A29:
F8(
a)
in <^((id F2()) . a),((F * G) . a)^>
by A4, A27;
A30:
F8(
a)
" in <^((F * G) . a),((id F2()) . a)^>
by A4, A27, A28;
F8(
a) is
one-to-one
by A4, A27;
hence
(
F8(
a)
in <^((id F2()) . a),((F * G) . a)^> &
<^((F * G) . a),((id F2()) . a)^> <> {} & ( for
f being
Morphism of
((id F2()) . a),
((F * G) . a) st
f = F8(
a) holds
f is
iso ) )
by A29, A30, Th41;
verum
end;
A31:
for a, b being Object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b
for g1 being Morphism of ((id F2()) . a),((F * G) . a) st g1 = F8(a) holds
for g2 being Morphism of ((id F2()) . b),((F * G) . b) st g2 = F8(b) holds
g2 * ((id F2()) . f) = ((F * G) . f) * g1
proof
let a,
b be
Object of
F2();
( <^a,b^> <> {} implies for f being Morphism of a,b
for g1 being Morphism of ((id F2()) . a),((F * G) . a) st g1 = F8(a) holds
for g2 being Morphism of ((id F2()) . b),((F * G) . b) st g2 = F8(b) holds
g2 * ((id F2()) . f) = ((F * G) . f) * g1 )
assume A32:
<^a,b^> <> {}
;
for f being Morphism of a,b
for g1 being Morphism of ((id F2()) . a),((F * G) . a) st g1 = F8(a) holds
for g2 being Morphism of ((id F2()) . b),((F * G) . b) st g2 = F8(b) holds
g2 * ((id F2()) . f) = ((F * G) . f) * g1
A33:
F8(
a)
in <^((id F2()) . a),((F * G) . a)^>
by A26;
reconsider g1 =
F8(
a) as
Morphism of
((id F2()) . a),
((F * G) . a) by A26;
A34:
F8(
b)
in <^((id F2()) . b),((F * G) . b)^>
by A26;
A35:
<^((F * G) . a),((F * G) . b)^> <> {}
by A32, FUNCTOR0:def 18;
A36:
<^((id F2()) . a),((id F2()) . b)^> <> {}
by A32, FUNCTOR0:def 18;
let f be
Morphism of
a,
b;
for g1 being Morphism of ((id F2()) . a),((F * G) . a) st g1 = F8(a) holds
for g2 being Morphism of ((id F2()) . b),((F * G) . b) st g2 = F8(b) holds
g2 * ((id F2()) . f) = ((F * G) . f) * g1
A37:
(F * G) . f = F . (G . f)
by A32, FUNCTOR3:6;
A38:
F4(
a)
= G . a
by A9;
A39:
F4(
b)
= G . b
by A9;
A40:
F6(
a,
b,
f)
= G . f
by A10, A32;
<^(G . a),(G . b)^> <> {}
by A32, FUNCTOR0:def 18;
then
F5(
F4(
a),
F4(
b),
F6(
a,
b,
f))
= (F * G) . f
by A8, A37, A38, A39, A40;
then ((F * G) . f) * g1 =
F5(
F4(
a),
F4(
b),
F6(
a,
b,
f))
* F8(
a)
by A33, A35, Th36
.=
F8(
b)
* f
by A6, A32
.=
F8(
b)
* ((id F2()) . f)
by A32, FUNCTOR0:31
;
hence
for
g1 being
Morphism of
((id F2()) . a),
((F * G) . a) st
g1 = F8(
a) holds
for
g2 being
Morphism of
((id F2()) . b),
((F * G) . b) st
g2 = F8(
b) holds
g2 * ((id F2()) . f) = ((F * G) . f) * g1
by A34, A36, Th36;
verum
end;
ex t being natural_equivalence of id F2(),F * G st
( id F2(),F * G are_naturally_equivalent & ( for a being Object of F2() holds t ! a = F8(a) ) )
from YELLOW18:sch 15(A26, A31);
hence
F * G, id F2() are_naturally_equivalent
; verum