let A, B, C be Category; for F1, F2 being Functor of [:A,B:],C st export F1 is_naturally_transformable_to export F2 holds
for t being natural_transformation of export F1, export F2 holds
( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u )
let F1, F2 be Functor of [:A,B:],C; ( export F1 is_naturally_transformable_to export F2 implies for t being natural_transformation of export F1, export F2 holds
( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u ) )
assume A1:
export F1 is_naturally_transformable_to export F2
; for t being natural_transformation of export F1, export F2 holds
( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u )
let t be natural_transformation of export F1, export F2; ( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u )
defpred S1[ set , set ] means for a being Object of A st $1 = a holds
t . a = [[((export F1) . a),((export F2) . a)],$2];
A2:
now let o be
set ;
( o in the carrier of A implies ex m being set st
( m in Funcs ( the carrier of B, the carrier' of C) & S1[o,m] ) )assume
o in the
carrier of
A
;
ex m being set st
( m in Funcs ( the carrier of B, the carrier' of C) & S1[o,m] )then reconsider a9 =
o as
Object of
A ;
consider f1,
f2 being
Functor of
B,
C,
tau being
natural_transformation of
f1,
f2 such that
f1 is_naturally_transformable_to f2
and A3:
dom (t . a9) = f1
and A4:
(
cod (t . a9) = f2 &
t . a9 = [[f1,f2],tau] )
by Th9;
reconsider m =
tau as
set ;
take m =
m;
( m in Funcs ( the carrier of B, the carrier' of C) & S1[o,m] )thus
m in Funcs ( the
carrier of
B, the
carrier' of
C)
by FUNCT_2:8;
S1[o,m]thus
S1[
o,
m]
verumproof
let a be
Object of
A;
( o = a implies t . a = [[((export F1) . a),((export F2) . a)],m] )
assume A5:
o = a
;
t . a = [[((export F1) . a),((export F2) . a)],m]
export F1 is_transformable_to export F2
by A1, NATTRA_1:def 7;
then A6:
Hom (
((export F1) . a),
((export F2) . a))
<> {}
by NATTRA_1:def 2;
then
(export F1) . a = f1
by A3, A5, CAT_1:5;
hence
t . a = [[((export F1) . a),((export F2) . a)],m]
by A4, A5, A6, CAT_1:5;
verum
end; end;
consider t9 being Function of the carrier of A,(Funcs ( the carrier of B, the carrier' of C)) such that
A7:
for o being set st o in the carrier of A holds
S1[o,t9 . o]
from FUNCT_2:sch 1(A2);
the carrier of [:A,B:] = [: the carrier of A, the carrier of B:]
by CAT_2:23;
then reconsider u9 = uncurry t9 as Function of the carrier of [:A,B:], the carrier' of C ;
A8:
the carrier of [:A,B:] = [: the carrier of A, the carrier of B:]
by CAT_2:23;
A9:
now let ab be
Object of
[:A,B:];
u9 . ab in Hom ((F1 . ab),(F2 . ab))consider a being
Object of
A,
b being
Object of
B such that A10:
ab = [a,b]
by A8, DOMAIN_1:1;
(
(export F1) . a = F1 ?- a &
(export F2) . a = F2 ?- a )
by Th24;
then
t . a = [[(F1 ?- a),(F2 ?- a)],(t9 . a)]
by A7;
then
[[(F1 ?- a),(F2 ?- a)],(t9 . a)] in the
carrier' of
(Functors (B,C))
;
then
[[(F1 ?- a),(F2 ?- a)],(t9 . a)] in NatTrans (
B,
C)
by NATTRA_1:def 17;
then consider G1,
G2 being
Functor of
B,
C,
t99 being
natural_transformation of
G1,
G2 such that A11:
[[(F1 ?- a),(F2 ?- a)],(t9 . a)] = [[G1,G2],t99]
and A12:
G1 is_naturally_transformable_to G2
by NATTRA_1:def 15;
A13:
G1 is_transformable_to G2
by A12, NATTRA_1:def 7;
A14:
[(F1 ?- a),(F2 ?- a)] = [G1,G2]
by A11, ZFMISC_1:27;
A15:
F1 . [a,b] =
(F1 ?- a) . b
by Th12
.=
G1 . b
by A14, ZFMISC_1:27
;
A16:
Hom (
(G1 . b),
(G2 . b))
<> {}
by A12, ISOCAT_1:25;
A17:
F2 . [a,b] =
(F2 ?- a) . b
by Th12
.=
G2 . b
by A14, ZFMISC_1:27
;
u9 . (
a,
b) =
(t9 . a) . b
by Th2
.=
t99 . b
by A11, ZFMISC_1:27
.=
t99 . b
by A13, NATTRA_1:def 5
;
hence
u9 . ab in Hom (
(F1 . ab),
(F2 . ab))
by A10, A15, A17, A16, CAT_1:def 4;
verum end;
A18:
F1 is_transformable_to F2
u9 is transformation of F1,F2
then reconsider u = u9 as transformation of F1,F2 ;
A19:
now
the
carrier' of
[:A,B:] = [: the carrier' of A, the carrier' of B:]
by CAT_2:23;
then reconsider FF1 =
F1,
FF2 =
F2 as
Function of
[: the carrier' of A, the carrier' of B:], the
carrier' of
C ;
let ab1,
ab2 be
Object of
[:A,B:];
( Hom (ab1,ab2) <> {} implies for f being Morphism of ab1,ab2 holds (u . ab2) * (F1 . f) = (F2 . f) * (u . ab1) )assume A20:
Hom (
ab1,
ab2)
<> {}
;
for f being Morphism of ab1,ab2 holds (u . ab2) * (F1 . f) = (F2 . f) * (u . ab1)A21:
Hom (
(F2 . ab1),
(F2 . ab2))
<> {}
by A20, CAT_1:84;
consider a2 being
Object of
A,
b2 being
Object of
B such that A22:
ab2 = [a2,b2]
by A8, DOMAIN_1:1;
(
(export F1) . a2 = F1 ?- a2 &
(export F2) . a2 = F2 ?- a2 )
by Th24;
then
t . a2 = [[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)]
by A7;
then
[[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] in the
carrier' of
(Functors (B,C))
;
then
[[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] in NatTrans (
B,
C)
by NATTRA_1:def 17;
then consider G2,
H2 being
Functor of
B,
C,
t2 being
natural_transformation of
G2,
H2 such that A23:
[[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] = [[G2,H2],t2]
and A24:
G2 is_naturally_transformable_to H2
by NATTRA_1:def 15;
A25:
(
t9 . a2 = t2 &
G2 is_transformable_to H2 )
by A23, A24, NATTRA_1:def 7, ZFMISC_1:27;
consider a1 being
Object of
A,
b1 being
Object of
B such that A26:
ab1 = [a1,b1]
by A8, DOMAIN_1:1;
(
(export F1) . a1 = F1 ?- a1 &
(export F2) . a1 = F2 ?- a1 )
by Th24;
then
t . a1 = [[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)]
by A7;
then
[[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] in the
carrier' of
(Functors (B,C))
;
then
[[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] in NatTrans (
B,
C)
by NATTRA_1:def 17;
then consider G1,
H1 being
Functor of
B,
C,
t1 being
natural_transformation of
G1,
H1 such that A27:
[[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] = [[G1,H1],t1]
and A28:
G1 is_naturally_transformable_to H1
by NATTRA_1:def 15;
A29:
(
t9 . a1 = t1 &
G1 is_transformable_to H1 )
by A27, A28, NATTRA_1:def 7, ZFMISC_1:27;
A30:
u . ab1 =
u9 . (
a1,
b1)
by A18, A26, NATTRA_1:def 5
.=
(t9 . a1) . b1
by Th2
.=
t1 . b1
by A29, NATTRA_1:def 5
;
A31:
Hom (
(G1 . b2),
(H1 . b2))
<> {}
by A28, ISOCAT_1:25;
A32:
Hom (
(F1 . ab1),
(F1 . ab2))
<> {}
by A20, CAT_1:84;
A33:
Hom (
(F1 . ab2),
(F2 . ab2))
<> {}
by A18, NATTRA_1:def 2;
(
(export F2) . a1 = F2 ?- a1 &
(export F1) . a1 = F1 ?- a1 )
by Th24;
then A34:
t . a1 = [[G1,H1],t1]
by A7, A27;
A35:
Hom (
(G1 . b1),
(H1 . b1))
<> {}
by A28, ISOCAT_1:25;
(
(export F1) . a2 = F1 ?- a2 &
(export F2) . a2 = F2 ?- a2 )
by Th24;
then A36:
t . a2 = [[G2,H2],t2]
by A7, A23;
A37:
Hom (
((export F1) . a2),
((export F2) . a2))
<> {}
by A1, ISOCAT_1:25;
A38:
Hom (
((export F1) . a1),
((export F2) . a1))
<> {}
by A1, ISOCAT_1:25;
let f be
Morphism of
ab1,
ab2;
(u . ab2) * (F1 . f) = (F2 . f) * (u . ab1)
the
carrier' of
[:A,B:] = [: the carrier' of A, the carrier' of B:]
by CAT_2:23;
then consider g being
Morphism of
A,
h being
Morphism of
B such that A39:
f = [g,h]
by DOMAIN_1:1;
reconsider g =
g as
Morphism of
a1,
a2 by A20, A26, A22, A39, Th14;
A40:
curry (
F2,
g)
= (curry FF2) . g
;
A41:
Hom (
a1,
a2)
<> {}
by A20, A26, A22, Th13;
then A42:
(
dom g = a1 &
cod g = a2 )
by CAT_1:5;
reconsider h =
h as
Morphism of
b1,
b2 by A20, A26, A22, A39, Th14;
reconsider g9 =
g as
Morphism of
A ;
reconsider h9 =
h as
Morphism of
B ;
reconsider f9 =
f as
Morphism of
[:A,B:] ;
A43:
dom (id b2) = b2
by CAT_1:19;
Hom (
a1,
a1)
<> {}
by CAT_1:27;
then A44:
g9 * (id a1) =
g * (id a1)
by A41, CAT_1:def 10
.=
g
by A41, CAT_1:29
;
A45:
dom g = a1
by A41, CAT_1:5;
A46:
Hom (
((export F2) . a1),
((export F2) . a2))
<> {}
by A41, CAT_1:84;
reconsider e1 =
(export F1) . g,
e2 =
(export F2) . g as
Morphism of
(Functors (B,C)) ;
A47:
curry (
F1,
g)
= (curry FF1) . g
;
A48:
Hom (
(F1 . ab1),
(F2 . ab1))
<> {}
by A18, NATTRA_1:def 2;
A49:
Hom (
b1,
b2)
<> {}
by A20, A26, A22, Th13;
then A50:
Hom (
(G1 . b1),
(G1 . b2))
<> {}
by CAT_1:84;
A51:
[(F1 ?- a1),(F2 ?- a1)] = [G1,H1]
by A27, ZFMISC_1:27;
then A52:
F2 ?- a1 = H1
by ZFMISC_1:27;
then A53:
H1 . h =
(F2 ?- a1) . h
by A49, NATTRA_1:def 1
.=
F2 . (
(id a1),
h)
by CAT_2:36
;
A54:
[(F1 ?- a2),(F2 ?- a2)] = [G2,H2]
by A23, ZFMISC_1:27;
then A55:
F2 ?- a2 = H2
by ZFMISC_1:27;
then A56:
Hom (
(H1 . b2),
(H2 . b2))
<> {}
by A52, A42, Th18, ISOCAT_1:25;
A57:
F1 ?- a2 = G2
by A54, ZFMISC_1:27;
then reconsider v1 =
F1 ?- g as
natural_transformation of
G1,
G2 by A51, A42, ZFMISC_1:27;
A58:
Hom (
((export F1) . a1),
((export F1) . a2))
<> {}
by A41, CAT_1:84;
(
cod (id a1) = a1 &
cod h = b2 )
by A49, CAT_1:5, CAT_1:19;
then A59:
cod [(id a1),h] =
[a1,b2]
by CAT_2:28
.=
dom [g,(id b2)]
by A45, A43, CAT_2:28
;
reconsider v2 =
F2 ?- g as
natural_transformation of
H1,
H2 by A51, A55, A42, ZFMISC_1:27;
A60:
(export F2) . g9 = [[H1,H2],v2]
by A52, A55, A42, Def4;
A61:
H1 is_naturally_transformable_to H2
by A52, A55, A42, Th18;
then
H1 is_transformable_to H2
by NATTRA_1:def 7;
then A62:
v2 . b2 =
((curry (F2,g)) * the Id of B) . b2
by NATTRA_1:def 5
.=
(curry (F2,g)) . ( the Id of B . b2)
by FUNCT_2:15
.=
F2 . (
g,
(id b2))
by A40, CAT_2:3
;
A63:
F1 ?- a1 = G1
by A51, ZFMISC_1:27;
then A64:
G1 . h =
(F1 ?- a1) . h
by A49, NATTRA_1:def 1
.=
F1 . (
(id a1),
h)
by CAT_2:36
;
(export F1) . g9 = [[G1,G2],v1]
by A63, A57, A42, Def4;
then [[G1,H2],(t2 `*` v1)] =
(t . a2) * ((export F1) . g9)
by A36, NATTRA_1:36
.=
(t . a2) * e1
by A41, NATTRA_1:def 1
.=
(t . a2) * ((export F1) . g)
by A58, A37, CAT_1:def 10
.=
((export F2) . g) * (t . a1)
by A1, A41, NATTRA_1:def 8
.=
e2 * (t . a1)
by A46, A38, CAT_1:def 10
.=
((export F2) . g9) * (t . a1)
by A41, NATTRA_1:def 1
.=
[[G1,H2],(v2 `*` t1)]
by A60, A34, NATTRA_1:36
;
then A65:
t2 `*` v1 = v2 `*` t1
by ZFMISC_1:27;
A66:
G1 is_naturally_transformable_to G2
by A63, A57, A42, Th18;
then
G1 is_transformable_to G2
by NATTRA_1:def 7;
then A67:
v1 . b2 =
((curry (F1,g)) * the Id of B) . b2
by NATTRA_1:def 5
.=
(curry (F1,g)) . ( the Id of B . b2)
by FUNCT_2:15
.=
F1 . (
g,
(id b2))
by A47, CAT_2:3
;
A68:
u . ab2 =
u9 . (
a2,
b2)
by A18, A22, NATTRA_1:def 5
.=
(t9 . a2) . b2
by Th2
.=
t2 . b2
by A25, NATTRA_1:def 5
;
A69:
Hom (
(G2 . b2),
(H2 . b2))
<> {}
by A24, ISOCAT_1:25;
Hom (
b2,
b2)
<> {}
by CAT_1:27;
then (id b2) * h9 =
(id b2) * h
by A49, CAT_1:def 10
.=
h
by A49, CAT_1:28
;
then A70:
f = [g,(id b2)] * [(id a1),h]
by A39, A44, A59, CAT_2:30;
A71:
Hom (
(H1 . b1),
(H1 . b2))
<> {}
by A49, CAT_1:84;
then A72:
Hom (
(H1 . b1),
(H2 . b2))
<> {}
by A56, CAT_1:24;
A73:
F2 . f =
F2 . f9
by A20, NATTRA_1:def 1
.=
(v2 . b2) * (H1 . h)
by A59, A70, A62, A53, CAT_1:64
.=
(v2 . b2) * (H1 . h)
by A56, A71, CAT_1:def 10
;
A74:
Hom (
(G1 . b2),
(G2 . b2))
<> {}
by A63, A57, A42, Th18, ISOCAT_1:25;
then A75:
Hom (
(G1 . b1),
(G2 . b2))
<> {}
by A50, CAT_1:24;
F1 . f =
F1 . f9
by A20, NATTRA_1:def 1
.=
(v1 . b2) * (G1 . h)
by A59, A70, A67, A64, CAT_1:64
.=
(v1 . b2) * (G1 . h)
by A74, A50, CAT_1:def 10
;
hence (u . ab2) * (F1 . f) =
(t2 . b2) * ((v1 . b2) * (G1 . h))
by A32, A33, A68, CAT_1:def 10
.=
(t2 . b2) * ((v1 . b2) * (G1 . h))
by A69, A75, CAT_1:def 10
.=
((t2 . b2) * (v1 . b2)) * (G1 . h)
by A69, A74, A50, CAT_1:25
.=
((v2 `*` t1) . b2) * (G1 . h)
by A24, A66, A65, NATTRA_1:25
.=
((v2 . b2) * (t1 . b2)) * (G1 . h)
by A28, A61, NATTRA_1:25
.=
(v2 . b2) * ((t1 . b2) * (G1 . h))
by A50, A56, A31, CAT_1:25
.=
(v2 . b2) * ((H1 . h) * (t1 . b1))
by A28, A49, NATTRA_1:def 8
.=
((v2 . b2) * (H1 . h)) * (t1 . b1)
by A56, A71, A35, CAT_1:25
.=
(F2 . f) * (u . ab1)
by A35, A72, A30, A73, CAT_1:def 10
.=
(F2 . f) * (u . ab1)
by A48, A21, CAT_1:def 10
;
verum
hence A76:
F1 is_naturally_transformable_to F2
by A18, NATTRA_1:def 7; ex u being natural_transformation of F1,F2 st t = export u
then reconsider u = u as natural_transformation of F1,F2 by A19, NATTRA_1:def 8;
take
u
; t = export u
now let s be
Function of
[: the carrier of A, the carrier of B:], the
carrier' of
C;
( u = s implies for a being Object of A holds t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )assume A77:
u = s
;
for a being Object of A holds t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]let a be
Object of
A;
t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
t9 = curry u9
by Th1;
hence
t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
by A7, A77;
verum end;
hence
t = export u
by A76, Def5; verum