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 for x being Element of NatTrans (A,B) ex b being Morphism of B st S1[x,b]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, XTUPLE_0:1;
then
(
F1 = F19 &
F2 = F29 )
by XTUPLE_0:1;
hence
b = t9 . a
by A3, A4, XTUPLE_0:1;
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;
then reconsider ff = f as Function of the carrier' of (Functors (A,B)), the carrier' of B ;
A7:
now for c being Object of (Functors (A,B)) ex d being Element of the carrier of B st f . (id c) = id dlet c be
Object of
(Functors (A,B));
ex d being Element of the carrier of B st f . (id c) = id dreconsider F =
c as
Functor of
A,
B by Th5;
take d =
F . a;
f . (id c) = id dA8:
[[F,F],(id F)] is
Morphism of
(Functors (A,B))
by A6, NATTRA_1:def 16;
thus 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
;
verum end;
A9:
now for m1, m2 being Morphism of (Functors (A,B)) st [m2,m1] in dom the Comp of (Functors (A,B)) holds
ff . (m2 (*) m1) = (ff . m2) (*) (ff . m1)let m1,
m2 be
Morphism of
(Functors (A,B));
( [m2,m1] in dom the Comp of (Functors (A,B)) implies ff . (m2 (*) m1) = (ff . m2) (*) (ff . m1) )assume A10:
[m2,m1] in dom the
Comp of
(Functors (A,B))
;
ff . (m2 (*) m1) = (ff . m2) (*) (ff . 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 Th6;
A13:
Hom (
(F . a),
(F1 . a))
<> {}
by A11, ISOCAT_1:25;
A14:
f . m19 = t . a
by A5, A12;
consider F19,
F2 being
Functor of
A,
B,
t9 being
natural_transformation of
F19,
F2 such that A15:
F19 is_naturally_transformable_to F2
and
dom m2 = F19
and
cod m2 = F2
and A16:
m2 = [[F19,F2],t9]
by Th6;
A17:
F19 =
dom m2
by A16, 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 ;
A18:
Hom (
(F1 . a),
(F2 . a))
<> {}
by A15, A17, ISOCAT_1:25;
A19:
f . m29 = t9 . a
by A5, A16, A17;
A20:
m2 (*) m1 = [[F,F2],(t9 `*` t)]
by A12, A16, A17, NATTRA_1:36;
thus ff . (m2 (*) m1) =
(t9 `*` t) . a
by A5, A6, A20
.=
(t9 . a) * (t . a)
by A11, A15, A17, NATTRA_1:25
.=
(t9 . a) (*) (t . a)
by A13, A18, CAT_1:def 13
.=
(ff . m2) (*) (ff . m1)
by A14, A19
;
verum end;
now for m being Morphism of (Functors (A,B)) holds
( f . (id (dom m)) = id (dom (ff . m)) & f . (id (cod m)) = id (cod (ff . m)) )let m be
Morphism of
(Functors (A,B));
( f . (id (dom m)) = id (dom (ff . m)) & f . (id (cod m)) = id (cod (ff . 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 A21:
F is_naturally_transformable_to F1
and A22:
dom m = F
and A23:
cod m = F1
and A24:
m = [[F,F1],t]
by Th6;
A25:
Hom (
(F . a),
(F1 . a))
<> {}
by A21, ISOCAT_1:25;
A26:
[[F,F],(id F)] is
Morphism of
(Functors (A,B))
by A6, NATTRA_1:def 16;
thus f . (id (dom m)) =
f . [[F,F],(id F)]
by A22, NATTRA_1:def 17
.=
(id F) . a
by A5, A6, A26
.=
id (F . a)
by NATTRA_1:20
.=
id (dom (t . a))
by A25, CAT_1:5
.=
id (dom (f . m9))
by A5, A24
.=
id (dom (ff . m))
;
f . (id (cod m)) = id (cod (ff . m))A27:
[[F1,F1],(id F1)] is
Morphism of
(Functors (A,B))
by A6, NATTRA_1:def 16;
thus f . (id (cod m)) =
f . [[F1,F1],(id F1)]
by A23, NATTRA_1:def 17
.=
(id F1) . a
by A5, A6, A27
.=
id (F1 . a)
by NATTRA_1:20
.=
id (cod (t . a))
by A25, CAT_1:5
.=
id (cod (f . m9))
by A5, A24
.=
id (cod (ff . m))
;
verum end;
then reconsider f = f as Functor of Functors (A,B),B by A7, A9, CAT_1:def 21;
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