let A, B, C be Category; for F being Functor of [:A,B:],C
for g, f being Morphism of A st dom g = cod f holds
for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g (*) f) = (F ?- g) `*` t
let F be Functor of [:A,B:],C; for g, f being Morphism of A st dom g = cod f holds
for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g (*) f) = (F ?- g) `*` t
let g, f be Morphism of A; ( dom g = cod f implies for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g (*) f) = (F ?- g) `*` t )
assume A1:
dom g = cod f
; for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g (*) f) = (F ?- g) `*` t
A2:
F ?- (dom f) is_naturally_transformable_to F ?- (dom g)
by A1, Th14;
then A3:
F ?- (dom f) is_transformable_to F ?- (dom g)
;
reconsider G = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ;
reconsider Fgf = (curry G) . (g (*) f), Ff = (curry G) . f, Fg = (curry G) . g as Function of the carrier' of B, the carrier' of C ;
let t be natural_transformation of F ?- (dom f),F ?- (dom g); ( t = F ?- f implies F ?- (g (*) f) = (F ?- g) `*` t )
assume A4:
t = F ?- f
; F ?- (g (*) f) = (F ?- g) `*` t
reconsider s = t as transformation of F ?- (dom f),F ?- (dom g) ;
A5:
F ?- (dom g) is_naturally_transformable_to F ?- (cod g)
by Th14;
then A6:
F ?- (dom g) is_transformable_to F ?- (cod g)
;
F ?- (dom (g (*) f)) is_naturally_transformable_to F ?- (cod (g (*) f))
by Th14;
then A7:
F ?- (dom (g (*) f)) is_transformable_to F ?- (cod (g (*) f))
;
A8:
now for b being Object of B holds (F ?- (g (*) f)) . b = ((F ?- g) `*` s) . blet b be
Object of
B;
(F ?- (g (*) f)) . b = ((F ?- g) `*` s) . bA9:
Hom (
b,
b)
<> {}
;
A10:
id b = (IdMap B) . b
by ISOCAT_1:def 12;
A11:
(F ?- g) . b =
((curry (F,g)) * (IdMap B)) . b
by A6, NATTRA_1:def 5
.=
Fg . (id b)
by A10, FUNCT_2:15
.=
F . (
g,
(id b))
by FUNCT_5:69
;
dom (id b) =
b
.=
cod (id b)
;
then A12:
dom [g,(id b)] =
[(cod f),(cod (id b))]
by A1, CAT_2:28
.=
cod [f,(id b)]
by CAT_2:28
;
A13:
(
Hom (
((F ?- (dom g)) . b),
((F ?- (cod g)) . b))
<> {} &
Hom (
((F ?- (dom f)) . b),
((F ?- (dom g)) . b))
<> {} )
by A3, A6;
A14:
(F ?- f) . b =
((curry (F,f)) * (IdMap B)) . b
by A1, A3, NATTRA_1:def 5
.=
Ff . (id b)
by A10, FUNCT_2:15
.=
F . (
f,
(id b))
by FUNCT_5:69
;
thus (F ?- (g (*) f)) . b =
((curry (F,(g (*) f))) * (IdMap B)) . b
by A7, NATTRA_1:def 5
.=
Fgf . (id b)
by A10, FUNCT_2:15
.=
F . (
(g (*) f),
(id b))
by FUNCT_5:69
.=
F . [(g (*) f),((id b) * (id b))]
.=
F . [(g (*) f),((id b) (*) (id b))]
by A9, CAT_1:def 13
.=
F . ([g,(id b)] (*) [f,(id b)])
by A12, CAT_2:30
.=
((F ?- g) . b) (*) (s . b)
by A1, A4, A11, A14, A12, CAT_1:64
.=
((F ?- g) . b) * (s . b)
by A13, CAT_1:def 13
.=
((F ?- g) `*` s) . b
by A3, A6, NATTRA_1:def 6
;
verum end;
( cod (g (*) f) = cod g & dom (g (*) f) = dom f )
by A1, CAT_1:17;
then
F ?- (g (*) f) = (F ?- g) `*` s
by A3, A6, A8, NATTRA_1:18, NATTRA_1:19;
hence
F ?- (g (*) f) = (F ?- g) `*` t
by A2, A5, NATTRA_1:def 9; verum