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 :: thesis: 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 ; :: thesis: ( 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)) ; :: thesis: 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; :: thesis: ( 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; :: thesis: S1[o,m]
thus S1[o,m] :: thesis: verum
proof
let F19, F29 be Functor of [:A,B:],C; :: thesis: 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; :: thesis: ( o = [[F19,F29],t9] implies m = [[(export F19),(export F29)],(export t9)] )
assume A4: o = [[F19,F29],t9] ; :: thesis: 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; :: 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 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 :: 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 Th5;
reconsider d = export F as Object of (Functors (A,(Functors (B,C)))) by Th5;
take d ; :: thesis: 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 ;
:: 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
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 ;
:: thesis: 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 ;
:: 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
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 ; :: thesis: 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; :: 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: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; :: thesis: verum