defpred S1[ set , set ] means for F1, F2 being Functor of [:A,B:],C
for t being natural_transformation of F1,F2 st $1 = [[F1,F2],t] holds
$2 = [[(export F1),(export F2)],(export t)];
A1:
now let o be
set ;
:: thesis: ( o in the carrier' of (Functors [:A,B:],C) implies ex m being set st
( m in the carrier' of (Functors A,(Functors B,C)) & S1[o,m] ) )assume
o in the
carrier' of
(Functors [:A,B:],C)
;
:: thesis: ex m being set st
( m in the carrier' of (Functors A,(Functors B,C)) & S1[o,m] )then
o in NatTrans [:A,B:],
C
by NATTRA_1:def 18;
then consider F1,
F2 being
Functor of
[:A,B:],
C,
t being
natural_transformation of
F1,
F2 such that A2:
o = [[F1,F2],t]
and A3:
F1 is_naturally_transformable_to F2
by NATTRA_1:def 16;
take m =
[[(export F1),(export F2)],(export t)];
:: thesis: ( m in the carrier' of (Functors A,(Functors B,C)) & S1[o,m] )
export F1 is_naturally_transformable_to export F2
by A3, Th27;
then
m in NatTrans A,
(Functors B,C)
by NATTRA_1:def 16;
hence
m in the
carrier' of
(Functors A,(Functors B,C))
by NATTRA_1:def 18;
:: thesis: S1[o,m]thus
S1[
o,
m]
:: thesis: verumproof
let F1',
F2' be
Functor of
[:A,B:],
C;
:: thesis: for t being natural_transformation of F1',F2' st o = [[F1',F2'],t] holds
m = [[(export F1'),(export F2')],(export t)]let t' be
natural_transformation of
F1',
F2';
:: thesis: ( o = [[F1',F2'],t'] implies m = [[(export F1'),(export F2')],(export t')] )
assume A4:
o = [[F1',F2'],t']
;
:: thesis: m = [[(export F1'),(export F2')],(export t')]
then
(
[F1,F2] = [F1',F2'] &
t = t' )
by A2, ZFMISC_1:33;
then
(
F1 = F1' &
F2 = F2' )
by ZFMISC_1:33;
hence
m = [[(export F1'),(export F2')],(export t')]
by A2, A4, ZFMISC_1:33;
:: thesis: verum
end; end;
consider FF being Function of the carrier' of (Functors [:A,B:],C),the carrier' of (Functors A,(Functors B,C)) such that
A5:
for o being set st o in the carrier' of (Functors [:A,B:],C) holds
S1[o,FF . o]
from FUNCT_2:sch 1(A1);
FF is Functor of Functors [:A,B:],C, Functors A,(Functors B,C)
proof
thus
for
c being
Object of
(Functors [:A,B:],C) ex
d being
Object of
(Functors A,(Functors B,C)) st
FF . (id c) = id d
:: according to ISOCAT_1:def 1 :: thesis: ( ( for b1 being Element of the carrier' of (Functors [:A,B:],C) holds
( FF . (id (dom b1)) = id (dom (FF . b1)) & FF . (id (cod b1)) = id (cod (FF . b1)) ) ) & ( for b1, b2 being Element of the carrier' of (Functors [:A,B:],C) holds
( not dom b2 = cod b1 or FF . (b2 * b1) = (FF . b2) * (FF . b1) ) ) )proof
let c be
Object of
(Functors [:A,B:],C);
:: thesis: ex d being Object of (Functors A,(Functors B,C)) st FF . (id c) = id d
reconsider F =
c as
Functor of
[:A,B:],
C by Th8;
A6:
id c = [[F,F],(id F)]
by NATTRA_1:def 18;
reconsider d =
export F as
Object of
(Functors A,(Functors B,C)) by Th8;
take
d
;
:: thesis: FF . (id c) = id d
A7:
id (export F) = export (id F)
by Th28;
thus FF . (id c) =
[[(export F),(export F)],(export (id F))]
by A5, A6
.=
id d
by A7, NATTRA_1:def 18
;
:: thesis: verum
end;
thus
for
f being
Morphism of
(Functors [:A,B:],C) holds
(
FF . (id (dom f)) = id (dom (FF . f)) &
FF . (id (cod f)) = id (cod (FF . f)) )
:: thesis: for b1, b2 being Element of the carrier' of (Functors [:A,B:],C) holds
( not dom b2 = cod b1 or FF . (b2 * b1) = (FF . b2) * (FF . b1) )proof
let f be
Morphism of
(Functors [:A,B:],C);
:: thesis: ( FF . (id (dom f)) = id (dom (FF . f)) & FF . (id (cod f)) = id (cod (FF . f)) )
consider F1,
F2 being
Functor of
[:A,B:],
C,
t being
natural_transformation of
F1,
F2 such that
F1 is_naturally_transformable_to F2
and A8:
(
dom f = F1 &
cod f = F2 &
f = [[F1,F2],t] )
by Th9;
A9:
id (dom f) = [[F1,F1],(id F1)]
by A8, NATTRA_1:def 18;
A10:
FF . f = [[(export F1),(export F2)],(export t)]
by A5, A8;
then A11:
dom (FF . f) = export F1
by NATTRA_1:39;
thus FF . (id (dom f)) =
[[(export F1),(export F1)],(export (id F1))]
by A5, A9
.=
[[(export F1),(export F1)],(id (export F1))]
by Th28
.=
id (dom (FF . f))
by A11, NATTRA_1:def 18
;
:: thesis: FF . (id (cod f)) = id (cod (FF . f))
A12:
id (cod f) = [[F2,F2],(id F2)]
by A8, NATTRA_1:def 18;
A13:
cod (FF . f) = export F2
by A10, NATTRA_1:39;
thus FF . (id (cod f)) =
[[(export F2),(export F2)],(export (id F2))]
by A5, A12
.=
[[(export F2),(export F2)],(id (export F2))]
by Th28
.=
id (cod (FF . f))
by A13, NATTRA_1:def 18
;
:: thesis: verum
end;
let f,
g be
Morphism of
(Functors [:A,B:],C);
:: thesis: ( not dom g = cod f or FF . (g * f) = (FF . g) * (FF . f) )
consider F1,
F2 being
Functor of
[:A,B:],
C,
t being
natural_transformation of
F1,
F2 such that A14:
F1 is_naturally_transformable_to F2
and A15:
(
dom f = F1 &
cod f = F2 &
f = [[F1,F2],t] )
by Th9;
A16:
FF . f = [[(export F1),(export F2)],(export t)]
by A5, A15;
consider G1,
G2 being
Functor of
[:A,B:],
C,
u being
natural_transformation of
G1,
G2 such that A17:
G1 is_naturally_transformable_to G2
and A18:
(
dom g = G1 &
cod g = G2 &
g = [[G1,G2],u] )
by Th9;
assume A19:
dom g = cod f
;
:: thesis: FF . (g * f) = (FF . g) * (FF . f)
then reconsider u =
u as
natural_transformation of
F2,
G2 by A15, A18;
g * f = [[F1,G2],(u `*` t)]
by A15, A18, A19, NATTRA_1:42;
then A20:
FF . (g * f) = [[(export F1),(export G2)],(export (u `*` t))]
by A5;
A21:
FF . g = [[(export F2),(export G2)],(export u)]
by A5, A15, A18, A19;
(export u) `*` (export t) = export (u `*` t)
by A14, A15, A17, A18, A19, Th29;
hence
FF . (g * f) = (FF . g) * (FF . f)
by A16, A20, A21, NATTRA_1:42;
:: thesis: verum
end;
then reconsider FF = FF as Functor of Functors [:A,B:],C, Functors A,(Functors B,C) ;
take
FF
; :: 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 holds FF . [[F1,F2],t] = [[(export F1),(export F2)],(export t)]
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 holds FF . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] )
assume A22:
F1 is_naturally_transformable_to F2
; :: thesis: for t being natural_transformation of F1,F2 holds FF . [[F1,F2],t] = [[(export F1),(export F2)],(export t)]
let t be natural_transformation of F1,F2; :: thesis: FF . [[F1,F2],t] = [[(export F1),(export F2)],(export t)]
[[F1,F2],t] in NatTrans [:A,B:],C
by A22, NATTRA_1:35;
then
[[F1,F2],t] in the carrier' of (Functors [:A,B:],C)
by NATTRA_1:def 18;
hence
FF . [[F1,F2],t] = [[(export F1),(export F2)],(export t)]
by A5; :: thesis: verum