let A, B, C be Category; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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:11; :: thesis: S1[o,m]
thus S1[o,m] :: thesis: verum
proof
let a be Object of A; :: thesis: ( o = a implies t . a = [[((export F1) . a),((export F2) . a)],m] )
assume A5: o = a ; :: thesis: 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:23;
hence t . a = [[((export F1) . a),((export F2) . a)],m] by A4, A5, A6, CAT_1:23; :: thesis: 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:33;
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:33;
A9: now
let ab be Object of [:A,B:]; :: thesis: 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:9;
( (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 18;
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:33;
A15: F1 . [a,b] = (F1 ?- a) . b by Th12
.= G1 . b by A14, ZFMISC_1:33 ;
A16: Hom (G1 . b),(G2 . b) <> {} by A12, ISOCAT_1:30;
A17: F2 . [a,b] = (F2 ?- a) . b by Th12
.= G2 . b by A14, ZFMISC_1:33 ;
u9 . a,b = (t9 . a) . b by Th2
.= t99 . b by A11, ZFMISC_1:33
.= 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 7; :: thesis: verum
end;
A18: F1 is_transformable_to F2
proof
let a be Object of [:A,B:]; :: according to NATTRA_1:def 2 :: thesis: not Hom (F1 . a),(F2 . a) = {}
thus not Hom (F1 . a),(F2 . a) = {} by A9; :: thesis: verum
end;
u9 is transformation of F1,F2
proof
thus F1 is_transformable_to F2 by A18; :: according to NATTRA_1:def 3 :: thesis: for b1 being Element of the carrier of [:A,B:] holds u9 . b1 is Morphism of F1 . b1,F2 . b1
let a be Object of [:A,B:]; :: thesis: u9 . a is Morphism of F1 . a,F2 . a
u9 . a in Hom (F1 . a),(F2 . a) by A9;
hence u9 . a is Morphism of F1 . a,F2 . a by CAT_1:def 7; :: thesis: verum
end;
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:33;
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:]; :: thesis: ( 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 <> {} ; :: thesis: 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:126;
consider a2 being Object of A, b2 being Object of B such that
A22: ab2 = [a2,b2] by A8, DOMAIN_1:9;
( (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 18;
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:33;
consider a1 being Object of A, b1 being Object of B such that
A26: ab1 = [a1,b1] by A8, DOMAIN_1:9;
( (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 18;
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:33;
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:30;
A32: Hom (F1 . ab1),(F1 . ab2) <> {} by A20, CAT_1:126;
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:30;
( (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:30;
A38: Hom ((export F1) . a1),((export F2) . a1) <> {} by A1, ISOCAT_1:30;
let f be Morphism of ab1,ab2; :: thesis: (u . ab2) * (F1 . f) = (F2 . f) * (u . ab1)
the carrier' of [:A,B:] = [:the carrier' of A,the carrier' of B:] by CAT_2:33;
then consider g being Morphism of A, h being Morphism of B such that
A39: f = [g,h] by DOMAIN_1:9;
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:23;
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:44;
Hom a1,a1 <> {} by CAT_1:56;
then A44: g9 * (id a1) = g * (id a1) by A41, CAT_1:def 13
.= g by A41, CAT_1:58 ;
A45: dom g = a1 by A41, CAT_1:23;
A46: Hom ((export F2) . a1),((export F2) . a2) <> {} by A41, CAT_1:126;
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:126;
A51: [(F1 ?- a1),(F2 ?- a1)] = [G1,H1] by A27, ZFMISC_1:33;
then A52: F2 ?- a1 = H1 by ZFMISC_1:33;
then A53: H1 . h = (F2 ?- a1) . h by A49, NATTRA_1:def 1
.= F2 . (id a1),h by CAT_2:47 ;
A54: [(F1 ?- a2),(F2 ?- a2)] = [G2,H2] by A23, ZFMISC_1:33;
then A55: F2 ?- a2 = H2 by ZFMISC_1:33;
then A56: Hom (H1 . b2),(H2 . b2) <> {} by A52, A42, Th18, ISOCAT_1:30;
A57: F1 ?- a2 = G2 by A54, ZFMISC_1:33;
then reconsider v1 = F1 ?- g as natural_transformation of G1,G2 by A51, A42, ZFMISC_1:33;
A58: Hom ((export F1) . a1),((export F1) . a2) <> {} by A41, CAT_1:126;
( cod (id a1) = a1 & cod h = b2 ) by A49, CAT_1:23, CAT_1:44;
then A59: cod [(id a1),h] = [a1,b2] by CAT_2:38
.= dom [g,(id b2)] by A45, A43, CAT_2:38 ;
reconsider v2 = F2 ?- g as natural_transformation of H1,H2 by A51, A55, A42, ZFMISC_1:33;
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:21
.= F2 . g,(id b2) by A40, CAT_2:3 ;
A63: F1 ?- a1 = G1 by A51, ZFMISC_1:33;
then A64: G1 . h = (F1 ?- a1) . h by A49, NATTRA_1:def 1
.= F1 . (id a1),h by CAT_2:47 ;
(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:42
.= (t . a2) * e1 by A41, NATTRA_1:def 1
.= (t . a2) * ((export F1) . g) by A58, A37, CAT_1:def 13
.= ((export F2) . g) * (t . a1) by A1, A41, NATTRA_1:def 8
.= e2 * (t . a1) by A46, A38, CAT_1:def 13
.= ((export F2) . g9) * (t . a1) by A41, NATTRA_1:def 1
.= [[G1,H2],(v2 `*` t1)] by A60, A34, NATTRA_1:42 ;
then A65: t2 `*` v1 = v2 `*` t1 by ZFMISC_1:33;
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:21
.= 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:30;
Hom b2,b2 <> {} by CAT_1:56;
then (id b2) * h9 = (id b2) * h by A49, CAT_1:def 13
.= h by A49, CAT_1:57 ;
then A70: f = [g,(id b2)] * [(id a1),h] by A39, A44, A59, CAT_2:40;
A71: Hom (H1 . b1),(H1 . b2) <> {} by A49, CAT_1:126;
then A72: Hom (H1 . b1),(H2 . b2) <> {} by A56, CAT_1:52;
A73: F2 . f = F2 . f9 by A20, NATTRA_1:def 1
.= (v2 . b2) * (H1 . h) by A59, A70, A62, A53, CAT_1:99
.= (v2 . b2) * (H1 . h) by A56, A71, CAT_1:def 13 ;
A74: Hom (G1 . b2),(G2 . b2) <> {} by A63, A57, A42, Th18, ISOCAT_1:30;
then A75: Hom (G1 . b1),(G2 . b2) <> {} by A50, CAT_1:52;
F1 . f = F1 . f9 by A20, NATTRA_1:def 1
.= (v1 . b2) * (G1 . h) by A59, A70, A67, A64, CAT_1:99
.= (v1 . b2) * (G1 . h) by A74, A50, CAT_1:def 13 ;
hence (u . ab2) * (F1 . f) = (t2 . b2) * ((v1 . b2) * (G1 . h)) by A32, A33, A68, CAT_1:def 13
.= (t2 . b2) * ((v1 . b2) * (G1 . h)) by A69, A75, CAT_1:def 13
.= ((t2 . b2) * (v1 . b2)) * (G1 . h) by A69, A74, A50, CAT_1:54
.= ((v2 `*` t1) . b2) * (G1 . h) by A24, A66, A65, NATTRA_1:27
.= ((v2 . b2) * (t1 . b2)) * (G1 . h) by A28, A61, NATTRA_1:27
.= (v2 . b2) * ((t1 . b2) * (G1 . h)) by A50, A56, A31, CAT_1:54
.= (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:54
.= (F2 . f) * (u . ab1) by A35, A72, A30, A73, CAT_1:def 13
.= (F2 . f) * (u . ab1) by A48, A21, CAT_1:def 13 ;
:: thesis: verum
end;
hence A76: F1 is_naturally_transformable_to F2 by A18, NATTRA_1:def 7; :: thesis: 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 ; :: thesis: t = export u
now
let s be Function of [:the carrier of A,the carrier of B:],the carrier' of C; :: thesis: ( 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 ; :: thesis: for a being Object of A holds t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
let a be Object of A; :: thesis: 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; :: thesis: verum
end;
hence t = export u by A76, Def5; :: thesis: verum