defpred S1[ object , object ] 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 for o being object st o in the carrier' of (Functors ([:A,B:],C)) holds
ex m being object st
( m in the carrier' of (Functors (A,(Functors (B,C)))) & S1[o,m] )let o be
object ;
( o in the carrier' of (Functors ([:A,B:],C)) implies ex m being object st
( m in the carrier' of (Functors (A,(Functors (B,C)))) & S1[o,m] ) )assume
o in the
carrier' of
(Functors ([:A,B:],C))
;
ex m being object 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 17;
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;
reconsider m =
[[(export F1),(export F2)],(export t)] as
object ;
take m =
m;
( m in the carrier' of (Functors (A,(Functors (B,C)))) & S1[o,m] )
export F1 is_naturally_transformable_to export F2
by A3, Th21;
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 17;
S1[o,m]thus
S1[
o,
m]
verumproof
let F19,
F29 be
Functor of
[:A,B:],
C;
for t being natural_transformation of F19,F29 st o = [[F19,F29],t] holds
m = [[(export F19),(export F29)],(export t)]let t9 be
natural_transformation of
F19,
F29;
( o = [[F19,F29],t9] implies m = [[(export F19),(export F29)],(export t9)] )
assume A4:
o = [[F19,F29],t9]
;
m = [[(export F19),(export F29)],(export t9)]
then
[F1,F2] = [F19,F29]
by A2, XTUPLE_0:1;
then
(
F1 = F19 &
F2 = F29 )
by XTUPLE_0:1;
hence
m = [[(export F19),(export F29)],(export t9)]
by A2, A4, XTUPLE_0:1;
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 object 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
ISOCAT_1:def 1 ( ( 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));
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 Th5;
reconsider d =
export F as
Object of
(Functors (A,(Functors (B,C)))) by Th5;
take
d
;
FF . (id c) = id d
A6:
id (export F) = export (id F)
by Th22;
id c = [[F,F],(id F)]
by NATTRA_1:def 17;
hence FF . (id c) =
[[(export F),(export F)],(export (id F))]
by A5
.=
id d
by A6, NATTRA_1:def 17
;
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)) )
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));
( 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 A7:
dom f = F1
and A8:
cod f = F2
and A9:
f = [[F1,F2],t]
by Th6;
A10:
FF . f = [[(export F1),(export F2)],(export t)]
by A5, A9;
then A11:
dom (FF . f) = export F1
by NATTRA_1:33;
id (dom f) = [[F1,F1],(id F1)]
by A7, NATTRA_1:def 17;
hence FF . (id (dom f)) =
[[(export F1),(export F1)],(export (id F1))]
by A5
.=
[[(export F1),(export F1)],(id (export F1))]
by Th22
.=
id (dom (FF . f))
by A11, NATTRA_1:def 17
;
FF . (id (cod f)) = id (cod (FF . f))
A12:
cod (FF . f) = export F2
by A10, NATTRA_1:33;
id (cod f) = [[F2,F2],(id F2)]
by A8, NATTRA_1:def 17;
hence FF . (id (cod f)) =
[[(export F2),(export F2)],(export (id F2))]
by A5
.=
[[(export F2),(export F2)],(id (export F2))]
by Th22
.=
id (cod (FF . f))
by A12, NATTRA_1:def 17
;
verum
end;
let f,
g be
Morphism of
(Functors ([:A,B:],C));
( 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 A13:
F1 is_naturally_transformable_to F2
and
dom f = F1
and A14:
cod f = F2
and A15:
f = [[F1,F2],t]
by Th6;
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
and
cod g = G2
and A19:
g = [[G1,G2],u]
by Th6;
assume A20:
dom g = cod f
;
FF . (g (*) f) = (FF . g) (*) (FF . f)
then reconsider u =
u as
natural_transformation of
F2,
G2 by A14, A18;
g (*) f = [[F1,G2],(u `*` t)]
by A14, A15, A18, A19, A20, NATTRA_1:36;
then A21:
FF . (g (*) f) = [[(export F1),(export G2)],(export (u `*` t))]
by A5;
(
FF . g = [[(export F2),(export G2)],(export u)] &
(export u) `*` (export t) = export (u `*` t) )
by A5, A13, A14, A17, A18, A19, A20, Th23;
hence
FF . (g (*) f) = (FF . g) (*) (FF . f)
by A16, A21, NATTRA_1:36;
verum
end;
then reconsider FF = FF as Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) ;
take
FF
; 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; ( 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
; 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; FF . [[F1,F2],t] = [[(export F1),(export F2)],(export t)]
[[F1,F2],t] in NatTrans ([:A,B:],C)
by A22, NATTRA_1:32;
then
[[F1,F2],t] in the carrier' of (Functors ([:A,B:],C))
by NATTRA_1:def 17;
hence
FF . [[F1,F2],t] = [[(export F1),(export F2)],(export t)]
by A5; verum