let A, B, C be Category; :: thesis: for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2
for a being Object of A holds
( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a )
let F1, F2 be Functor of [:A,B:],C; :: thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2
for a being Object of A holds
( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a ) )
assume A1: F1 is_naturally_transformable_to F2 ; :: thesis: for t being natural_transformation of F1,F2
for a being Object of A holds
( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a )
then A2: F1 is_transformable_to F2 ;
let u be natural_transformation of F1,F2; :: thesis: for a being Object of A holds
( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a )
let a be Object of A; :: thesis: ( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a )
reconsider t = u as Function of [: the carrier of A, the carrier of B:], the carrier' of C ;
A3: F1 ?- a is_transformable_to F2 ?- a
proof
let b be Object of B; :: according to NATTRA_1:def 2 :: thesis: not Hom (((F1 ?- a) . b),((F2 ?- a) . b)) = {}
( (F1 ?- a) . b = F1 . [a,b] & (F2 ?- a) . b = F2 . [a,b] ) by Th8;
hence not Hom (((F1 ?- a) . b),((F2 ?- a) . b)) = {} by A2; :: thesis: verum
end;
A4: now :: thesis: for b being Object of B holds ((curry t) . a) . b in Hom (((F1 ?- a) . b),((F2 ?- a) . b))
let b be Object of B; :: thesis: ((curry t) . a) . b in Hom (((F1 ?- a) . b),((F2 ?- a) . b))
A5: ( (F1 ?- a) . b = F1 . [a,b] & (F2 ?- a) . b = F2 . [a,b] ) by Th8;
A6: Hom (((F1 ?- a) . b),((F2 ?- a) . b)) <> {} by A3;
((curry t) . a) . b = t . (a,b) by FUNCT_5:69
.= u . [a,b] by A2, NATTRA_1:def 5 ;
hence ((curry t) . a) . b in Hom (((F1 ?- a) . b),((F2 ?- a) . b)) by A5, A6, CAT_1:def 5; :: thesis: verum
end;
now :: thesis: for b being Object of B holds ((curry t) . a) . b is Morphism of (F1 ?- a) . b,(F2 ?- a) . b
let b be Object of B; :: thesis: ((curry t) . a) . b is Morphism of (F1 ?- a) . b,(F2 ?- a) . b
((curry t) . a) . b in Hom (((F1 ?- a) . b),((F2 ?- a) . b)) by A4;
hence ((curry t) . a) . b is Morphism of (F1 ?- a) . b,(F2 ?- a) . b by CAT_1:def 5; :: thesis: verum
end;
then reconsider s = (curry t) . a as transformation of F1 ?- a,F2 ?- a by A3, NATTRA_1:def 3;
A7: now :: thesis: for b1, b2 being Object of B st Hom (b1,b2) <> {} holds
for f being Morphism of b1,b2 holds (s . b2) * ((F1 ?- a) /. f) = ((F2 ?- a) /. f) * (s . b1)
let b1, b2 be Object of B; :: thesis: ( Hom (b1,b2) <> {} implies for f being Morphism of b1,b2 holds (s . b2) * ((F1 ?- a) /. f) = ((F2 ?- a) /. f) * (s . b1) )
assume A8: Hom (b1,b2) <> {} ; :: thesis: for f being Morphism of b1,b2 holds (s . b2) * ((F1 ?- a) /. f) = ((F2 ?- a) /. f) * (s . b1)
A9: Hom (((F1 ?- a) . b1),((F1 ?- a) . b2)) <> {} by A8, CAT_1:84;
let f be Morphism of b1,b2; :: thesis: (s . b2) * ((F1 ?- a) /. f) = ((F2 ?- a) /. f) * (s . b1)
A10: Hom (a,a) <> {} ;
then reconsider g = [(id a),f] as Morphism of [a,b1],[a,b2] by A8, CAT_2:33;
A11: Hom ([a,b1],[a,b2]) <> {} by A8, A10, Th9;
then A12: Hom ((F1 . [a,b1]),(F1 . [a,b2])) <> {} by CAT_1:84;
A13: s . b1 = ((curry t) . a) . b1 by A3, NATTRA_1:def 5
.= t . (a,b1) by FUNCT_5:69
.= u . [a,b1] by A2, NATTRA_1:def 5 ;
A14: Hom ((F1 . [a,b2]),(F2 . [a,b2])) <> {} by A2;
A15: Hom (((F2 ?- a) . b1),((F2 ?- a) . b2)) <> {} by A8, CAT_1:84;
A16: ( (F1 ?- a) . b1 = F1 . [a,b1] & (F2 ?- a) . b1 = F2 . [a,b1] ) by Th8;
A17: ( (F1 ?- a) . b2 = F1 . [a,b2] & (F2 ?- a) . b2 = F2 . [a,b2] ) by Th8;
A18: Hom ((F1 . [a,b1]),(F2 . [a,b1])) <> {} by A2;
A19: Hom ((F2 . [a,b1]),(F2 . [a,b2])) <> {} by A11, CAT_1:84;
s . b2 = ((curry t) . a) . b2 by A3, NATTRA_1:def 5
.= t . (a,b2) by FUNCT_5:69
.= u . [a,b2] by A2, NATTRA_1:def 5 ;
hence (s . b2) * ((F1 ?- a) /. f) = (u . [a,b2]) (*) ((F1 ?- a) /. f) by A14, A9, A17, CAT_1:def 13
.= (u . [a,b2]) (*) ((F1 ?- a) . f) by A8, CAT_3:def 10
.= (u . [a,b2]) (*) (F1 . ((id a),f)) by CAT_2:36
.= (u . [a,b2]) (*) (F1 /. g) by A11, CAT_3:def 10
.= (u . [a,b2]) * (F1 /. g) by A12, A14, CAT_1:def 13
.= (F2 /. g) * (u . [a,b1]) by A1, A11, NATTRA_1:def 8
.= (F2 /. g) (*) (u . [a,b1]) by A18, A19, CAT_1:def 13
.= (F2 . ((id a),f)) (*) (u . [a,b1]) by A11, CAT_3:def 10
.= ((F2 ?- a) . f) (*) (u . [a,b1]) by CAT_2:36
.= ((F2 ?- a) /. f) (*) (s . b1) by A8, A13, CAT_3:def 10
.= ((F2 ?- a) /. f) * (s . b1) by A18, A15, A16, CAT_1:def 13 ;
:: thesis: verum
end;
hence F1 ?- a is_naturally_transformable_to F2 ?- a by A3; :: thesis: (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a
hence (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a by A7, NATTRA_1:def 8; :: thesis: verum