defpred S1[ set , set ] means for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st $1 = [[F1,F2],t] holds
$2 = t . a;
A1:
the carrier' of (Functors (A,B)) = NatTrans (A,B)
by NATTRA_1:def 17;
A2:
now let x be
Element of
NatTrans (
A,
B);
ex b being Morphism of B st S1[x,b]consider F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F1,
F2 such that A3:
x = [[F1,F2],t]
and
F1 is_naturally_transformable_to F2
by NATTRA_1:def 16;
reconsider b =
t . a as
Morphism of
B ;
take b =
b;
S1[x,b]thus
S1[
x,
b]
verumproof
let F19,
F29 be
Functor of
A,
B;
for t being natural_transformation of F19,F29 st x = [[F19,F29],t] holds
b = t . alet t9 be
natural_transformation of
F19,
F29;
( x = [[F19,F29],t9] implies b = t9 . a )
assume A4:
x = [[F19,F29],t9]
;
b = t9 . a
then
[F1,F2] = [F19,F29]
by A3, ZFMISC_1:27;
then
(
F1 = F19 &
F2 = F29 )
by ZFMISC_1:27;
hence
b = t9 . a
by A3, A4, ZFMISC_1:27;
verum
end; end;
consider f being Function of (NatTrans (A,B)), the carrier' of B such that
A5:
for x being Element of NatTrans (A,B) holds S1[x,f . x]
from FUNCT_2:sch 3(A2);
A6:
the carrier' of (Functors (A,B)) = NatTrans (A,B)
by NATTRA_1:def 17;
A7:
now let c be
Object of
(Functors (A,B));
ex d being Element of the carrier of B st f . ( the Id of (Functors (A,B)) . c) = the Id of B . dreconsider F =
c as
Functor of
A,
B by Th8;
take d =
F . a;
f . ( the Id of (Functors (A,B)) . c) = the Id of B . dA8:
[[F,F],(id F)] is
Morphism of
(Functors (A,B))
by A6, NATTRA_1:def 16;
thus f . ( the Id of (Functors (A,B)) . c) =
f . (id c)
.=
f . [[F,F],(id F)]
by NATTRA_1:def 17
.=
(id F) . a
by A5, A6, A8
.=
id d
by NATTRA_1:20
.=
the
Id of
B . d
;
verum end;
A9:
now let m1,
m2 be
Morphism of
(Functors (A,B));
( [m2,m1] in dom the Comp of (Functors (A,B)) implies f . ( the Comp of (Functors (A,B)) . (m2,m1)) = the Comp of B . ((f . m2),(f . m1)) )assume A10:
[m2,m1] in dom the
Comp of
(Functors (A,B))
;
f . ( the Comp of (Functors (A,B)) . (m2,m1)) = the Comp of B . ((f . m2),(f . m1))reconsider m19 =
m1,
m29 =
m2 as
Element of
NatTrans (
A,
B)
by NATTRA_1:def 17;
consider F,
F1 being
Functor of
A,
B,
t being
natural_transformation of
F,
F1 such that A11:
F is_naturally_transformable_to F1
and
dom m1 = F
and
cod m1 = F1
and A12:
m1 = [[F,F1],t]
by Th9;
A13:
Hom (
(F . a),
(F1 . a))
<> {}
by A11, ISOCAT_1:25;
A14:
f . m19 = t . a
by A5, A12;
then A15:
cod (f . m19) = F1 . a
by A13, CAT_1:5;
consider F19,
F2 being
Functor of
A,
B,
t9 being
natural_transformation of
F19,
F2 such that A16:
F19 is_naturally_transformable_to F2
and
dom m2 = F19
and
cod m2 = F2
and A17:
m2 = [[F19,F2],t9]
by Th9;
A18:
F19 =
dom m2
by A17, NATTRA_1:33
.=
cod m1
by A10, CAT_1:15
.=
F1
by A12, NATTRA_1:33
;
then reconsider t9 =
t9 as
natural_transformation of
F1,
F2 ;
A19:
Hom (
(F1 . a),
(F2 . a))
<> {}
by A16, A18, ISOCAT_1:25;
A20:
f . m29 = t9 . a
by A5, A17, A18;
then
dom (f . m29) = F1 . a
by A19, CAT_1:5;
then A21:
[(f . m2),(f . m1)] in dom the
Comp of
B
by A15, CAT_1:15;
A22:
m2 * m1 = [[F,F2],(t9 `*` t)]
by A12, A17, A18, NATTRA_1:36;
thus f . ( the Comp of (Functors (A,B)) . (m2,m1)) =
f . (m2 * m1)
by A10, CAT_1:def 1
.=
(t9 `*` t) . a
by A5, A6, A22
.=
(t9 . a) * (t . a)
by A11, A16, A18, NATTRA_1:25
.=
(t9 . a) * (t . a)
by A13, A19, CAT_1:def 10
.=
the
Comp of
B . (
(f . m2),
(f . m1))
by A14, A20, A21, CAT_1:def 1
;
verum end;
now let m be
Morphism of
(Functors (A,B));
( f . ( the Id of (Functors (A,B)) . ( the Source of (Functors (A,B)) . m)) = the Id of B . ( the Source of B . (f . m)) & f . ( the Id of (Functors (A,B)) . ( the Target of (Functors (A,B)) . m)) = the Id of B . ( the Target of B . (f . m)) )reconsider m9 =
m as
Element of
NatTrans (
A,
B)
by NATTRA_1:def 17;
consider F,
F1 being
Functor of
A,
B,
t being
natural_transformation of
F,
F1 such that A23:
F is_naturally_transformable_to F1
and A24:
dom m = F
and A25:
cod m = F1
and A26:
m = [[F,F1],t]
by Th9;
A27:
Hom (
(F . a),
(F1 . a))
<> {}
by A23, ISOCAT_1:25;
A28:
[[F,F],(id F)] is
Morphism of
(Functors (A,B))
by A6, NATTRA_1:def 16;
thus f . ( the Id of (Functors (A,B)) . ( the Source of (Functors (A,B)) . m)) =
f . (id (dom m))
.=
f . [[F,F],(id F)]
by A24, NATTRA_1:def 17
.=
(id F) . a
by A5, A6, A28
.=
id (F . a)
by NATTRA_1:20
.=
id (dom (t . a))
by A27, CAT_1:5
.=
id (dom (f . m9))
by A5, A26
.=
the
Id of
B . ( the Source of B . (f . m))
;
f . ( the Id of (Functors (A,B)) . ( the Target of (Functors (A,B)) . m)) = the Id of B . ( the Target of B . (f . m))A29:
[[F1,F1],(id F1)] is
Morphism of
(Functors (A,B))
by A6, NATTRA_1:def 16;
thus f . ( the Id of (Functors (A,B)) . ( the Target of (Functors (A,B)) . m)) =
f . (id (cod m))
.=
f . [[F1,F1],(id F1)]
by A25, NATTRA_1:def 17
.=
(id F1) . a
by A5, A6, A29
.=
id (F1 . a)
by NATTRA_1:20
.=
id (cod (t . a))
by A27, CAT_1:5
.=
id (cod (f . m9))
by A5, A26
.=
the
Id of
B . ( the Target of B . (f . m))
;
verum end;
then reconsider f = f as Functor of Functors (A,B),B by A6, A7, A9, CAT_1:def 15;
take
f
; for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
f . [[F1,F2],t] = t . a
let F1, F2 be Functor of A,B; for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
f . [[F1,F2],t] = t . a
let t be natural_transformation of F1,F2; ( F1 is_naturally_transformable_to F2 implies f . [[F1,F2],t] = t . a )
assume
F1 is_naturally_transformable_to F2
; f . [[F1,F2],t] = t . a
then
[[F1,F2],t] is Morphism of (Functors (A,B))
by A1, NATTRA_1:32;
hence
f . [[F1,F2],t] = t . a
by A5, A1; verum