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 18;
A2:
now let x be
Element of
NatTrans A,
B;
:: thesis: 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;
:: thesis: S1[x,b]thus
S1[
x,
b]
:: thesis: verumproof
let F1',
F2' be
Functor of
A,
B;
:: thesis: for t being natural_transformation of F1',F2' st x = [[F1',F2'],t] holds
b = t . alet t' be
natural_transformation of
F1',
F2';
:: thesis: ( x = [[F1',F2'],t'] implies b = t' . a )
assume A4:
x = [[F1',F2'],t']
;
:: thesis: b = t' . a
then
[F1,F2] = [F1',F2']
by A3, ZFMISC_1:33;
then
(
F1 = F1' &
F2 = F2' )
by ZFMISC_1:33;
hence
b = t' . a
by A3, A4, ZFMISC_1:33;
:: thesis: 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 18;
A7:
now let c be
Object of
(Functors A,B);
:: thesis: 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;
:: thesis: 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 18
.=
(id F) . a
by A5, A6, A8
.=
id d
by NATTRA_1:21
.=
the
Id of
B . d
;
:: thesis: verum end;
A9:
now let m1,
m2 be
Morphism of
(Functors A,B);
:: thesis: ( [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)
;
:: thesis: f . (the Comp of (Functors A,B) . m2,m1) = the Comp of B . (f . m2),(f . m1)reconsider m1' =
m1,
m2' =
m2 as
Element of
NatTrans A,
B by NATTRA_1:def 18;
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:30;
A14:
f . m1' = t . a
by A5, A12;
then A15:
cod (f . m1') = F1 . a
by A13, CAT_1:23;
consider F1',
F2 being
Functor of
A,
B,
t' being
natural_transformation of
F1',
F2 such that A16:
F1' is_naturally_transformable_to F2
and
dom m2 = F1'
and
cod m2 = F2
and A17:
m2 = [[F1',F2],t']
by Th9;
A18:
F1' =
dom m2
by A17, NATTRA_1:39
.=
cod m1
by A10, CAT_1:40
.=
F1
by A12, NATTRA_1:39
;
then reconsider t' =
t' as
natural_transformation of
F1,
F2 ;
A19:
Hom (F1 . a),
(F2 . a) <> {}
by A16, A18, ISOCAT_1:30;
A20:
f . m2' = t' . a
by A5, A17, A18;
then
dom (f . m2') = F1 . a
by A19, CAT_1:23;
then A21:
[(f . m2),(f . m1)] in dom the
Comp of
B
by A15, CAT_1:40;
A22:
m2 * m1 = [[F,F2],(t' `*` t)]
by A12, A17, A18, NATTRA_1:42;
thus f . (the Comp of (Functors A,B) . m2,m1) =
f . (m2 * m1)
by A10, CAT_1:def 4
.=
(t' `*` t) . a
by A5, A6, A22
.=
(t' . a) * (t . a)
by A11, A16, A18, NATTRA_1:27
.=
(t' . a) * (t . a)
by A13, A19, CAT_1:def 13
.=
the
Comp of
B . (f . m2),
(f . m1)
by A14, A20, A21, CAT_1:def 4
;
:: thesis: verum end;
now let m be
Morphism of
(Functors A,B);
:: thesis: ( 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 m' =
m as
Element of
NatTrans A,
B by NATTRA_1:def 18;
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:30;
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 18
.=
(id F) . a
by A5, A6, A28
.=
id (F . a)
by NATTRA_1:21
.=
id (dom (t . a))
by A27, CAT_1:23
.=
id (dom (f . m'))
by A5, A26
.=
the
Id of
B . (the Source of B . (f . m))
;
:: thesis: 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 18
.=
(id F1) . a
by A5, A6, A29
.=
id (F1 . a)
by NATTRA_1:21
.=
id (cod (t . a))
by A27, CAT_1:23
.=
id (cod (f . m'))
by A5, A26
.=
the
Id of
B . (the Target of B . (f . m))
;
:: thesis: verum end;
then reconsider f = f as Functor of Functors A,B,B by A6, A7, A9, CAT_1:def 18;
take
f
; :: thesis: 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; :: thesis: 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; :: thesis: ( F1 is_naturally_transformable_to F2 implies f . [[F1,F2],t] = t . a )
assume
F1 is_naturally_transformable_to F2
; :: thesis: f . [[F1,F2],t] = t . a
then
[[F1,F2],t] is Morphism of (Functors A,B)
by A1, NATTRA_1:35;
hence
f . [[F1,F2],t] = t . a
by A5, A1; :: thesis: verum