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