:: ISOCAT_2 semantic presentation begin definition let A, B, C be non empty set ; let f be Function of A,(Funcs (B,C)); :: original: uncurry redefine func uncurry f -> Function of [:A,B:],C; coherence uncurry f is Function of [:A,B:],C proof A1: rng f c= Funcs (B,C) ; dom (uncurry f) = [:(dom f),B:] by A1, FUNCT_5:26 .= [:A,B:] by FUNCT_2:def_1 ; hence uncurry f is Function of [:A,B:],C ; ::_thesis: verum end; end; theorem Th1: :: ISOCAT_2:1 for A, B, C being non empty set for f being Function of A,(Funcs (B,C)) holds curry (uncurry f) = f proof let A, B, C be non empty set ; ::_thesis: for f being Function of A,(Funcs (B,C)) holds curry (uncurry f) = f let f be Function of A,(Funcs (B,C)); ::_thesis: curry (uncurry f) = f rng f c= Funcs (B,C) ; hence curry (uncurry f) = f by FUNCT_5:48; ::_thesis: verum end; theorem Th2: :: ISOCAT_2:2 for A, B, C being non empty set for f being Function of A,(Funcs (B,C)) for a being Element of A for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b proof let A, B, C be non empty set ; ::_thesis: for f being Function of A,(Funcs (B,C)) for a being Element of A for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b let f be Function of A,(Funcs (B,C)); ::_thesis: for a being Element of A for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b let a be Element of A; ::_thesis: for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b let b be Element of B; ::_thesis: (uncurry f) . (a,b) = (f . a) . b ( dom f = A & dom (f . a) = B ) by FUNCT_2:def_1; hence (uncurry f) . (a,b) = (f . a) . b by FUNCT_5:38; ::_thesis: verum end; theorem :: ISOCAT_2:3 canceled; theorem :: ISOCAT_2:4 canceled; theorem Th5: :: ISOCAT_2:5 for A being Category for f being Morphism of A holds (id (cod f)) (*) f = f proof let A be Category; ::_thesis: for f being Morphism of A holds (id (cod f)) (*) f = f let f be Morphism of A; ::_thesis: (id (cod f)) (*) f = f reconsider f9 = f as Morphism of dom f, cod f by CAT_1:4; A1: Hom ((dom f),(cod f)) <> {} by CAT_1:2; Hom ((cod f),(cod f)) <> {} ; hence (id (cod f)) (*) f = (id (cod f)) * f9 by A1, CAT_1:def_13 .= f by A1, CAT_1:28 ; ::_thesis: verum end; theorem Th6: :: ISOCAT_2:6 for A being Category for f being Morphism of A holds f (*) (id (dom f)) = f proof let A be Category; ::_thesis: for f being Morphism of A holds f (*) (id (dom f)) = f let f be Morphism of A; ::_thesis: f (*) (id (dom f)) = f reconsider f9 = f as Morphism of dom f, cod f by CAT_1:4; A1: Hom ((dom f),(cod f)) <> {} by CAT_1:2; Hom ((dom f),(dom f)) <> {} ; hence f (*) (id (dom f)) = f9 * (id (dom f)) by A1, CAT_1:def_13 .= f by A1, CAT_1:29 ; ::_thesis: verum end; theorem Th7: :: ISOCAT_2:7 for A, B being Category for o being set holds ( o is Object of (Functors (A,B)) iff o is Functor of A,B ) proof let A, B be Category; ::_thesis: for o being set holds ( o is Object of (Functors (A,B)) iff o is Functor of A,B ) let o be set ; ::_thesis: ( o is Object of (Functors (A,B)) iff o is Functor of A,B ) the carrier of (Functors (A,B)) = Funct (A,B) by NATTRA_1:def_17; hence ( o is Object of (Functors (A,B)) iff o is Functor of A,B ) by CAT_2:def_2; ::_thesis: verum end; theorem Th8: :: ISOCAT_2:8 for A, B being Category for f being Morphism of (Functors (A,B)) ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( F1 is_naturally_transformable_to F2 & dom f = F1 & cod f = F2 & f = [[F1,F2],t] ) proof let A, B be Category; ::_thesis: for f being Morphism of (Functors (A,B)) ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( F1 is_naturally_transformable_to F2 & dom f = F1 & cod f = F2 & f = [[F1,F2],t] ) let m be Morphism of (Functors (A,B)); ::_thesis: ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( F1 is_naturally_transformable_to F2 & dom m = F1 & cod m = F2 & m = [[F1,F2],t] ) ( Hom ((dom m),(cod m)) <> {} & m is Morphism of dom m, cod m ) by CAT_1:2, CAT_1:4; then consider F, F1 being Functor of A,B, t being natural_transformation of F,F1 such that A1: ( dom m = F & cod m = F1 ) and A2: m = [[F,F1],t] by NATTRA_1:34; take F ; ::_thesis: ex F2 being Functor of A,B ex t being natural_transformation of F,F2 st ( F is_naturally_transformable_to F2 & dom m = F & cod m = F2 & m = [[F,F2],t] ) take F1 ; ::_thesis: ex t being natural_transformation of F,F1 st ( F is_naturally_transformable_to F1 & dom m = F & cod m = F1 & m = [[F,F1],t] ) take t ; ::_thesis: ( F is_naturally_transformable_to F1 & dom m = F & cod m = F1 & m = [[F,F1],t] ) the carrier' of (Functors (A,B)) = NatTrans (A,B) by NATTRA_1:def_17; hence F is_naturally_transformable_to F1 by A2, NATTRA_1:32; ::_thesis: ( dom m = F & cod m = F1 & m = [[F,F1],t] ) thus ( dom m = F & cod m = F1 & m = [[F,F1],t] ) by A1, A2; ::_thesis: verum end; begin definition let A, B be Category; let a be Object of A; funca |-> B -> Functor of Functors (A,B),B means :Def1: :: ISOCAT_2:def 1 for F1, F2 being Functor of A,B for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds it . [[F1,F2],t] = t . a; existence ex b1 being Functor of Functors (A,B),B st for F1, F2 being Functor of A,B for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds b1 . [[F1,F2],t] = t . a proof 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__::_thesis:_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); ::_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: verum proof let F19, F29 be Functor of A,B; ::_thesis: for t being natural_transformation of F19,F29 st x = [[F19,F29],t] holds b = t . a let t9 be natural_transformation of F19,F29; ::_thesis: ( x = [[F19,F29],t9] implies b = t9 . a ) assume A4: x = [[F19,F29],t9] ; ::_thesis: 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; ::_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_17; then reconsider ff = f as Function of the carrier' of (Functors (A,B)), the carrier' of B ; A7: now__::_thesis:_for_c_being_Object_of_(Functors_(A,B))_ex_d_being_Element_of_the_carrier_of_B_st_f_._(id_c)_=_id_d let c be Object of (Functors (A,B)); ::_thesis: ex d being Element of the carrier of B st f . (id c) = id d reconsider F = c as Functor of A,B by Th7; take d = F . a; ::_thesis: f . (id c) = id d A8: [[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 ; ::_thesis: verum end; A9: now__::_thesis:_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)); ::_thesis: ( [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)) ; ::_thesis: 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 Th8; 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 Th8; 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 ; ::_thesis: verum end; now__::_thesis:_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)); ::_thesis: ( 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 Th8; 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)) ; ::_thesis: 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)) ; ::_thesis: verum end; then reconsider f = f as Functor of Functors (A,B),B by A7, A9, CAT_1:def_21; 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:32; hence f . [[F1,F2],t] = t . a by A5, A1; ::_thesis: verum end; uniqueness for b1, b2 being Functor of Functors (A,B),B st ( for F1, F2 being Functor of A,B for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds b1 . [[F1,F2],t] = t . a ) & ( for F1, F2 being Functor of A,B for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds b2 . [[F1,F2],t] = t . a ) holds b1 = b2 proof let f1, f2 be Functor of Functors (A,B),B; ::_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 f1 . [[F1,F2],t] = t . a ) & ( for F1, F2 being Functor of A,B for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds f2 . [[F1,F2],t] = t . a ) implies f1 = f2 ) assume that A28: for F1, F2 being Functor of A,B for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds f1 . [[F1,F2],t] = t . a and A29: for F1, F2 being Functor of A,B for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds f2 . [[F1,F2],t] = t . a ; ::_thesis: f1 = f2 now__::_thesis:_for_c_being_Morphism_of_(Functors_(A,B))_holds_f1_._c_=_f2_._c let c be Morphism of (Functors (A,B)); ::_thesis: f1 . c = f2 . c the carrier' of (Functors (A,B)) = NatTrans (A,B) by NATTRA_1:def_17; then consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that A30: ( c = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) by NATTRA_1:def_15; thus f1 . c = t . a by A28, A30 .= f2 . c by A29, A30 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines |-> ISOCAT_2:def_1_:_ for A, B being Category for a being Object of A for b4 being Functor of Functors (A,B),B holds ( b4 = a |-> B iff for F1, F2 being Functor of A,B for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds b4 . [[F1,F2],t] = t . a ); theorem :: ISOCAT_2:9 for A being Category for o, m being set holds Functors ((1Cat (o,m)),A) ~= A proof let A be Category; ::_thesis: for o, m being set holds Functors ((1Cat (o,m)),A) ~= A let o, m be set ; ::_thesis: Functors ((1Cat (o,m)),A) ~= A reconsider a = o as Object of (1Cat (o,m)) by TARSKI:def_1; take F = a |-> A; :: according to ISOCAT_1:def_4 ::_thesis: F is isomorphic now__::_thesis:_for_x,_y_being_set_st_x_in_the_carrier'_of_(Functors_((1Cat_(o,m)),A))_&_y_in_the_carrier'_of_(Functors_((1Cat_(o,m)),A))_&_F_._x_=_F_._y_holds_ x_=_y let x, y be set ; ::_thesis: ( x in the carrier' of (Functors ((1Cat (o,m)),A)) & y in the carrier' of (Functors ((1Cat (o,m)),A)) & F . x = F . y implies x = y ) A1: the carrier' of (Functors ((1Cat (o,m)),A)) = NatTrans ((1Cat (o,m)),A) by NATTRA_1:def_17; assume x in the carrier' of (Functors ((1Cat (o,m)),A)) ; ::_thesis: ( y in the carrier' of (Functors ((1Cat (o,m)),A)) & F . x = F . y implies x = y ) then consider F1, F2 being Functor of 1Cat (o,m),A, t being natural_transformation of F1,F2 such that A2: x = [[F1,F2],t] and A3: F1 is_naturally_transformable_to F2 by A1, NATTRA_1:def_16; assume y in the carrier' of (Functors ((1Cat (o,m)),A)) ; ::_thesis: ( F . x = F . y implies x = y ) then consider F19, F29 being Functor of 1Cat (o,m),A, t9 being natural_transformation of F19,F29 such that A4: y = [[F19,F29],t9] and A5: F19 is_naturally_transformable_to F29 by A1, NATTRA_1:def_16; assume F . x = F . y ; ::_thesis: x = y then A6: t . a = F . y by A2, A3, Def1 .= t9 . a by A4, A5, Def1 ; reconsider G1 = F1, G19 = F19, G2 = F2, G29 = F29 as Function of {m}, the carrier' of A ; reconsider s = t, s9 = t9 as Function of {a}, the carrier' of A ; A7: id a = m by TARSKI:def_1; A8: F1 is_transformable_to F2 by A3, NATTRA_1:def_7; then A9: Hom ((F1 . a),(F2 . a)) <> {} by NATTRA_1:def_2; A10: F19 is_transformable_to F29 by A5, NATTRA_1:def_7; then A11: Hom ((F19 . a),(F29 . a)) <> {} by NATTRA_1:def_2; then F1 . a = F19 . a by A6, A9, CAT_1:6; then G1 . (id a) = id (F19 . a) by CAT_1:71 .= G19 . (id a) by CAT_1:71 ; then A12: F1 = F19 by A7, FUNCT_2:125; F2 . a = F29 . a by A6, A9, A11, CAT_1:6; then G2 . (id a) = id (F29 . a) by CAT_1:71 .= G29 . (id a) by CAT_1:71 ; then A13: F2 = F29 by A7, FUNCT_2:125; s . a = t9 . a by A8, A6, NATTRA_1:def_5 .= s9 . a by A10, NATTRA_1:def_5 ; hence x = y by A2, A4, A12, A13, FUNCT_2:125; ::_thesis: verum end; hence F is one-to-one by FUNCT_2:19; :: according to ISOCAT_1:def_3 ::_thesis: rng F = the carrier' of A thus rng F c= the carrier' of A ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier' of A c= rng F let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of A or x in rng F ) assume x in the carrier' of A ; ::_thesis: x in rng F then reconsider f = x as Morphism of A ; reconsider F1 = {m} --> (id (dom f)), F2 = {m} --> (id (cod f)) as Function of the carrier' of (1Cat (o,m)), the carrier' of A ; A14: now__::_thesis:_for_g_being_Morphism_of_(1Cat_(o,m))_holds_ (_F1_._(id_(dom_g))_=_id_(dom_(F1_._g))_&_F1_._(id_(cod_g))_=_id_(cod_(F1_._g))_) let g be Morphism of (1Cat (o,m)); ::_thesis: ( F1 . (id (dom g)) = id (dom (F1 . g)) & F1 . (id (cod g)) = id (cod (F1 . g)) ) thus F1 . (id (dom g)) = id (dom f) by FUNCOP_1:7 .= id (dom (id (dom f))) .= id (dom (F1 . g)) by FUNCOP_1:7 ; ::_thesis: F1 . (id (cod g)) = id (cod (F1 . g)) thus F1 . (id (cod g)) = id (dom f) by FUNCOP_1:7 .= id (cod (id (dom f))) .= id (cod (F1 . g)) by FUNCOP_1:7 ; ::_thesis: verum end; A15: now__::_thesis:_for_h,_g_being_Morphism_of_(1Cat_(o,m))_st_dom_g_=_cod_h_holds_ F1_._(g_(*)_h)_=_(F1_._g)_(*)_(F1_._h) let h, g be Morphism of (1Cat (o,m)); ::_thesis: ( dom g = cod h implies F1 . (g (*) h) = (F1 . g) (*) (F1 . h) ) assume dom g = cod h ; ::_thesis: F1 . (g (*) h) = (F1 . g) (*) (F1 . h) A16: Hom ((dom f),(dom f)) <> {} ; thus F1 . (g (*) h) = id (dom f) by FUNCOP_1:7 .= (id (dom f)) * (id (dom f)) .= (id (dom f)) (*) (id (dom f)) by A16, CAT_1:def_13 .= (id (dom f)) (*) (F1 . h) by FUNCOP_1:7 .= (F1 . g) (*) (F1 . h) by FUNCOP_1:7 ; ::_thesis: verum end; A17: now__::_thesis:_for_h,_g_being_Morphism_of_(1Cat_(o,m))_st_dom_g_=_cod_h_holds_ F2_._(g_(*)_h)_=_(F2_._g)_(*)_(F2_._h) let h, g be Morphism of (1Cat (o,m)); ::_thesis: ( dom g = cod h implies F2 . (g (*) h) = (F2 . g) (*) (F2 . h) ) assume dom g = cod h ; ::_thesis: F2 . (g (*) h) = (F2 . g) (*) (F2 . h) A18: Hom ((cod f),(cod f)) <> {} ; thus F2 . (g (*) h) = id (cod f) by FUNCOP_1:7 .= (id (cod f)) * (id (cod f)) .= (id (cod f)) (*) (id (cod f)) by A18, CAT_1:def_13 .= (id (cod f)) (*) (F2 . h) by FUNCOP_1:7 .= (F2 . g) (*) (F2 . h) by FUNCOP_1:7 ; ::_thesis: verum end; A19: now__::_thesis:_for_g_being_Morphism_of_(1Cat_(o,m))_holds_ (_F2_._(id_(dom_g))_=_id_(dom_(F2_._g))_&_F2_._(id_(cod_g))_=_id_(cod_(F2_._g))_) let g be Morphism of (1Cat (o,m)); ::_thesis: ( F2 . (id (dom g)) = id (dom (F2 . g)) & F2 . (id (cod g)) = id (cod (F2 . g)) ) thus F2 . (id (dom g)) = id (cod f) by FUNCOP_1:7 .= id (dom (id (cod f))) .= id (dom (F2 . g)) by FUNCOP_1:7 ; ::_thesis: F2 . (id (cod g)) = id (cod (F2 . g)) thus F2 . (id (cod g)) = id (cod f) by FUNCOP_1:7 .= id (cod (id (cod f))) .= id (cod (F2 . g)) by FUNCOP_1:7 ; ::_thesis: verum end; ( ( for c being Object of (1Cat (o,m)) ex d being Object of A st F1 . (id c) = id d ) & ( for c being Object of (1Cat (o,m)) ex d being Object of A st F2 . (id c) = id d ) ) by FUNCOP_1:7; then reconsider F1 = F1, F2 = F2 as Functor of 1Cat (o,m),A by A14, A15, A19, A17, CAT_1:61; reconsider t = {a} --> f as Function of the carrier of (1Cat (o,m)), the carrier' of A ; A20: for b being Object of (1Cat (o,m)) holds ( F1 . b = dom f & F2 . b = cod f ) proof let b be Object of (1Cat (o,m)); ::_thesis: ( F1 . b = dom f & F2 . b = cod f ) F2 . (id b) = id (cod f) by FUNCOP_1:7; then A21: id (F2 . b) = id (cod f) by CAT_1:71; F1 . (id b) = id (dom f) by FUNCOP_1:7; then id (F1 . b) = id (dom f) by CAT_1:71; hence ( F1 . b = dom f & F2 . b = cod f ) by A21, CAT_1:59; ::_thesis: verum end; A22: now__::_thesis:_for_b_being_Object_of_(1Cat_(o,m))_holds_t_._b_is_Morphism_of_F1_._b,F2_._b let b be Object of (1Cat (o,m)); ::_thesis: t . b is Morphism of F1 . b,F2 . b A23: F2 . b = cod f by A20; ( t . b = f & F1 . b = dom f ) by A20, FUNCOP_1:7; then t . b in Hom ((F1 . b),(F2 . b)) by A23; hence t . b is Morphism of F1 . b,F2 . b by CAT_1:def_5; ::_thesis: verum end; A24: now__::_thesis:_for_b_being_Object_of_(1Cat_(o,m))_holds_Hom_((F1_._b),(F2_._b))_<>_{} let b be Object of (1Cat (o,m)); ::_thesis: Hom ((F1 . b),(F2 . b)) <> {} ( F1 . b = dom f & F2 . b = cod f ) by A20; hence Hom ((F1 . b),(F2 . b)) <> {} by CAT_1:2; ::_thesis: verum end; then A25: F1 is_transformable_to F2 by NATTRA_1:def_2; then reconsider t = t as transformation of F1,F2 by A22, NATTRA_1:def_3; A26: for b being Object of (1Cat (o,m)) holds t . b = f proof let b be Object of (1Cat (o,m)); ::_thesis: t . b = f thus f = ({a} --> f) . b by FUNCOP_1:7 .= t . b by A25, NATTRA_1:def_5 ; ::_thesis: verum end; A27: now__::_thesis:_for_b1,_b2_being_Object_of_(1Cat_(o,m))_st_Hom_(b1,b2)_<>_{}_holds_ for_g_being_Morphism_of_b1,b2_holds_(t_._b2)_*_(F1_/._g)_=_(F2_/._g)_*_(t_._b1) let b1, b2 be Object of (1Cat (o,m)); ::_thesis: ( Hom (b1,b2) <> {} implies for g being Morphism of b1,b2 holds (t . b2) * (F1 /. g) = (F2 /. g) * (t . b1) ) assume A28: Hom (b1,b2) <> {} ; ::_thesis: for g being Morphism of b1,b2 holds (t . b2) * (F1 /. g) = (F2 /. g) * (t . b1) A29: Hom ((F2 . b1),(F2 . b2)) <> {} by A28, CAT_1:82; let g be Morphism of b1,b2; ::_thesis: (t . b2) * (F1 /. g) = (F2 /. g) * (t . b1) A30: ( t . b1 = f & Hom ((F1 . b1),(F2 . b1)) <> {} ) by A24, A26; A31: Hom ((F1 . b1),(F1 . b2)) <> {} by A28, CAT_1:82; A32: m in {m} by TARSKI:def_1; A33: g = m by TARSKI:def_1; then A34: F2 /. g = F2 . m by A28, CAT_3:def_10 .= id (cod f) by A32, FUNCOP_1:7 ; A35: F1 /. g = F1 . m by A28, A33, CAT_3:def_10 .= id (dom f) by A32, FUNCOP_1:7 ; ( t . b2 = f & Hom ((F1 . b2),(F2 . b2)) <> {} ) by A24, A26; hence (t . b2) * (F1 /. g) = f (*) (F1 /. g) by A31, CAT_1:def_13 .= f by A35, CAT_1:22 .= (F2 /. g) (*) f by A34, CAT_1:21 .= (F2 /. g) * (t . b1) by A30, A29, CAT_1:def_13 ; ::_thesis: verum end; F1 is_transformable_to F2 by A24, NATTRA_1:def_2; then A36: F1 is_naturally_transformable_to F2 by A27, NATTRA_1:def_7; then reconsider t = t as natural_transformation of F1,F2 by A27, NATTRA_1:def_8; [[F1,F2],t] in NatTrans ((1Cat (o,m)),A) by A36, NATTRA_1:def_16; then A37: [[F1,F2],t] in the carrier' of (Functors ((1Cat (o,m)),A)) by NATTRA_1:def_17; F . [[F1,F2],t] = t . a by A36, Def1 .= f by A26 ; hence x in rng F by A37, FUNCT_2:4; ::_thesis: verum end; begin theorem Th10: :: ISOCAT_2:10 for A, B, C being Category for F being Functor of [:A,B:],C for a being Object of A for b being Object of B holds (F ?- a) . b = F . [a,b] proof let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C for a being Object of A for b being Object of B holds (F ?- a) . b = F . [a,b] let F be Functor of [:A,B:],C; ::_thesis: for a being Object of A for b being Object of B holds (F ?- a) . b = F . [a,b] let a be Object of A; ::_thesis: for b being Object of B holds (F ?- a) . b = F . [a,b] let b be Object of B; ::_thesis: (F ?- a) . b = F . [a,b] thus (F ?- a) . b = (Obj F) . (a,b) by CAT_2:37 .= F . [a,b] ; ::_thesis: verum end; theorem Th11: :: ISOCAT_2:11 for A, B being Category for a1, a2 being Object of A for b1, b2 being Object of B holds ( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} ) proof let A, B be Category; ::_thesis: for a1, a2 being Object of A for b1, b2 being Object of B holds ( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} ) let a1, a2 be Object of A; ::_thesis: for b1, b2 being Object of B holds ( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} ) let b1, b2 be Object of B; ::_thesis: ( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} ) Hom ([a1,b1],[a2,b2]) = [:(Hom (a1,a2)),(Hom (b1,b2)):] by CAT_2:32; hence ( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} ) by ZFMISC_1:90; ::_thesis: verum end; theorem Th12: :: ISOCAT_2:12 for A, B being Category for a1, a2 being Object of A for b1, b2 being Object of B st Hom ([a1,b1],[a2,b2]) <> {} holds for f being Morphism of A for g being Morphism of B holds ( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) ) proof let A, B be Category; ::_thesis: for a1, a2 being Object of A for b1, b2 being Object of B st Hom ([a1,b1],[a2,b2]) <> {} holds for f being Morphism of A for g being Morphism of B holds ( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) ) let a1, a2 be Object of A; ::_thesis: for b1, b2 being Object of B st Hom ([a1,b1],[a2,b2]) <> {} holds for f being Morphism of A for g being Morphism of B holds ( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) ) let b1, b2 be Object of B; ::_thesis: ( Hom ([a1,b1],[a2,b2]) <> {} implies for f being Morphism of A for g being Morphism of B holds ( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) ) ) assume A1: Hom ([a1,b1],[a2,b2]) <> {} ; ::_thesis: for f being Morphism of A for g being Morphism of B holds ( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) ) let f be Morphism of A; ::_thesis: for g being Morphism of B holds ( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) ) let g be Morphism of B; ::_thesis: ( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) ) thus ( [f,g] is Morphism of [a1,b1],[a2,b2] implies ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) ) ::_thesis: ( f is Morphism of a1,a2 & g is Morphism of b1,b2 implies [f,g] is Morphism of [a1,b1],[a2,b2] ) proof assume [f,g] is Morphism of [a1,b1],[a2,b2] ; ::_thesis: ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) then A2: [f,g] in Hom ([a1,b1],[a2,b2]) by A1, CAT_1:def_5; Hom ([a1,b1],[a2,b2]) = [:(Hom (a1,a2)),(Hom (b1,b2)):] by CAT_2:32; then ( f in Hom (a1,a2) & g in Hom (b1,b2) ) by A2, ZFMISC_1:87; hence ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) by CAT_1:def_5; ::_thesis: verum end; ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) by A1, Th11; hence ( f is Morphism of a1,a2 & g is Morphism of b1,b2 implies [f,g] is Morphism of [a1,b1],[a2,b2] ) by CAT_2:33; ::_thesis: verum end; theorem Th13: :: ISOCAT_2:13 for A, B, C being Category 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 for a being Object of A holds ( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a ) proof let A, B, C be Category; ::_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 for a being Object of A holds ( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a ) 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 for a being Object of A holds ( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a ) ) assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2 for a being Object of A holds ( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a ) then A2: F1 is_transformable_to F2 by NATTRA_1:def_7; let u be natural_transformation of F1,F2; ::_thesis: for a being Object of A holds ( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a ) let a be Object of A; ::_thesis: ( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a ) reconsider t = u as Function of [: the carrier of A, the carrier of B:], the carrier' of C ; A3: F1 ?- a is_transformable_to F2 ?- a proof let b be Object of B; :: according to NATTRA_1:def_2 ::_thesis: not Hom (((F1 ?- a) . b),((F2 ?- a) . b)) = {} ( (F1 ?- a) . b = F1 . [a,b] & (F2 ?- a) . b = F2 . [a,b] ) by Th10; hence not Hom (((F1 ?- a) . b),((F2 ?- a) . b)) = {} by A2, NATTRA_1:def_2; ::_thesis: verum end; A4: now__::_thesis:_for_b_being_Object_of_B_holds_((curry_t)_._a)_._b_in_Hom_(((F1_?-_a)_._b),((F2_?-_a)_._b)) let b be Object of B; ::_thesis: ((curry t) . a) . b in Hom (((F1 ?- a) . b),((F2 ?- a) . b)) A5: ( (F1 ?- a) . b = F1 . [a,b] & (F2 ?- a) . b = F2 . [a,b] ) by Th10; A6: Hom (((F1 ?- a) . b),((F2 ?- a) . b)) <> {} by A3, NATTRA_1:def_2; ((curry t) . a) . b = t . (a,b) by FUNCT_5:69 .= u . [a,b] by A2, NATTRA_1:def_5 ; hence ((curry t) . a) . b in Hom (((F1 ?- a) . b),((F2 ?- a) . b)) by A5, A6, CAT_1:def_5; ::_thesis: verum end; now__::_thesis:_for_b_being_Object_of_B_holds_((curry_t)_._a)_._b_is_Morphism_of_(F1_?-_a)_._b,(F2_?-_a)_._b let b be Object of B; ::_thesis: ((curry t) . a) . b is Morphism of (F1 ?- a) . b,(F2 ?- a) . b ((curry t) . a) . b in Hom (((F1 ?- a) . b),((F2 ?- a) . b)) by A4; hence ((curry t) . a) . b is Morphism of (F1 ?- a) . b,(F2 ?- a) . b by CAT_1:def_5; ::_thesis: verum end; then reconsider s = (curry t) . a as transformation of F1 ?- a,F2 ?- a by A3, NATTRA_1:def_3; A7: now__::_thesis:_for_b1,_b2_being_Object_of_B_st_Hom_(b1,b2)_<>_{}_holds_ for_f_being_Morphism_of_b1,b2_holds_(s_._b2)_*_((F1_?-_a)_/._f)_=_((F2_?-_a)_/._f)_*_(s_._b1) let b1, b2 be Object of B; ::_thesis: ( Hom (b1,b2) <> {} implies for f being Morphism of b1,b2 holds (s . b2) * ((F1 ?- a) /. f) = ((F2 ?- a) /. f) * (s . b1) ) assume A8: Hom (b1,b2) <> {} ; ::_thesis: for f being Morphism of b1,b2 holds (s . b2) * ((F1 ?- a) /. f) = ((F2 ?- a) /. f) * (s . b1) A9: Hom (((F1 ?- a) . b1),((F1 ?- a) . b2)) <> {} by A8, CAT_1:84; let f be Morphism of b1,b2; ::_thesis: (s . b2) * ((F1 ?- a) /. f) = ((F2 ?- a) /. f) * (s . b1) A10: Hom (a,a) <> {} ; then reconsider g = [(id a),f] as Morphism of [a,b1],[a,b2] by A8, CAT_2:33; A11: Hom ([a,b1],[a,b2]) <> {} by A8, A10, Th11; then A12: Hom ((F1 . [a,b1]),(F1 . [a,b2])) <> {} by CAT_1:84; A13: s . b1 = ((curry t) . a) . b1 by A3, NATTRA_1:def_5 .= t . (a,b1) by FUNCT_5:69 .= u . [a,b1] by A2, NATTRA_1:def_5 ; A14: Hom ((F1 . [a,b2]),(F2 . [a,b2])) <> {} by A2, NATTRA_1:def_2; A15: Hom (((F2 ?- a) . b1),((F2 ?- a) . b2)) <> {} by A8, CAT_1:84; A16: ( (F1 ?- a) . b1 = F1 . [a,b1] & (F2 ?- a) . b1 = F2 . [a,b1] ) by Th10; A17: ( (F1 ?- a) . b2 = F1 . [a,b2] & (F2 ?- a) . b2 = F2 . [a,b2] ) by Th10; A18: Hom ((F1 . [a,b1]),(F2 . [a,b1])) <> {} by A2, NATTRA_1:def_2; A19: Hom ((F2 . [a,b1]),(F2 . [a,b2])) <> {} by A11, CAT_1:84; s . b2 = ((curry t) . a) . b2 by A3, NATTRA_1:def_5 .= t . (a,b2) by FUNCT_5:69 .= u . [a,b2] by A2, NATTRA_1:def_5 ; hence (s . b2) * ((F1 ?- a) /. f) = (u . [a,b2]) (*) ((F1 ?- a) /. f) by A14, A9, A17, CAT_1:def_13 .= (u . [a,b2]) (*) ((F1 ?- a) . f) by A8, CAT_3:def_10 .= (u . [a,b2]) (*) (F1 . ((id a),f)) by CAT_2:36 .= (u . [a,b2]) (*) (F1 /. g) by A11, CAT_3:def_10 .= (u . [a,b2]) * (F1 /. g) by A12, A14, CAT_1:def_13 .= (F2 /. g) * (u . [a,b1]) by A1, A11, NATTRA_1:def_8 .= (F2 /. g) (*) (u . [a,b1]) by A18, A19, CAT_1:def_13 .= (F2 . ((id a),f)) (*) (u . [a,b1]) by A11, CAT_3:def_10 .= ((F2 ?- a) . f) (*) (u . [a,b1]) by CAT_2:36 .= ((F2 ?- a) /. f) (*) (s . b1) by A8, A13, CAT_3:def_10 .= ((F2 ?- a) /. f) * (s . b1) by A18, A15, A16, CAT_1:def_13 ; ::_thesis: verum end; hence F1 ?- a is_naturally_transformable_to F2 ?- a by A3, NATTRA_1:def_7; ::_thesis: (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a hence (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a by A7, NATTRA_1:def_8; ::_thesis: verum end; definition let A, B, C be Category; let F be Functor of [:A,B:],C; let f be Morphism of A; func curry (F,f) -> Function of the carrier' of B, the carrier' of C equals :: ISOCAT_2:def 2 (curry F) . f; coherence (curry F) . f is Function of the carrier' of B, the carrier' of C proof reconsider F = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ; (curry F) . f is Function of the carrier' of B, the carrier' of C ; hence (curry F) . f is Function of the carrier' of B, the carrier' of C ; ::_thesis: verum end; end; :: deftheorem defines curry ISOCAT_2:def_2_:_ for A, B, C being Category for F being Functor of [:A,B:],C for f being Morphism of A holds curry (F,f) = (curry F) . f; theorem Th14: :: ISOCAT_2:14 for A, B being Category for a1, a2 being Object of A for b1, b2 being Object of B for f being Morphism of A for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds [f,g] in Hom ([a1,b1],[a2,b2]) proof let A, B be Category; ::_thesis: for a1, a2 being Object of A for b1, b2 being Object of B for f being Morphism of A for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds [f,g] in Hom ([a1,b1],[a2,b2]) let a1, a2 be Object of A; ::_thesis: for b1, b2 being Object of B for f being Morphism of A for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds [f,g] in Hom ([a1,b1],[a2,b2]) let b1, b2 be Object of B; ::_thesis: for f being Morphism of A for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds [f,g] in Hom ([a1,b1],[a2,b2]) let f be Morphism of A; ::_thesis: for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds [f,g] in Hom ([a1,b1],[a2,b2]) let g be Morphism of B; ::_thesis: ( f in Hom (a1,a2) & g in Hom (b1,b2) implies [f,g] in Hom ([a1,b1],[a2,b2]) ) assume ( f in Hom (a1,a2) & g in Hom (b1,b2) ) ; ::_thesis: [f,g] in Hom ([a1,b1],[a2,b2]) then [f,g] in [:(Hom (a1,a2)),(Hom (b1,b2)):] by ZFMISC_1:87; hence [f,g] in Hom ([a1,b1],[a2,b2]) by CAT_2:32; ::_thesis: verum end; theorem Th15: :: ISOCAT_2:15 for A, B, C being Category for F being Functor of [:A,B:],C for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ( F ?- a is_naturally_transformable_to F ?- b & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a,F ?- b ) proof let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ( F ?- a is_naturally_transformable_to F ?- b & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a,F ?- b ) let F be Functor of [:A,B:],C; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ( F ?- a is_naturally_transformable_to F ?- b & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a,F ?- b ) let a1, a2 be Object of A; ::_thesis: ( Hom (a1,a2) <> {} implies for f being Morphism of a1,a2 holds ( F ?- a1 is_naturally_transformable_to F ?- a2 & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2 ) ) assume A1: Hom (a1,a2) <> {} ; ::_thesis: for f being Morphism of a1,a2 holds ( F ?- a1 is_naturally_transformable_to F ?- a2 & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2 ) reconsider G = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ; let f be Morphism of a1,a2; ::_thesis: ( F ?- a1 is_naturally_transformable_to F ?- a2 & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2 ) reconsider Ff = (curry G) . f as Function of the carrier' of B, the carrier' of C ; A2: now__::_thesis:_for_b_being_Object_of_B_holds_((curry_(F,f))_*_(IdMap_B))_._b_in_Hom_(((F_?-_a1)_._b),((F_?-_a2)_._b)) let b be Object of B; ::_thesis: ((curry (F,f)) * (IdMap B)) . b in Hom (((F ?- a1) . b),((F ?- a2) . b)) ( f in Hom (a1,a2) & id b in Hom (b,b) ) by A1, CAT_1:def_5; then [f,(id b)] in Hom ([a1,b],[a2,b]) by Th14; then A3: F . (f,(id b)) in Hom ((F . [a1,b]),(F . [a2,b])) by CAT_1:81; A4: id b = (IdMap B) . b by ISOCAT_1:def_12; ( (F ?- a1) . b = F . [a1,b] & (F ?- a2) . b = F . [a2,b] ) by Th10; then Ff . (id b) in Hom (((F ?- a1) . b),((F ?- a2) . b)) by A3, FUNCT_5:69; hence ((curry (F,f)) * (IdMap B)) . b in Hom (((F ?- a1) . b),((F ?- a2) . b)) by FUNCT_2:15, A4; ::_thesis: verum end; A5: F ?- a1 is_transformable_to F ?- a2 proof let b be Object of B; :: according to NATTRA_1:def_2 ::_thesis: not Hom (((F ?- a1) . b),((F ?- a2) . b)) = {} thus not Hom (((F ?- a1) . b),((F ?- a2) . b)) = {} by A2; ::_thesis: verum end; reconsider FfI = (curry (F,f)) * (IdMap B) as Function of the carrier of B, the carrier' of C ; now__::_thesis:_for_b_being_Object_of_B_holds_FfI_._b_is_Morphism_of_(F_?-_a1)_._b,(F_?-_a2)_._b let b be Object of B; ::_thesis: FfI . b is Morphism of (F ?- a1) . b,(F ?- a2) . b ((curry (F,f)) * (IdMap B)) . b in Hom (((F ?- a1) . b),((F ?- a2) . b)) by A2; hence FfI . b is Morphism of (F ?- a1) . b,(F ?- a2) . b by CAT_1:def_5; ::_thesis: verum end; then reconsider t = (curry (F,f)) * (IdMap B) as transformation of F ?- a1,F ?- a2 by A5, NATTRA_1:def_3; A6: now__::_thesis:_for_b1,_b2_being_Object_of_B_st_Hom_(b1,b2)_<>_{}_holds_ for_g_being_Morphism_of_b1,b2_holds_(t_._b2)_*_((F_?-_a1)_/._g)_=_((F_?-_a2)_/._g)_*_(t_._b1) reconsider ida1 = id a1, ida2 = id a2 as Morphism of A ; A7: Hom (a1,a1) <> {} ; A8: Hom (a2,a2) <> {} ; let b1, b2 be Object of B; ::_thesis: ( Hom (b1,b2) <> {} implies for g being Morphism of b1,b2 holds (t . b2) * ((F ?- a1) /. g) = ((F ?- a2) /. g) * (t . b1) ) assume A9: Hom (b1,b2) <> {} ; ::_thesis: for g being Morphism of b1,b2 holds (t . b2) * ((F ?- a1) /. g) = ((F ?- a2) /. g) * (t . b1) A10: Hom (((F ?- a2) . b1),((F ?- a2) . b2)) <> {} by A9, CAT_1:84; let g be Morphism of b1,b2; ::_thesis: (t . b2) * ((F ?- a1) /. g) = ((F ?- a2) /. g) * (t . b1) reconsider idb1 = id b1, idb2 = id b2 as Morphism of B ; A11: Hom (b1,b1) <> {} ; A12: dom (id b2) = b2 .= cod g by A9, CAT_1:5 ; Hom (b2,b2) <> {} ; then A13: [(f (*) ida1),(idb2 (*) g)] = [(f (*) ida1),((id b2) * g)] by A9, CAT_1:def_13 .= [(f (*) ida1),g] by A9, CAT_1:28 .= [(f * (id a1)),g] by A1, A7, CAT_1:def_13 .= [f,g] by A1, CAT_1:29 .= [((id a2) * f),g] by A1, CAT_1:28 .= [(ida2 (*) f),g] by A1, A8, CAT_1:def_13 .= [(ida2 (*) f),(g * (id b1))] by A9, CAT_1:29 .= [(ida2 (*) f),(g (*) idb1)] by A9, A11, CAT_1:def_13 ; A14: ( Hom (((F ?- a1) . b2),((F ?- a2) . b2)) <> {} & t . b2 = FfI . b2 ) by A5, NATTRA_1:def_2, NATTRA_1:def_5; A15: cod (id a1) = a1 .= dom f by A1, CAT_1:5 ; then A16: cod [(id a1),g] = [(dom f),(cod g)] by CAT_2:28 .= dom [f,(id b2)] by A12, CAT_2:28 ; A17: ( Hom (((F ?- a1) . b1),((F ?- a2) . b1)) <> {} & t . b1 = FfI . b1 ) by A5, NATTRA_1:def_2, NATTRA_1:def_5; A18: dom g = b1 by A9, CAT_1:5 .= cod (id b1) ; A19: dom (id a2) = a2 .= cod f by A1, CAT_1:5 ; then A20: dom [(id a2),g] = [(cod f),(dom g)] by CAT_2:28 .= cod [f,(id b1)] by A18, CAT_2:28 ; A21: id b2 = (IdMap B) . b2 by ISOCAT_1:def_12; A22: id b1 = (IdMap B) . b1 by ISOCAT_1:def_12; Hom (((F ?- a1) . b1),((F ?- a1) . b2)) <> {} by A9, CAT_1:84; hence (t . b2) * ((F ?- a1) /. g) = (FfI . b2) (*) ((F ?- a1) /. g) by A14, CAT_1:def_13 .= (Ff . (id b2)) (*) ((F ?- a1) /. g) by FUNCT_2:15, A21 .= (F . (f,(id b2))) (*) ((F ?- a1) /. g) by FUNCT_5:69 .= (F . [f,(id b2)]) (*) ((F ?- a1) . g) by A9, CAT_3:def_10 .= (F . (f,(id b2))) (*) (F . ((id a1),g)) by CAT_2:36 .= F . ([f,(id b2)] (*) [(id a1),g]) by A16, CAT_1:64 .= F . [(f (*) ida1),(idb2 (*) g)] by A15, A12, CAT_2:29 .= F . ([ida2,g] (*) [f,idb1]) by A19, A18, A13, CAT_2:29 .= (F . ((id a2),g)) (*) (F . [f,(id b1)]) by A20, CAT_1:64 .= ((F ?- a2) . g) (*) (F . [f,(id b1)]) by CAT_2:36 .= ((F ?- a2) /. g) (*) (F . (f,(id b1))) by A9, CAT_3:def_10 .= ((F ?- a2) /. g) (*) (Ff . (id b1)) by FUNCT_5:69 .= ((F ?- a2) /. g) (*) (FfI . b1) by FUNCT_2:15, A22 .= ((F ?- a2) /. g) * (t . b1) by A10, A17, CAT_1:def_13 ; ::_thesis: verum end; hence F ?- a1 is_naturally_transformable_to F ?- a2 by A5, NATTRA_1:def_7; ::_thesis: (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2 hence (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2 by A6, NATTRA_1:def_8; ::_thesis: verum end; definition let A, B, C be Category; let F be Functor of [:A,B:],C; let f be Morphism of A; funcF ?- f -> natural_transformation of F ?- (dom f),F ?- (cod f) equals :: ISOCAT_2:def 3 (curry (F,f)) * (IdMap B); coherence (curry (F,f)) * (IdMap B) is natural_transformation of F ?- (dom f),F ?- (cod f) proof ( Hom ((dom f),(cod f)) <> {} & f is Morphism of dom f, cod f ) by CAT_1:2, CAT_1:4; hence (curry (F,f)) * (IdMap B) is natural_transformation of F ?- (dom f),F ?- (cod f) by Th15; ::_thesis: verum end; correctness ; end; :: deftheorem defines ?- ISOCAT_2:def_3_:_ for A, B, C being Category for F being Functor of [:A,B:],C for f being Morphism of A holds F ?- f = (curry (F,f)) * (IdMap B); theorem Th16: :: ISOCAT_2:16 for A, B, C being Category for F being Functor of [:A,B:],C for g being Morphism of A holds F ?- (dom g) is_naturally_transformable_to F ?- (cod g) proof let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C for g being Morphism of A holds F ?- (dom g) is_naturally_transformable_to F ?- (cod g) let F be Functor of [:A,B:],C; ::_thesis: for g being Morphism of A holds F ?- (dom g) is_naturally_transformable_to F ?- (cod g) let g be Morphism of A; ::_thesis: F ?- (dom g) is_naturally_transformable_to F ?- (cod g) Hom ((dom g),(cod g)) <> {} by CAT_1:2; hence F ?- (dom g) is_naturally_transformable_to F ?- (cod g) by Th15; ::_thesis: verum end; theorem Th17: :: ISOCAT_2:17 for A, B, C being Category for F being Functor of [:A,B:],C for f being Morphism of A for b being Object of B holds (F ?- f) . b = F . (f,(id b)) proof let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C for f being Morphism of A for b being Object of B holds (F ?- f) . b = F . (f,(id b)) let F be Functor of [:A,B:],C; ::_thesis: for f being Morphism of A for b being Object of B holds (F ?- f) . b = F . (f,(id b)) let f be Morphism of A; ::_thesis: for b being Object of B holds (F ?- f) . b = F . (f,(id b)) let b be Object of B; ::_thesis: (F ?- f) . b = F . (f,(id b)) reconsider G = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ; reconsider Ff = (curry G) . f as Function of the carrier' of B, the carrier' of C ; A1: id b = (IdMap B) . b by ISOCAT_1:def_12; F ?- (dom f) is_naturally_transformable_to F ?- (cod f) by Th16; then F ?- (dom f) is_transformable_to F ?- (cod f) by NATTRA_1:def_7; hence (F ?- f) . b = ((curry (F,f)) * (IdMap B)) . b by NATTRA_1:def_5 .= Ff . (id b) by FUNCT_2:15, A1 .= F . (f,(id b)) by FUNCT_5:69 ; ::_thesis: verum end; theorem Th18: :: ISOCAT_2:18 for A, B, C being Category for F being Functor of [:A,B:],C for a being Object of A holds id (F ?- a) = F ?- (id a) proof let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C for a being Object of A holds id (F ?- a) = F ?- (id a) let F be Functor of [:A,B:],C; ::_thesis: for a being Object of A holds id (F ?- a) = F ?- (id a) let a be Object of A; ::_thesis: id (F ?- a) = F ?- (id a) reconsider G = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ; reconsider Ff = (curry G) . (id a) as Function of the carrier' of B, the carrier' of C ; reconsider I = F ?- (id a) as transformation of F ?- a,F ?- a ; now__::_thesis:_for_b_being_Object_of_B_holds_I_._b_=_id_((F_?-_a)_._b) let b be Object of B; ::_thesis: I . b = id ((F ?- a) . b) A1: id b = (IdMap B) . b by ISOCAT_1:def_12; thus I . b = Ff . (id b) by FUNCT_2:15, A1 .= F . ((id a),(id b)) by FUNCT_5:69 .= F . (id [a,b]) by CAT_2:31 .= id (F . [a,b]) by CAT_1:71 .= id ((F ?- a) . b) by Th10 ; ::_thesis: verum end; hence id (F ?- a) = F ?- (id a) by NATTRA_1:def_4; ::_thesis: verum end; theorem Th19: :: ISOCAT_2:19 for A, B, C being Category for F being Functor of [:A,B:],C for g, f being Morphism of A st dom g = cod f holds for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds F ?- (g (*) f) = (F ?- g) `*` t proof let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C for g, f being Morphism of A st dom g = cod f holds for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds F ?- (g (*) f) = (F ?- g) `*` t let F be Functor of [:A,B:],C; ::_thesis: for g, f being Morphism of A st dom g = cod f holds for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds F ?- (g (*) f) = (F ?- g) `*` t let g, f be Morphism of A; ::_thesis: ( dom g = cod f implies for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds F ?- (g (*) f) = (F ?- g) `*` t ) assume A1: dom g = cod f ; ::_thesis: for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds F ?- (g (*) f) = (F ?- g) `*` t A2: F ?- (dom f) is_naturally_transformable_to F ?- (dom g) by A1, Th16; then A3: F ?- (dom f) is_transformable_to F ?- (dom g) by NATTRA_1:def_7; reconsider G = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ; reconsider Fgf = (curry G) . (g (*) f), Ff = (curry G) . f, Fg = (curry G) . g as Function of the carrier' of B, the carrier' of C ; let t be natural_transformation of F ?- (dom f),F ?- (dom g); ::_thesis: ( t = F ?- f implies F ?- (g (*) f) = (F ?- g) `*` t ) assume A4: t = F ?- f ; ::_thesis: F ?- (g (*) f) = (F ?- g) `*` t reconsider s = t as transformation of F ?- (dom f),F ?- (dom g) ; A5: F ?- (dom g) is_naturally_transformable_to F ?- (cod g) by Th16; then A6: F ?- (dom g) is_transformable_to F ?- (cod g) by NATTRA_1:def_7; F ?- (dom (g (*) f)) is_naturally_transformable_to F ?- (cod (g (*) f)) by Th16; then A7: F ?- (dom (g (*) f)) is_transformable_to F ?- (cod (g (*) f)) by NATTRA_1:def_7; A8: now__::_thesis:_for_b_being_Object_of_B_holds_(F_?-_(g_(*)_f))_._b_=_((F_?-_g)_`*`_s)_._b let b be Object of B; ::_thesis: (F ?- (g (*) f)) . b = ((F ?- g) `*` s) . b A9: Hom (b,b) <> {} ; A10: id b = (IdMap B) . b by ISOCAT_1:def_12; A11: (F ?- g) . b = ((curry (F,g)) * (IdMap B)) . b by A6, NATTRA_1:def_5 .= Fg . (id b) by FUNCT_2:15, A10 .= F . (g,(id b)) by FUNCT_5:69 ; dom (id b) = b .= cod (id b) ; then A12: dom [g,(id b)] = [(cod f),(cod (id b))] by A1, CAT_2:28 .= cod [f,(id b)] by CAT_2:28 ; A13: ( Hom (((F ?- (dom g)) . b),((F ?- (cod g)) . b)) <> {} & Hom (((F ?- (dom f)) . b),((F ?- (dom g)) . b)) <> {} ) by A3, A6, NATTRA_1:def_2; A14: (F ?- f) . b = ((curry (F,f)) * (IdMap B)) . b by A1, A3, NATTRA_1:def_5 .= Ff . (id b) by FUNCT_2:15, A10 .= F . (f,(id b)) by FUNCT_5:69 ; thus (F ?- (g (*) f)) . b = ((curry (F,(g (*) f))) * (IdMap B)) . b by A7, NATTRA_1:def_5 .= Fgf . (id b) by FUNCT_2:15, A10 .= F . ((g (*) f),(id b)) by FUNCT_5:69 .= F . [(g (*) f),((id b) * (id b))] .= F . [(g (*) f),((id b) (*) (id b))] by A9, CAT_1:def_13 .= F . ([g,(id b)] (*) [f,(id b)]) by A12, CAT_2:30 .= ((F ?- g) . b) (*) (s . b) by A1, A4, A11, A14, A12, CAT_1:64 .= ((F ?- g) . b) * (s . b) by A13, CAT_1:def_13 .= ((F ?- g) `*` s) . b by A3, A6, NATTRA_1:def_6 ; ::_thesis: verum end; ( cod (g (*) f) = cod g & dom (g (*) f) = dom f ) by A1, CAT_1:17; then F ?- (g (*) f) = (F ?- g) `*` s by A3, A6, A8, NATTRA_1:18, NATTRA_1:19; hence F ?- (g (*) f) = (F ?- g) `*` t by A2, A5, NATTRA_1:def_9; ::_thesis: verum end; definition let A, B, C be Category; let F be Functor of [:A,B:],C; func export F -> Functor of A, Functors (B,C) means :Def4: :: ISOCAT_2:def 4 for f being Morphism of A holds it . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)]; existence ex b1 being Functor of A, Functors (B,C) st for f being Morphism of A holds b1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] proof defpred S1[ set , set ] means for f being Morphism of A st \$1 = f holds \$2 = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)]; A1: now__::_thesis:_for_m_being_set_st_m_in_the_carrier'_of_A_holds_ ex_o_being_set_st_ (_o_in_the_carrier'_of_(Functors_(B,C))_&_S1[m,o]_) let m be set ; ::_thesis: ( m in the carrier' of A implies ex o being set st ( o in the carrier' of (Functors (B,C)) & S1[m,o] ) ) assume m in the carrier' of A ; ::_thesis: ex o being set st ( o in the carrier' of (Functors (B,C)) & S1[m,o] ) then reconsider g = m as Morphism of A ; take o = [[(F ?- (dom g)),(F ?- (cod g))],(F ?- g)]; ::_thesis: ( o in the carrier' of (Functors (B,C)) & S1[m,o] ) F ?- (dom g) is_naturally_transformable_to F ?- (cod g) by Th16; then o in NatTrans (B,C) by NATTRA_1:32; hence o in the carrier' of (Functors (B,C)) by NATTRA_1:def_17; ::_thesis: S1[m,o] thus S1[m,o] ; ::_thesis: verum end; consider G being Function of the carrier' of A, the carrier' of (Functors (B,C)) such that A2: for m being set st m in the carrier' of A holds S1[m,G . m] from FUNCT_2:sch_1(A1); G is Functor of A, Functors (B,C) proof thus for c being Object of A ex d being Object of (Functors (B,C)) st G . (id c) = id d :: according to ISOCAT_1:def_1 ::_thesis: ( ( for b1 being Element of the carrier' of A holds ( G . (id (dom b1)) = id (dom (G . b1)) & G . (id (cod b1)) = id (cod (G . b1)) ) ) & ( for b1, b2 being Element of the carrier' of A holds ( not dom b2 = cod b1 or G . (b2 (*) b1) = (G . b2) (*) (G . b1) ) ) ) proof let c be Object of A; ::_thesis: ex d being Object of (Functors (B,C)) st G . (id c) = id d reconsider d = F ?- c as Object of (Functors (B,C)) by Th7; take d ; ::_thesis: G . (id c) = id d thus G . (id c) = [[(F ?- c),(F ?- c)],(F ?- (id c))] by A2 .= [[(F ?- c),(F ?- c)],(id (F ?- c))] by Th18 .= id d by NATTRA_1:def_17 ; ::_thesis: verum end; thus for f being Morphism of A holds ( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) ) ::_thesis: for b1, b2 being Element of the carrier' of A holds ( not dom b2 = cod b1 or G . (b2 (*) b1) = (G . b2) (*) (G . b1) ) proof let f be Element of the carrier' of A; ::_thesis: ( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) ) reconsider d = F ?- (dom f), c = F ?- (cod f) as Object of (Functors (B,C)) by Th7; A3: G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] by A2; thus G . (id (dom f)) = [[(F ?- (dom f)),(F ?- (dom f))],(F ?- (id (dom f)))] by A2 .= [[(F ?- (dom f)),(F ?- (dom f))],(id (F ?- (dom f)))] by Th18 .= id d by NATTRA_1:def_17 .= id (dom (G . f)) by A3, NATTRA_1:33 ; ::_thesis: G . (id (cod f)) = id (cod (G . f)) thus G . (id (cod f)) = [[(F ?- (cod f)),(F ?- (cod f))],(F ?- (id (cod f)))] by A2 .= [[(F ?- (cod f)),(F ?- (cod f))],(id (F ?- (cod f)))] by Th18 .= id c by NATTRA_1:def_17 .= id (cod (G . f)) by A3, NATTRA_1:33 ; ::_thesis: verum end; let f, g be Morphism of A; ::_thesis: ( not dom g = cod f or G . (g (*) f) = (G . g) (*) (G . f) ) assume A4: dom g = cod f ; ::_thesis: G . (g (*) f) = (G . g) (*) (G . f) then reconsider t = F ?- f as natural_transformation of F ?- (dom f),F ?- (dom g) ; A5: ( cod (g (*) f) = cod g & dom (g (*) f) = dom f ) by A4, CAT_1:17; A6: F ?- (dom g) is_naturally_transformable_to F ?- (cod g) by Th16; ( the carrier' of (Functors (B,C)) = NatTrans (B,C) & F ?- (dom f) is_naturally_transformable_to F ?- (cod f) ) by Th16, NATTRA_1:def_17; then reconsider gg = [[(F ?- (dom g)),(F ?- (cod g))],(F ?- g)], ff = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] as Morphism of (Functors (B,C)) by A6, NATTRA_1:32; A7: G . f = ff by A2; thus G . (g (*) f) = [[(F ?- (dom (g (*) f))),(F ?- (cod (g (*) f)))],(F ?- (g (*) f))] by A2 .= [[(F ?- (dom (g (*) f))),(F ?- (cod (g (*) f)))],((F ?- g) `*` t)] by A4, Th19 .= gg (*) ff by A4, A5, NATTRA_1:36 .= (G . g) (*) (G . f) by A2, A7 ; ::_thesis: verum end; then reconsider G = G as Functor of A, Functors (B,C) ; take G ; ::_thesis: for f being Morphism of A holds G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] thus for f being Morphism of A holds G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] by A2; ::_thesis: verum end; uniqueness for b1, b2 being Functor of A, Functors (B,C) st ( for f being Morphism of A holds b1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) & ( for f being Morphism of A holds b2 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) holds b1 = b2 proof let G1, G2 be Functor of A, Functors (B,C); ::_thesis: ( ( for f being Morphism of A holds G1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) & ( for f being Morphism of A holds G2 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) implies G1 = G2 ) assume that A8: for f being Morphism of A holds G1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] and A9: for f being Morphism of A holds G2 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ; ::_thesis: G1 = G2 now__::_thesis:_for_f_being_Morphism_of_A_holds_G1_._f_=_G2_._f let f be Morphism of A; ::_thesis: G1 . f = G2 . f thus G1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] by A8 .= G2 . f by A9 ; ::_thesis: verum end; hence G1 = G2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines export ISOCAT_2:def_4_:_ for A, B, C being Category for F being Functor of [:A,B:],C for b5 being Functor of A, Functors (B,C) holds ( b5 = export F iff for f being Morphism of A holds b5 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ); Lm1: for A, B being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a)) proof let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a)) let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2 for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a)) ) assume A1: F1 is_transformable_to F2 ; ::_thesis: for t being transformation of F1,F2 for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a)) let t be transformation of F1,F2; ::_thesis: for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a)) let a be Object of A; ::_thesis: t . a in Hom ((F1 . a),(F2 . a)) Hom ((F1 . a),(F2 . a)) <> {} by A1, NATTRA_1:def_2; hence t . a in Hom ((F1 . a),(F2 . a)) by CAT_1:def_5; ::_thesis: verum end; theorem Th20: :: ISOCAT_2:20 for A, B, C being Category for F being Functor of [:A,B:],C for a being Object of A holds (export F) . a = F ?- a proof let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C for a being Object of A holds (export F) . a = F ?- a let F be Functor of [:A,B:],C; ::_thesis: for a being Object of A holds (export F) . a = F ?- a let a be Object of A; ::_thesis: (export F) . a = F ?- a reconsider o = F ?- a as Object of (Functors (B,C)) by Th7; reconsider i = id a as Morphism of A ; (export F) . i = [[(F ?- a),(F ?- a)],(F ?- (id a))] by Def4 .= [[(F ?- a),(F ?- a)],(id (F ?- a))] by Th18 .= id o by NATTRA_1:def_17 ; hence (export F) . a = F ?- a by CAT_1:67; ::_thesis: verum end; theorem Th21: :: ISOCAT_2:21 for A, B, C being Category for F being Functor of [:A,B:],C for a being Object of A holds (export F) . a is Functor of B,C proof let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C for a being Object of A holds (export F) . a is Functor of B,C let F be Functor of [:A,B:],C; ::_thesis: for a being Object of A holds (export F) . a is Functor of B,C let a be Object of A; ::_thesis: (export F) . a is Functor of B,C (export F) . a = F ?- a by Th20; hence (export F) . a is Functor of B,C ; ::_thesis: verum end; theorem Th22: :: ISOCAT_2:22 for A, B, C being Category for F1, F2 being Functor of [:A,B:],C st export F1 = export F2 holds F1 = F2 proof let A, B, C be Category; ::_thesis: for F1, F2 being Functor of [:A,B:],C st export F1 = export F2 holds F1 = F2 let F1, F2 be Functor of [:A,B:],C; ::_thesis: ( export F1 = export F2 implies F1 = F2 ) assume A1: export F1 = export F2 ; ::_thesis: F1 = F2 now__::_thesis:_for_fg_being_Morphism_of_[:A,B:]_holds_F1_._fg_=_F2_._fg let fg be Morphism of [:A,B:]; ::_thesis: F1 . fg = F2 . fg consider f being Morphism of A, g being Morphism of B such that A2: fg = [f,g] by CAT_2:27; A3: ( dom (id (cod f)) = cod f & dom g = cod (id (dom g)) ) ; A4: fg = [((id (cod f)) (*) f),g] by A2, Th5 .= [((id (cod f)) (*) f),(g (*) (id (dom g)))] by Th6 .= [(id (cod f)),g] (*) [f,(id (dom g))] by A3, CAT_2:29 ; A5: [[(F1 ?- (dom f)),(F1 ?- (cod f))],(F1 ?- f)] = (export F2) . f by A1, Def4 .= [[(F2 ?- (dom f)),(F2 ?- (cod f))],(F2 ?- f)] by Def4 ; then A6: [(F1 ?- (dom f)),(F1 ?- (cod f))] = [(F2 ?- (dom f)),(F2 ?- (cod f))] by XTUPLE_0:1; then A7: F1 ?- (dom f) = F2 ?- (dom f) by XTUPLE_0:1; A8: F1 ?- (cod f) = F2 ?- (cod f) by A6, XTUPLE_0:1; then A9: F1 . ((id (cod f)),g) = (F2 ?- (cod f)) . g by CAT_2:36 .= F2 . ((id (cod f)),g) by CAT_2:36 ; A10: cod [f,(id (dom g))] = [(cod f),(cod (id (dom g)))] by CAT_2:28 .= [(cod f),(dom g)] .= [(dom (id (cod f))),(dom g)] .= dom [(id (cod f)),g] by CAT_2:28 ; F1 . (f,(id (dom g))) = (F1 ?- f) . (dom g) by Th17 .= (F2 ?- f) . (dom g) by A5, A7, A8, XTUPLE_0:1 .= F2 . (f,(id (dom g))) by Th17 ; hence F1 . fg = (F2 . [(id (cod f)),g]) (*) (F2 . [f,(id (dom g))]) by A4, A9, A10, CAT_1:64 .= F2 . fg by A4, A10, CAT_1:64 ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; theorem Th23: :: ISOCAT_2:23 for A, B, C being Category 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 ( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) proof let A, B, C be Category; ::_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 ( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) 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 ( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) ) assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2 holds ( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) then A2: F1 is_transformable_to F2 by NATTRA_1:def_7; let t be natural_transformation of F1,F2; ::_thesis: ( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) reconsider s = t as Function of [: the carrier of A, the carrier of B:], the carrier' of C ; A3: now__::_thesis:_for_a_being_Object_of_A for_S1,_S2_being_Functor_of_B,C_st_S1_=_(export_F1)_._a_&_S2_=_(export_F2)_._a_holds_ for_b_being_Object_of_B_holds_((curry_s)_._a)_._b_in_Hom_((S1_._b),(S2_._b)) let a be Object of A; ::_thesis: for S1, S2 being Functor of B,C st S1 = (export F1) . a & S2 = (export F2) . a holds for b being Object of B holds ((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) let S1, S2 be Functor of B,C; ::_thesis: ( S1 = (export F1) . a & S2 = (export F2) . a implies for b being Object of B holds ((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) ) assume that A4: S1 = (export F1) . a and A5: S2 = (export F2) . a ; ::_thesis: for b being Object of B holds ((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) let b be Object of B; ::_thesis: ((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) A6: S2 . b = (F2 ?- a) . b by A5, Th20 .= F2 . [a,b] by Th10 ; A7: ((curry s) . a) . b = s . (a,b) by FUNCT_5:69 .= t . [a,b] by A2, NATTRA_1:def_5 ; S1 . b = (F1 ?- a) . b by A4, Th20 .= F1 . [a,b] by Th10 ; hence ((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) by A2, A6, A7, Lm1; ::_thesis: verum end; A8: now__::_thesis:_for_a_being_Object_of_A for_S1,_S2_being_Functor_of_B,C_st_S1_=_(export_F1)_._a_&_S2_=_(export_F2)_._a_holds_ S1_is_transformable_to_S2 let a be Object of A; ::_thesis: for S1, S2 being Functor of B,C st S1 = (export F1) . a & S2 = (export F2) . a holds S1 is_transformable_to S2 let S1, S2 be Functor of B,C; ::_thesis: ( S1 = (export F1) . a & S2 = (export F2) . a implies S1 is_transformable_to S2 ) assume ( S1 = (export F1) . a & S2 = (export F2) . a ) ; ::_thesis: S1 is_transformable_to S2 then for b being Object of B holds Hom ((S1 . b),(S2 . b)) <> {} by A3; hence S1 is_transformable_to S2 by NATTRA_1:def_2; ::_thesis: verum end; A9: now__::_thesis:_for_a_being_Object_of_A for_S1,_S2_being_Functor_of_B,C for_T_being_transformation_of_S1,S2_st_S1_=_(export_F1)_._a_&_S2_=_(export_F2)_._a_&_T_=_(curry_s)_._a_holds_ for_b1,_b2_being_Object_of_B_st_Hom_(b1,b2)_<>_{}_holds_ for_f_being_Morphism_of_b1,b2_holds_(T_._b2)_*_(S1_/._f)_=_(S2_/._f)_*_(T_._b1) let a be Object of A; ::_thesis: for S1, S2 being Functor of B,C for T being transformation of S1,S2 st S1 = (export F1) . a & S2 = (export F2) . a & T = (curry s) . a holds for b1, b2 being Object of B st Hom (b1,b2) <> {} holds for f being Morphism of b1,b2 holds (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1) let S1, S2 be Functor of B,C; ::_thesis: for T being transformation of S1,S2 st S1 = (export F1) . a & S2 = (export F2) . a & T = (curry s) . a holds for b1, b2 being Object of B st Hom (b1,b2) <> {} holds for f being Morphism of b1,b2 holds (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1) let T be transformation of S1,S2; ::_thesis: ( S1 = (export F1) . a & S2 = (export F2) . a & T = (curry s) . a implies for b1, b2 being Object of B st Hom (b1,b2) <> {} holds for f being Morphism of b1,b2 holds (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1) ) assume that A10: S1 = (export F1) . a and A11: S2 = (export F2) . a and A12: T = (curry s) . a ; ::_thesis: for b1, b2 being Object of B st Hom (b1,b2) <> {} holds for f being Morphism of b1,b2 holds (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1) let b1, b2 be Object of B; ::_thesis: ( Hom (b1,b2) <> {} implies for f being Morphism of b1,b2 holds (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1) ) assume A13: Hom (b1,b2) <> {} ; ::_thesis: for f being Morphism of b1,b2 holds (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1) A14: Hom ((S1 . b1),(S1 . b2)) <> {} by A13, CAT_1:84; A15: T . b2 = T . b2 by A8, A10, A11, NATTRA_1:def_5 .= s . (a,b2) by A12, FUNCT_5:69 .= t . [a,b2] by A2, NATTRA_1:def_5 ; A16: Hom ((F1 . [a,b2]),(F2 . [a,b2])) <> {} by A2, NATTRA_1:def_2; let f be Morphism of b1,b2; ::_thesis: (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1) A17: Hom (a,a) <> {} ; then reconsider g = [(id a),f] as Morphism of [a,b1],[a,b2] by A13, CAT_2:33; A18: Hom ([a,b1],[a,b2]) <> {} by A13, A17, Th11; then A19: Hom ((F1 . [a,b1]),(F1 . [a,b2])) <> {} by CAT_1:84; A20: S1 is_transformable_to S2 by A8, A10, A11; then A21: Hom ((S1 . b1),(S2 . b1)) <> {} by NATTRA_1:def_2; A22: T . b1 = T . b1 by A8, A10, A11, NATTRA_1:def_5 .= s . (a,b1) by A12, FUNCT_5:69 .= t . [a,b1] by A2, NATTRA_1:def_5 ; A23: Hom ((F1 . [a,b1]),(F2 . [a,b1])) <> {} by A2, NATTRA_1:def_2; A24: Hom ((S1 . b2),(S2 . b2)) <> {} by A20, NATTRA_1:def_2; A25: Hom ((S2 . b1),(S2 . b2)) <> {} by A13, CAT_1:84; A26: S2 /. f = (F2 ?- a) /. f by A11, Th20 .= (F2 ?- a) /. f by A13, CAT_3:def_10 .= F2 . ((id a),f) by CAT_2:36 .= F2 /. g by A18, CAT_3:def_10 ; A27: Hom ((F2 . [a,b1]),(F2 . [a,b2])) <> {} by A18, CAT_1:84; A28: S1 /. f = (F1 ?- a) /. f by A10, Th20 .= (F1 ?- a) /. f by A13, CAT_3:def_10 .= F1 . ((id a),f) by CAT_2:36 .= F1 /. g by A18, CAT_3:def_10 ; thus (T . b2) * (S1 /. f) = (T . b2) (*) (S1 /. f) by A14, A24, CAT_1:def_13 .= (t . [a,b2]) * (F1 /. g) by A19, A16, A15, A28, CAT_1:def_13 .= (F2 /. g) * (t . [a,b1]) by A1, A18, NATTRA_1:def_8 .= (S2 /. f) (*) (T . b1) by A27, A23, A22, A26, CAT_1:def_13 .= (S2 /. f) * (T . b1) by A25, A21, CAT_1:def_13 ; ::_thesis: verum end; defpred S1[ set , set ] means for f being Object of A for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s & \$1 = f holds \$2 = [[((export F1) . f),((export F2) . f)],((curry s) . f)]; A29: now__::_thesis:_for_a_being_Object_of_A for_S1,_S2_being_Functor_of_B,C_st_S1_=_(export_F1)_._a_&_S2_=_(export_F2)_._a_holds_ (curry_s)_._a_is_transformation_of_S1,S2 let a be Object of A; ::_thesis: for S1, S2 being Functor of B,C st S1 = (export F1) . a & S2 = (export F2) . a holds (curry s) . a is transformation of S1,S2 let S1, S2 be Functor of B,C; ::_thesis: ( S1 = (export F1) . a & S2 = (export F2) . a implies (curry s) . a is transformation of S1,S2 ) assume A30: ( S1 = (export F1) . a & S2 = (export F2) . a ) ; ::_thesis: (curry s) . a is transformation of S1,S2 thus (curry s) . a is transformation of S1,S2 ::_thesis: verum proof thus S1 is_transformable_to S2 by A8, A30; :: according to NATTRA_1:def_3 ::_thesis: for b1 being Element of the carrier of B holds ((curry s) . a) . b1 is Morphism of S1 . b1,S2 . b1 let b be Object of B; ::_thesis: ((curry s) . a) . b is Morphism of S1 . b,S2 . b ((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) by A3, A30; hence ((curry s) . a) . b is Morphism of S1 . b,S2 . b by CAT_1:def_5; ::_thesis: verum end; end; A31: now__::_thesis:_for_m_being_set_st_m_in_the_carrier_of_A_holds_ ex_o_being_set_st_ (_o_in_the_carrier'_of_(Functors_(B,C))_&_S1[m,o]_) let m be set ; ::_thesis: ( m in the carrier of A implies ex o being set st ( o in the carrier' of (Functors (B,C)) & S1[m,o] ) ) assume m in the carrier of A ; ::_thesis: ex o being set st ( o in the carrier' of (Functors (B,C)) & S1[m,o] ) then reconsider a = m as Object of A ; reconsider S1 = (export F1) . a, S2 = (export F2) . a as Functor of B,C by Th21; take o = [[((export F1) . a),((export F2) . a)],((curry s) . a)]; ::_thesis: ( o in the carrier' of (Functors (B,C)) & S1[m,o] ) reconsider T = (curry s) . a as transformation of S1,S2 by A29; A32: S1 is_naturally_transformable_to S2 proof thus S1 is_transformable_to S2 by A8; :: according to NATTRA_1:def_7 ::_thesis: ex b1 being transformation of S1,S2 st for b2, b3 being Element of the carrier of B holds ( Hom (b2,b3) = {} or for b4 being Morphism of b2,b3 holds (b1 . b3) * (S1 /. b4) = (S2 /. b4) * (b1 . b2) ) take T ; ::_thesis: for b1, b2 being Element of the carrier of B holds ( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (T . b2) * (S1 /. b3) = (S2 /. b3) * (T . b1) ) thus for b1, b2 being Element of the carrier of B holds ( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (T . b2) * (S1 /. b3) = (S2 /. b3) * (T . b1) ) by A9; ::_thesis: verum end; for a, b being Object of B st Hom (a,b) <> {} holds for f being Morphism of a,b holds (T . b) * (S1 /. f) = (S2 /. f) * (T . a) by A9; then T is natural_transformation of S1,S2 by A32, NATTRA_1:def_8; then o in NatTrans (B,C) by A32, NATTRA_1:32; hence o in the carrier' of (Functors (B,C)) by NATTRA_1:def_17; ::_thesis: S1[m,o] thus S1[m,o] ; ::_thesis: verum end; consider G being Function of the carrier of A, the carrier' of (Functors (B,C)) such that A33: for m being set st m in the carrier of A holds S1[m,G . m] from FUNCT_2:sch_1(A31); A34: now__::_thesis:_for_a_being_Object_of_A_holds_G_._a_in_Hom_(((export_F1)_._a),((export_F2)_._a)) let a be Object of A; ::_thesis: G . a in Hom (((export F1) . a),((export F2) . a)) reconsider S1 = (export F1) . a, S2 = (export F2) . a as Functor of B,C by Th21; reconsider T = (curry s) . a as transformation of S1,S2 by A29; A35: G . a = [[S1,S2],T] by A33; A36: S1 is_naturally_transformable_to S2 proof thus S1 is_transformable_to S2 by A8; :: according to NATTRA_1:def_7 ::_thesis: ex b1 being transformation of S1,S2 st for b2, b3 being Element of the carrier of B holds ( Hom (b2,b3) = {} or for b4 being Morphism of b2,b3 holds (b1 . b3) * (S1 /. b4) = (S2 /. b4) * (b1 . b2) ) take T ; ::_thesis: for b1, b2 being Element of the carrier of B holds ( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (T . b2) * (S1 /. b3) = (S2 /. b3) * (T . b1) ) thus for b1, b2 being Element of the carrier of B holds ( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (T . b2) * (S1 /. b3) = (S2 /. b3) * (T . b1) ) by A9; ::_thesis: verum end; for a, b being Object of B st Hom (a,b) <> {} holds for f being Morphism of a,b holds (T . b) * (S1 /. f) = (S2 /. f) * (T . a) by A9; then T is natural_transformation of S1,S2 by A36, NATTRA_1:def_8; then ( dom (G . a) = S1 & cod (G . a) = S2 ) by A35, NATTRA_1:33; hence G . a in Hom (((export F1) . a),((export F2) . a)) ; ::_thesis: verum end; then A37: for a being Object of A holds Hom (((export F1) . a),((export F2) . a)) <> {} ; G is transformation of export F1, export F2 proof thus export F1 is_transformable_to export F2 by A37, NATTRA_1:def_2; :: according to NATTRA_1:def_3 ::_thesis: for b1 being Element of the carrier of A holds G . b1 is Morphism of (export F1) . b1,(export F2) . b1 let a be Object of A; ::_thesis: G . a is Morphism of (export F1) . a,(export F2) . a G . a in Hom (((export F1) . a),((export F2) . a)) by A34; hence G . a is Morphism of (export F1) . a,(export F2) . a by CAT_1:def_5; ::_thesis: verum end; then reconsider G = G as transformation of export F1, export F2 ; A38: export F1 is_transformable_to export F2 by A37, NATTRA_1:def_2; A39: now__::_thesis:_for_a,_b_being_Object_of_A_st_Hom_(a,b)_<>_{}_holds_ for_f_being_Morphism_of_a,b_holds_(G_._b)_*_((export_F1)_/._f)_=_((export_F2)_/._f)_*_(G_._a) let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (G . b) * ((export F1) /. f) = ((export F2) /. f) * (G . a) ) assume A40: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds (G . b) * ((export F1) /. f) = ((export F2) /. f) * (G . a) A41: Hom (((export F2) . a),((export F2) . b)) <> {} by A40, CAT_1:84; reconsider S1 = (export F1) . a, S2 = (export F2) . a, S3 = (export F1) . b, S4 = (export F2) . b as Functor of B,C by Th21; let f be Morphism of a,b; ::_thesis: (G . b) * ((export F1) /. f) = ((export F2) /. f) * (G . a) A42: F2 ?- a = (export F2) . a by Th20; A43: F1 ?- a = (export F1) . a by Th20; then reconsider T12 = (curry s) . a as natural_transformation of S1,S2 by A1, A42, Th13; A44: F2 ?- b = (export F2) . b by Th20; then A45: F2 ?- (cod f) = (export F2) . b by A40, CAT_1:5; then reconsider T24 = F2 ?- f as natural_transformation of S2,S4 by A40, A42, CAT_1:5; A46: G . a = G . a by A38, NATTRA_1:def_5 .= [[S1,S2],T12] by A33 ; A47: F1 ?- b = (export F1) . b by Th20; then reconsider T34 = (curry s) . b as natural_transformation of S3,S4 by A1, A44, Th13; A48: S3 is_naturally_transformable_to S4 by A1, A47, A44, Th13; then A49: S3 is_transformable_to S4 by NATTRA_1:def_7; A50: F1 ?- (cod f) = (export F1) . b by A40, A47, CAT_1:5; then reconsider T13 = F1 ?- f as natural_transformation of S1,S3 by A40, A43, CAT_1:5; A51: G . b = G . b by A38, NATTRA_1:def_5 .= [[S3,S4],T34] by A33 ; A52: S1 is_naturally_transformable_to S2 by A1, A42, A43, Th13; then A53: S1 is_transformable_to S2 by NATTRA_1:def_7; reconsider g = f as Morphism of A ; A54: Hom (((export F1) . a),((export F2) . a)) <> {} by A34; F2 ?- (dom f) = (export F2) . a by A40, A42, CAT_1:5; then A55: (export F2) . g = [[S2,S4],T24] by A45, Def4; A56: Hom (((export F1) . a),((export F1) . b)) <> {} by A40, CAT_1:84; A57: S2 is_naturally_transformable_to S4 by A40, A42, A44, Th15; then A58: S2 is_transformable_to S4 by NATTRA_1:def_7; A59: S1 is_naturally_transformable_to S3 by A40, A47, A43, Th15; then A60: S1 is_transformable_to S3 by NATTRA_1:def_7; now__::_thesis:_for_c_being_Object_of_B_holds_(T34_`*`_T13)_._c_=_(T24_`*`_T12)_._c reconsider FF1 = F1, FF2 = F2 as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ; let c be Object of B; ::_thesis: (T34 `*` T13) . c = (T24 `*` T12) . c A61: Hom ((F1 . [a,c]),(F2 . [a,c])) <> {} by A2, NATTRA_1:def_2; A62: Hom ((F1 . [b,c]),(F2 . [b,c])) <> {} by A2, NATTRA_1:def_2; A63: ( Hom ((S3 . c),(S4 . c)) <> {} & Hom ((S1 . c),(S3 . c)) <> {} ) by A60, A49, NATTRA_1:def_2; A64: ( Hom ((S2 . c),(S4 . c)) <> {} & Hom ((S1 . c),(S2 . c)) <> {} ) by A53, A58, NATTRA_1:def_2; A65: t . [b,c] = s . (b,c) by A2, NATTRA_1:def_5 .= ((curry s) . b) . c by FUNCT_5:69 .= T34 . c by A49, NATTRA_1:def_5 ; A66: t . [a,c] = s . (a,c) by A2, NATTRA_1:def_5 .= ((curry s) . a) . c by FUNCT_5:69 .= T12 . c by A53, NATTRA_1:def_5 ; A67: Hom (c,c) <> {} ; then reconsider fi = [f,(id c)] as Morphism of [a,c],[b,c] by A40, CAT_2:33; A68: Hom ([a,c],[b,c]) <> {} by A40, A67, Th11; then A69: Hom ((F2 . [a,c]),(F2 . [b,c])) <> {} by CAT_1:84; A70: id c = (IdMap B) . c by ISOCAT_1:def_12; A71: F1 /. fi = FF1 . (f,(id c)) by A68, CAT_3:def_10 .= (curry (F1,f)) . (id c) by FUNCT_5:69 .= (F1 ?- f) . c by FUNCT_2:15, A70 .= T13 . c by A60, NATTRA_1:def_5 ; A72: F2 /. fi = FF2 . (f,(id c)) by A68, CAT_3:def_10 .= (curry (F2,f)) . (id c) by FUNCT_5:69 .= (F2 ?- f) . c by FUNCT_2:15, A70 .= T24 . c by A58, NATTRA_1:def_5 ; A73: Hom ((F1 . [a,c]),(F1 . [b,c])) <> {} by A68, CAT_1:84; thus (T34 `*` T13) . c = (T34 . c) * (T13 . c) by A59, A48, NATTRA_1:25 .= (t . [b,c]) (*) (F1 /. fi) by A63, A71, A65, CAT_1:def_13 .= (t . [b,c]) * (F1 /. fi) by A62, A73, CAT_1:def_13 .= (F2 /. fi) * (t . [a,c]) by A1, A68, NATTRA_1:def_8 .= (F2 /. fi) (*) (t . [a,c]) by A61, A69, CAT_1:def_13 .= (T24 . c) * (T12 . c) by A64, A72, A66, CAT_1:def_13 .= (T24 `*` T12) . c by A52, A57, NATTRA_1:25 ; ::_thesis: verum end; then A74: T34 `*` T13 = T24 `*` T12 by A53, A58, NATTRA_1:18, NATTRA_1:19; F1 ?- (dom f) = (export F1) . a by A40, A43, CAT_1:5; then A75: (export F1) . g = [[S1,S3],T13] by A50, Def4; Hom (((export F1) . b),((export F2) . b)) <> {} by A34; hence (G . b) * ((export F1) /. f) = (G . b) (*) ((export F1) /. f) by A56, CAT_1:def_13 .= (G . b) (*) ((export F1) . g) by A40, CAT_3:def_10 .= [[S1,S4],(T34 `*` T13)] by A75, A51, NATTRA_1:36 .= ((export F2) /. g) (*) (G . a) by A55, A46, A74, NATTRA_1:36 .= ((export F2) /. f) (*) (G . a) by A40, CAT_3:def_10 .= ((export F2) /. f) * (G . a) by A54, A41, CAT_1:def_13 ; ::_thesis: verum end; A76: export F1 is_transformable_to export F2 by A37, NATTRA_1:def_2; hence export F1 is_naturally_transformable_to export F2 by A39, NATTRA_1:def_7; ::_thesis: ex G being natural_transformation of export F1, export F2 st for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] export F1 is_naturally_transformable_to export F2 by A39, A76, NATTRA_1:def_7; then reconsider G = G as natural_transformation of export F1, export F2 by A39, NATTRA_1:def_8; take G ; ::_thesis: for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] let s be Function of [: the carrier of A, the carrier of B:], the carrier' of C; ::_thesis: ( t = s implies for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) assume A77: t = s ; ::_thesis: for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] let a be Object of A; ::_thesis: G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] thus G . a = G . a by A38, NATTRA_1:def_5 .= [[((export F1) . a),((export F2) . a)],((curry s) . a)] by A33, A77 ; ::_thesis: verum end; definition let A, B, C be Category; let F1, F2 be Functor of [:A,B:],C; assume B1: F1 is_naturally_transformable_to F2 ; let t be natural_transformation of F1,F2; func export t -> natural_transformation of export F1, export F2 means :Def5: :: ISOCAT_2:def 5 for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds it . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]; existence ex b1 being natural_transformation of export F1, export F2 st for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds b1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] by B1, Th23; uniqueness for b1, b2 being natural_transformation of export F1, export F2 st ( for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds b1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) & ( for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds b2 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) holds b1 = b2 proof reconsider s = t as Function of [: the carrier of A, the carrier of B:], the carrier' of C ; let T1, T2 be natural_transformation of export F1, export F2; ::_thesis: ( ( for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds T1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) & ( for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds T2 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) implies T1 = T2 ) assume that A1: for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds T1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] and A2: for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds T2 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ; ::_thesis: T1 = T2 A3: now__::_thesis:_for_a_being_Object_of_A_holds_T1_._a_=_T2_._a let a be Object of A; ::_thesis: T1 . a = T2 . a T1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] by A1; hence T1 . a = T2 . a by A2; ::_thesis: verum end; export F1 is_naturally_transformable_to export F2 by B1, Th23; then export F1 is_transformable_to export F2 by NATTRA_1:def_7; hence T1 = T2 by A3, NATTRA_1:19; ::_thesis: verum end; end; :: deftheorem Def5 defines export ISOCAT_2:def_5_:_ for A, B, C being Category 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 for b7 being natural_transformation of export F1, export F2 holds ( b7 = export t iff for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a being Object of A holds b7 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ); theorem Th24: :: ISOCAT_2:24 for A, B, C being Category for F being Functor of [:A,B:],C holds id (export F) = export (id F) proof let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C holds id (export F) = export (id F) let F be Functor of [:A,B:],C; ::_thesis: id (export F) = export (id F) reconsider s = id F as Function of [: the carrier of A, the carrier of B:], the carrier' of C ; now__::_thesis:_for_a_being_Object_of_A_holds_(id_(export_F))_._a_=_(export_(id_F))_._a let a be Object of A; ::_thesis: (id (export F)) . a = (export (id F)) . a reconsider ff = (export F) . a as Functor of B,C by Th7; A1: now__::_thesis:_for_b_being_Object_of_B_holds_(id_ff)_._b_=_((curry_s)_._a)_._b let b be Object of B; ::_thesis: (id ff) . b = ((curry s) . a) . b thus (id ff) . b = (id ff) . b by NATTRA_1:def_5 .= id (ff . b) by NATTRA_1:20 .= ff . (id b) by CAT_1:71 .= (F ?- a) . (id b) by Th20 .= F . ((id a),(id b)) by CAT_2:36 .= F . (id [a,b]) by CAT_2:31 .= id (F . [a,b]) by CAT_1:71 .= (id F) . [a,b] by NATTRA_1:20 .= (id F) . (a,b) by NATTRA_1:def_5 .= ((curry s) . a) . b by FUNCT_5:69 ; ::_thesis: verum end; thus (id (export F)) . a = id ((export F) . a) by NATTRA_1:20 .= [[ff,ff],(id ff)] by NATTRA_1:def_17 .= [[((export F) . a),((export F) . a)],((curry s) . a)] by A1, FUNCT_2:63 .= (export (id F)) . a by Def5 ; ::_thesis: verum end; hence id (export F) = export (id F) by NATTRA_1:19; ::_thesis: verum end; theorem Th25: :: ISOCAT_2:25 for A, B, C being Category for F1, F2, F3 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds for t1 being natural_transformation of F1,F2 for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1) proof let A, B, C be Category; ::_thesis: for F1, F2, F3 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds for t1 being natural_transformation of F1,F2 for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1) let F1, F2, F3 be Functor of [:A,B:],C; ::_thesis: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t1 being natural_transformation of F1,F2 for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1) ) assume that A1: F1 is_naturally_transformable_to F2 and A2: F2 is_naturally_transformable_to F3 ; ::_thesis: for t1 being natural_transformation of F1,F2 for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1) A3: F2 is_transformable_to F3 by A2, NATTRA_1:def_7; let t1 be natural_transformation of F1,F2; ::_thesis: for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1) let t2 be natural_transformation of F2,F3; ::_thesis: export (t2 `*` t1) = (export t2) `*` (export t1) A4: F1 is_transformable_to F2 by A1, NATTRA_1:def_7; A5: export F1 is_naturally_transformable_to export F2 by A1, Th23; then A6: export F1 is_transformable_to export F2 by NATTRA_1:def_7; A7: export F2 is_naturally_transformable_to export F3 by A2, Th23; then A8: export F2 is_transformable_to export F3 by NATTRA_1:def_7; A9: F1 is_naturally_transformable_to F3 by A1, A2, NATTRA_1:23; then A10: F1 is_transformable_to F3 by NATTRA_1:def_7; now__::_thesis:_for_a_being_Object_of_A_holds_(export_(t2_`*`_t1))_._a_=_((export_t2)_`*`_(export_t1))_._a let a be Object of A; ::_thesis: (export (t2 `*` t1)) . a = ((export t2) `*` (export t1)) . a reconsider S1 = (export F1) . a, S2 = (export F2) . a, S3 = (export F3) . a as Functor of B,C by Th7; reconsider s1 = t1, s2 = t2, s3 = t2 `*` t1 as Function of [: the carrier of A, the carrier of B:], the carrier' of C ; A11: S2 = F2 ?- a by Th20; A12: S3 = F3 ?- a by Th20; then reconsider T2 = (curry s2) . a as natural_transformation of S2,S3 by A2, A11, Th13; A13: S2 is_naturally_transformable_to S3 by A2, A11, A12, Th13; then A14: S2 is_transformable_to S3 by NATTRA_1:def_7; A15: S1 = F1 ?- a by Th20; then reconsider T1 = (curry s1) . a as natural_transformation of S1,S2 by A1, A11, Th13; A16: ( (export t2) . a = [[S2,S3],T2] & (export t1) . a = [[S1,S2],T1] ) by A1, A2, Def5; A17: S1 is_naturally_transformable_to S2 by A1, A15, A11, Th13; then S1 is_naturally_transformable_to S3 by A13, NATTRA_1:23; then A18: S1 is_transformable_to S3 by NATTRA_1:def_7; reconsider T3 = (curry s3) . a as natural_transformation of S1,S3 by A9, A15, A12, Th13; A19: ( Hom (((export F1) . a),((export F2) . a)) <> {} & Hom (((export F2) . a),((export F3) . a)) <> {} ) by A6, A8, NATTRA_1:def_2; A20: S1 is_transformable_to S2 by A17, NATTRA_1:def_7; now__::_thesis:_for_b_being_Object_of_B_holds_T3_._b_=_(T2_`*`_T1)_._b let b be Object of B; ::_thesis: T3 . b = (T2 `*` T1) . b A21: ( Hom ((F1 . [a,b]),(F2 . [a,b])) <> {} & Hom ((F2 . [a,b]),(F3 . [a,b])) <> {} ) by A4, A3, NATTRA_1:def_2; A22: ( Hom ((S1 . b),(S2 . b)) <> {} & Hom ((S2 . b),(S3 . b)) <> {} ) by A20, A14, NATTRA_1:def_2; A23: T1 . b = T1 . b by A20, NATTRA_1:def_5 .= s1 . (a,b) by FUNCT_5:69 .= t1 . [a,b] by A4, NATTRA_1:def_5 ; A24: T2 . b = T2 . b by A14, NATTRA_1:def_5 .= s2 . (a,b) by FUNCT_5:69 .= t2 . [a,b] by A3, NATTRA_1:def_5 ; thus T3 . b = T3 . b by A18, NATTRA_1:def_5 .= s3 . (a,b) by FUNCT_5:69 .= (t2 `*` t1) . [a,b] by A10, NATTRA_1:def_5 .= (t2 . [a,b]) * (t1 . [a,b]) by A1, A2, NATTRA_1:25 .= (T2 . b) (*) (T1 . b) by A21, A24, A23, CAT_1:def_13 .= (T2 . b) * (T1 . b) by A22, CAT_1:def_13 .= (T2 `*` T1) . b by A17, A13, NATTRA_1:25 ; ::_thesis: verum end; then A25: T3 = T2 `*` T1 by A18, NATTRA_1:19; thus (export (t2 `*` t1)) . a = [[S1,S3],T3] by A9, Def5 .= ((export t2) . a) (*) ((export t1) . a) by A16, A25, NATTRA_1:36 .= ((export t2) . a) * ((export t1) . a) by A19, CAT_1:def_13 .= ((export t2) `*` (export t1)) . a by A5, A7, NATTRA_1:25 ; ::_thesis: verum end; hence export (t2 `*` t1) = (export t2) `*` (export t1) by A6, A8, NATTRA_1:18, NATTRA_1:19; ::_thesis: verum end; theorem Th26: :: ISOCAT_2:26 for A, B, C being Category for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds for t1, t2 being natural_transformation of F1,F2 st export t1 = export t2 holds t1 = t2 proof let A, B, C be Category; ::_thesis: for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds for t1, t2 being natural_transformation of F1,F2 st export t1 = export t2 holds t1 = t2 let F1, F2 be Functor of [:A,B:],C; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t1, t2 being natural_transformation of F1,F2 st export t1 = export t2 holds t1 = t2 ) assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for t1, t2 being natural_transformation of F1,F2 st export t1 = export t2 holds t1 = t2 then A2: F1 is_transformable_to F2 by NATTRA_1:def_7; let t1, t2 be natural_transformation of F1,F2; ::_thesis: ( export t1 = export t2 implies t1 = t2 ) assume A3: export t1 = export t2 ; ::_thesis: t1 = t2 now__::_thesis:_for_ab_being_Object_of_[:A,B:]_holds_t1_._ab_=_t2_._ab reconsider s1 = t1, s2 = t2 as Function of [: the carrier of A, the carrier of B:], the carrier' of C ; let ab be Object of [:A,B:]; ::_thesis: t1 . ab = t2 . ab consider a being Object of A, b being Object of B such that A4: ab = [a,b] by DOMAIN_1:1; [[((export F1) . a),((export F2) . a)],((curry s1) . a)] = (export t1) . a by A1, Def5 .= [[((export F1) . a),((export F2) . a)],((curry s2) . a)] by A1, A3, Def5 ; then A5: (curry s1) . a = (curry s2) . a by XTUPLE_0:1; thus t1 . ab = s1 . (a,b) by A2, A4, NATTRA_1:def_5 .= ((curry s2) . a) . b by A5, FUNCT_5:69 .= s2 . (a,b) by FUNCT_5:69 .= t2 . ab by A2, A4, NATTRA_1:def_5 ; ::_thesis: verum end; hence t1 = t2 by A1, ISOCAT_1:26; ::_thesis: verum end; theorem Th27: :: ISOCAT_2:27 for A, B, C being Category for G being Functor of A, Functors (B,C) ex F being Functor of [:A,B:],C st G = export F proof let A, B, C be Category; ::_thesis: for G being Functor of A, Functors (B,C) ex F being Functor of [:A,B:],C st G = export F let G be Functor of A, Functors (B,C); ::_thesis: ex F being Functor of [:A,B:],C st G = export F defpred S1[ set , set ] means for f being Morphism of A for g being Morphism of B st \$1 = [f,g] holds for f1, f2 being Functor of B,C for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds \$2 = (t . (cod g)) (*) (f1 . g); A1: now__::_thesis:_for_m_being_set_st_m_in_the_carrier'_of_[:A,B:]_holds_ ex_o_being_set_st_ (_o_in_the_carrier'_of_C_&_S1[m,o]_) let m be set ; ::_thesis: ( m in the carrier' of [:A,B:] implies ex o being set st ( o in the carrier' of C & S1[m,o] ) ) assume m in the carrier' of [:A,B:] ; ::_thesis: ex o being set st ( o in the carrier' of C & S1[m,o] ) then consider m1 being Morphism of A, m2 being Morphism of B such that A2: m = [m1,m2] by CAT_2:27; consider F1, F2 being Functor of B,C, t1 being natural_transformation of F1,F2 such that F1 is_naturally_transformable_to F2 and dom (G . m1) = F1 and cod (G . m1) = F2 and A3: G . m1 = [[F1,F2],t1] by Th8; reconsider o = (t1 . (cod m2)) (*) (F1 . m2) as set ; take o = o; ::_thesis: ( o in the carrier' of C & S1[m,o] ) thus o in the carrier' of C ; ::_thesis: S1[m,o] thus S1[m,o] ::_thesis: verum proof let f be Morphism of A; ::_thesis: for g being Morphism of B st m = [f,g] holds for f1, f2 being Functor of B,C for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds o = (t . (cod g)) (*) (f1 . g) let g be Morphism of B; ::_thesis: ( m = [f,g] implies for f1, f2 being Functor of B,C for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds o = (t . (cod g)) (*) (f1 . g) ) assume A4: m = [f,g] ; ::_thesis: for f1, f2 being Functor of B,C for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds o = (t . (cod g)) (*) (f1 . g) then A5: g = m2 by A2, XTUPLE_0:1; let f1, f2 be Functor of B,C; ::_thesis: for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds o = (t . (cod g)) (*) (f1 . g) let t be natural_transformation of f1,f2; ::_thesis: ( G . f = [[f1,f2],t] implies o = (t . (cod g)) (*) (f1 . g) ) assume A6: G . f = [[f1,f2],t] ; ::_thesis: o = (t . (cod g)) (*) (f1 . g) A7: f = m1 by A2, A4, XTUPLE_0:1; then [F1,F2] = [f1,f2] by A3, A6, XTUPLE_0:1; then ( F1 = f1 & F2 = f2 ) by XTUPLE_0:1; hence o = (t . (cod g)) (*) (f1 . g) by A3, A7, A5, A6, XTUPLE_0:1; ::_thesis: verum end; end; consider F being Function of the carrier' of [:A,B:], the carrier' of C such that A8: for m being set st m in the carrier' of [:A,B:] holds S1[m,F . m] from FUNCT_2:sch_1(A1); F is Functor of [:A,B:],C proof thus for ab being Object of [:A,B:] ex c being Object of C st F . (id ab) = id c :: according to ISOCAT_1:def_1 ::_thesis: ( ( for b1 being Element of the carrier' of [:A,B:] holds ( F . (id (dom b1)) = id (dom (F . b1)) & F . (id (cod b1)) = id (cod (F . b1)) ) ) & ( for b1, b2 being Element of the carrier' of [:A,B:] holds ( not dom b2 = cod b1 or F . (b2 (*) b1) = (F . b2) (*) (F . b1) ) ) ) proof let ab be Object of [:A,B:]; ::_thesis: ex c being Object of C st F . (id ab) = id c consider a being Object of A, b being Object of B such that A9: ab = [a,b] by CAT_2:25; reconsider H = G . a as Functor of B,C by Th7; take H . b ; ::_thesis: F . (id ab) = id (H . b) A10: Hom ((H . b),(H . b)) <> {} ; A11: G . (id a) = id (G . a) by CAT_1:71 .= [[H,H],(id H)] by NATTRA_1:def_17 ; id ab = [(id a),(id b)] by A9, CAT_2:31; hence F . (id ab) = ((id H) . (cod (id b))) (*) (H . (id b)) by A8, A11 .= ((id H) . (cod (id b))) (*) (id (H . b)) by CAT_1:71 .= ((id H) . b) (*) (id (H . b)) by CAT_1:58 .= (id (H . b)) (*) (id (H . b)) by NATTRA_1:20 .= (id (H . b)) * (id (H . b)) by A10, CAT_1:def_13 .= id (H . b) ; ::_thesis: verum end; thus for f being Morphism of [:A,B:] holds ( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ::_thesis: for b1, b2 being Element of the carrier' of [:A,B:] holds ( not dom b2 = cod b1 or F . (b2 (*) b1) = (F . b2) (*) (F . b1) ) proof let f be Morphism of [:A,B:]; ::_thesis: ( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) consider f1 being Morphism of A, f2 being Morphism of B such that A12: f = [f1,f2] by CAT_2:27; reconsider H = G . (dom f1) as Functor of B,C by Th7; A13: Hom ((dom (H . f2)),(dom (H . f2))) <> {} ; A14: ( id (G . (dom f1)) = [[H,H],(id H)] & G . (id (dom f1)) = id (G . (dom f1)) ) by CAT_1:71, NATTRA_1:def_17; consider F1, F2 being Functor of B,C, t being natural_transformation of F1,F2 such that A15: F1 is_naturally_transformable_to F2 and A16: dom (G . f1) = F1 and A17: cod (G . f1) = F2 and A18: G . f1 = [[F1,F2],t] by Th8; A19: F1 . (cod f2) = cod (F1 . f2) by CAT_1:72; Hom ((F1 . (cod f2)),(F2 . (cod f2))) <> {} by A15, ISOCAT_1:25; then A20: dom (t . (cod f2)) = cod (F1 . f2) by A19, CAT_1:5; A21: F1 = H by A16, CAT_1:72; id (dom f) = id [(dom f1),(dom f2)] by A12, CAT_2:28 .= [(id (dom f1)),(id (dom f2))] by CAT_2:31 ; hence F . (id (dom f)) = ((id H) . (cod (id (dom f2)))) (*) (H . (id (dom f2))) by A8, A14 .= ((id H) . (cod (id (dom f2)))) (*) (id (H . (dom f2))) by CAT_1:71 .= ((id H) . (cod (id (dom f2)))) (*) (id (dom (H . f2))) by CAT_1:72 .= ((id H) . (dom f2)) (*) (id (dom (H . f2))) by CAT_1:58 .= (id (H . (dom f2))) (*) (id (dom (H . f2))) by NATTRA_1:20 .= (id (dom (H . f2))) (*) (id (dom (H . f2))) by CAT_1:72 .= (id (dom (H . f2))) * (id (dom (H . f2))) by A13, CAT_1:def_13 .= id (dom (F1 . f2)) by A21 .= id (dom ((t . (cod f2)) (*) (F1 . f2))) by A20, CAT_1:17 .= id (dom (F . f)) by A8, A12, A18 ; ::_thesis: F . (id (cod f)) = id (cod (F . f)) reconsider H = G . (cod f1) as Functor of B,C by Th7; A22: F2 = H by A17, CAT_1:72; A23: Hom ((cod (H . f2)),(cod (H . f2))) <> {} ; A24: id (cod f) = id [(cod f1),(cod f2)] by A12, CAT_2:28 .= [(id (cod f1)),(id (cod f2))] by CAT_2:31 ; A25: Hom ((F1 . (cod f2)),(F2 . (cod f2))) <> {} by A15, ISOCAT_1:25; F1 . (cod f2) = cod (F1 . f2) by CAT_1:72; then A26: dom (t . (cod f2)) = cod (F1 . f2) by A25, CAT_1:5; ( id (G . (cod f1)) = [[H,H],(id H)] & G . (id (cod f1)) = id (G . (cod f1)) ) by CAT_1:71, NATTRA_1:def_17; hence F . (id (cod f)) = ((id H) . (cod (id (cod f2)))) (*) (H . (id (cod f2))) by A8, A24 .= ((id H) . (cod (id (cod f2)))) (*) (id (H . (cod f2))) by CAT_1:71 .= ((id H) . (cod (id (cod f2)))) (*) (id (cod (H . f2))) by CAT_1:72 .= ((id H) . (cod f2)) (*) (id (cod (H . f2))) by CAT_1:58 .= (id (H . (cod f2))) (*) (id (cod (H . f2))) by NATTRA_1:20 .= (id (cod (H . f2))) (*) (id (cod (H . f2))) by CAT_1:72 .= (id (cod (H . f2))) * (id (cod (H . f2))) by A23, CAT_1:def_13 .= id (cod (H . f2)) .= id (F2 . (cod f2)) by A22, CAT_1:72 .= id (cod (t . (cod f2))) by A25, CAT_1:5 .= id (cod ((t . (cod f2)) (*) (F1 . f2))) by A26, CAT_1:17 .= id (cod (F . f)) by A8, A12, A18 ; ::_thesis: verum end; let f, g be Morphism of [:A,B:]; ::_thesis: ( not dom g = cod f or F . (g (*) f) = (F . g) (*) (F . f) ) assume A27: dom g = cod f ; ::_thesis: F . (g (*) f) = (F . g) (*) (F . f) consider g1 being Morphism of A, g2 being Morphism of B such that A28: g = [g1,g2] by CAT_2:27; reconsider g29 = g2 as Morphism of dom g2, cod g2 by CAT_1:4; consider f1 being Morphism of A, f2 being Morphism of B such that A29: f = [f1,f2] by CAT_2:27; A30: [(cod f1),(cod f2)] = cod f by A29, CAT_2:28; consider G1, G2 being Functor of B,C, s being natural_transformation of G1,G2 such that A31: G1 is_naturally_transformable_to G2 and A32: dom (G . g1) = G1 and cod (G . g1) = G2 and A33: G . g1 = [[G1,G2],s] by Th8; consider F1, F2 being Functor of B,C, t being natural_transformation of F1,F2 such that A34: F1 is_naturally_transformable_to F2 and dom (G . f1) = F1 and A35: cod (G . f1) = F2 and A36: G . f1 = [[F1,F2],t] by Th8; A37: F . f = (t . (cod f2)) (*) (F1 . f2) by A8, A29, A36; A38: [(dom g1),(dom g2)] = dom g by A28, CAT_2:28; then A39: cod f1 = dom g1 by A27, A30, XTUPLE_0:1; then reconsider s = s as natural_transformation of F2,G2 by A35, A32, CAT_1:64; A40: cod f2 = dom g2 by A27, A30, A38, XTUPLE_0:1; then A41: g (*) f = [(g1 (*) f1),(g2 (*) f2)] by A29, A28, A39, CAT_2:29; reconsider f29 = f2 as Morphism of dom f2, dom g2 by A40, CAT_1:4; A42: cod (g2 (*) f2) = cod g2 by A40, CAT_1:17; A43: Hom ((dom f2),(dom g2)) <> {} by A40, CAT_1:2; then A44: Hom ((F1 . (dom f2)),(F1 . (dom g2))) <> {} by CAT_1:84; A45: Hom ((F1 . (dom g2)),(F2 . (dom g2))) <> {} by A34, ISOCAT_1:25; then A46: Hom ((F1 . (dom f2)),(F2 . (dom g2))) <> {} by A44, CAT_1:24; A47: Hom ((dom g2),(cod g2)) <> {} by CAT_1:2; then A48: F1 /. g2 = F1 /. g29 by CAT_3:def_10; A49: F2 = G1 by A35, A32, A39, CAT_1:64; then A50: Hom ((F2 . (cod g2)),(G2 . (cod g2))) <> {} by A31, ISOCAT_1:25; A51: G1 /. g2 = F2 /. g29 by A49, A47, CAT_3:def_10; A52: Hom ((F2 . (dom g2)),(F2 . (cod g2))) <> {} by A47, CAT_1:84; then A53: Hom ((F2 . (dom g2)),(G2 . (cod g2))) <> {} by A50, CAT_1:24; A54: Hom ((F1 . (dom g2)),(F1 . (cod g2))) <> {} by A47, CAT_1:84; then A55: Hom ((F1 . (dom f2)),(F1 . (cod g2))) <> {} by A44, CAT_1:24; A56: Hom ((F1 . (cod g2)),(F2 . (cod g2))) <> {} by A34, ISOCAT_1:25; then A57: Hom ((F1 . (cod g2)),(G2 . (cod g2))) <> {} by A50, CAT_1:24; A58: F1 /. f2 = F1 /. f29 by A43, CAT_3:def_10; G . (g1 (*) f1) = (G . g1) (*) (G . f1) by A39, CAT_1:64 .= [[F1,G2],(s `*` t)] by A36, A33, A49, NATTRA_1:36 ; hence F . (g (*) f) = ((s `*` t) . (cod (g2 (*) f2))) (*) (F1 . (g2 (*) f2)) by A8, A41 .= ((s . (cod g2)) * (t . (cod g2))) (*) (F1 . (g2 (*) f2)) by A34, A31, A49, A42, NATTRA_1:25 .= ((s . (cod g2)) * (t . (cod g2))) (*) ((F1 /. g2) (*) (F1 /. f2)) by A40, CAT_1:64 .= ((s . (cod g2)) * (t . (cod g2))) (*) ((F1 /. g29) * (F1 /. f29)) by A44, A54, A48, A58, CAT_1:def_13 .= ((s . (cod g2)) * (t . (cod g2))) * ((F1 /. g29) * (F1 /. f29)) by A55, A57, CAT_1:def_13 .= (s . (cod g2)) * ((t . (cod g2)) * ((F1 /. g29) * (F1 /. f29))) by A50, A56, A55, CAT_1:25 .= (s . (cod g2)) * (((t . (cod g2)) * (F1 /. g29)) * (F1 /. f29)) by A56, A44, A54, CAT_1:25 .= (s . (cod g2)) * (((F2 /. g29) * (t . (dom g2))) * (F1 /. f29)) by A34, A47, NATTRA_1:def_8 .= (s . (cod g2)) * ((F2 /. g29) * ((t . (dom g2)) * (F1 /. f29))) by A44, A52, A45, CAT_1:25 .= ((s . (cod g2)) * (F2 /. g29)) * ((t . (dom g2)) * (F1 /. f29)) by A50, A52, A46, CAT_1:25 .= ((s . (cod g2)) * (F2 /. g29)) (*) ((t . (dom g2)) * (F1 /. f29)) by A46, A53, CAT_1:def_13 .= ((s . (cod g2)) * (F2 /. g29)) (*) ((t . (cod f2)) (*) (F1 . f2)) by A40, A44, A45, A58, CAT_1:def_13 .= ((s . (cod g2)) (*) (G1 /. g2)) (*) ((t . (cod f2)) (*) (F1 . f2)) by A50, A52, A51, CAT_1:def_13 .= (F . g) (*) (F . f) by A8, A28, A33, A49, A37 ; ::_thesis: verum end; then reconsider F = F as Functor of [:A,B:],C ; take F ; ::_thesis: G = export F now__::_thesis:_for_f_being_Morphism_of_A_holds_G_._f_=_[[(F_?-_(dom_f)),(F_?-_(cod_f))],(F_?-_f)] let f be Morphism of A; ::_thesis: G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] consider f1, f2 being Functor of B,C, t being natural_transformation of f1,f2 such that A59: f1 is_naturally_transformable_to f2 and A60: dom (G . f) = f1 and A61: cod (G . f) = f2 and A62: G . f = [[f1,f2],t] by Th8; now__::_thesis:_for_g_being_Morphism_of_B_holds_(F_?-_(dom_f))_._g_=_f1_._g let g be Morphism of B; ::_thesis: (F ?- (dom f)) . g = f1 . g A63: dom (id (cod g)) = cod g ; A64: f1 = G . (dom f) by A60, CAT_1:72; A65: G . (id (dom f)) = id (G . (dom f)) by CAT_1:71 .= [[f1,f1],(id f1)] by A64, NATTRA_1:def_17 ; thus (F ?- (dom f)) . g = F . ((id (dom f)),g) by CAT_2:36 .= F . [(id (dom f)),g] .= ((id f1) . (cod g)) (*) (f1 . g) by A8, A65 .= (id (f1 . (cod g))) (*) (f1 . g) by NATTRA_1:20 .= (f1 . (id (cod g))) (*) (f1 . g) by CAT_1:71 .= f1 . ((id (cod g)) (*) g) by A63, CAT_1:64 .= f1 . g by CAT_1:21 ; ::_thesis: verum end; then A66: f1 = F ?- (dom f) by FUNCT_2:63; now__::_thesis:_for_g_being_Morphism_of_B_holds_(F_?-_(cod_f))_._g_=_f2_._g let g be Morphism of B; ::_thesis: (F ?- (cod f)) . g = f2 . g A67: dom (id (cod g)) = cod g ; A68: f2 = G . (cod f) by A61, CAT_1:72; A69: G . (id (cod f)) = id (G . (cod f)) by CAT_1:71 .= [[f2,f2],(id f2)] by A68, NATTRA_1:def_17 ; thus (F ?- (cod f)) . g = F . ((id (cod f)),g) by CAT_2:36 .= F . [(id (cod f)),g] .= ((id f2) . (cod g)) (*) (f2 . g) by A8, A69 .= (id (f2 . (cod g))) (*) (f2 . g) by NATTRA_1:20 .= (f2 . (id (cod g))) (*) (f2 . g) by CAT_1:71 .= f2 . ((id (cod g)) (*) g) by A67, CAT_1:64 .= f2 . g by CAT_1:21 ; ::_thesis: verum end; then A70: f2 = F ?- (cod f) by FUNCT_2:63; now__::_thesis:_for_b_being_Object_of_B_holds_(F_?-_f)_._b_=_t_._b let b be Object of B; ::_thesis: (F ?- f) . b = t . b A71: Hom ((f1 . b),(f1 . b)) <> {} ; A72: Hom ((f1 . b),(f2 . b)) <> {} by A59, ISOCAT_1:25; thus (F ?- f) . b = F . (f,(id b)) by Th17 .= F . [f,(id b)] .= (t . (cod (id b))) (*) (f1 . (id b)) by A8, A62 .= (t . (cod (id b))) (*) (id (f1 . b)) by CAT_1:71 .= (t . b) (*) (id (f1 . b)) by CAT_1:58 .= (t . b) * (id (f1 . b)) by A72, A71, CAT_1:def_13 .= t . b by A72, CAT_1:29 ; ::_thesis: verum end; hence G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] by A59, A62, A66, A70, ISOCAT_1:26; ::_thesis: verum end; hence G = export F by Def4; ::_thesis: verum end; theorem Th28: :: ISOCAT_2:28 for A, B, C being Category for F1, F2 being Functor of [:A,B:],C st export F1 is_naturally_transformable_to export F2 holds for t being natural_transformation of export F1, export F2 holds ( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u ) proof let A, B, C be Category; ::_thesis: for F1, F2 being Functor of [:A,B:],C st export F1 is_naturally_transformable_to export F2 holds for t being natural_transformation of export F1, export F2 holds ( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u ) let F1, F2 be Functor of [:A,B:],C; ::_thesis: ( export F1 is_naturally_transformable_to export F2 implies for t being natural_transformation of export F1, export F2 holds ( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u ) ) assume A1: export F1 is_naturally_transformable_to export F2 ; ::_thesis: for t being natural_transformation of export F1, export F2 holds ( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u ) let t be natural_transformation of export F1, export F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u ) defpred S1[ set , set ] means for a being Object of A st \$1 = a holds t . a = [[((export F1) . a),((export F2) . a)],\$2]; A2: now__::_thesis:_for_o_being_set_st_o_in_the_carrier_of_A_holds_ ex_m_being_set_st_ (_m_in_Funcs_(_the_carrier_of_B,_the_carrier'_of_C)_&_S1[o,m]_) let o be set ; ::_thesis: ( o in the carrier of A implies ex m being set st ( m in Funcs ( the carrier of B, the carrier' of C) & S1[o,m] ) ) assume o in the carrier of A ; ::_thesis: ex m being set st ( m in Funcs ( the carrier of B, the carrier' of C) & S1[o,m] ) then reconsider a9 = o as Object of A ; consider f1, f2 being Functor of B,C, tau being natural_transformation of f1,f2 such that f1 is_naturally_transformable_to f2 and A3: dom (t . a9) = f1 and A4: ( cod (t . a9) = f2 & t . a9 = [[f1,f2],tau] ) by Th8; reconsider m = tau as set ; take m = m; ::_thesis: ( m in Funcs ( the carrier of B, the carrier' of C) & S1[o,m] ) thus m in Funcs ( the carrier of B, the carrier' of C) by FUNCT_2:8; ::_thesis: S1[o,m] thus S1[o,m] ::_thesis: verum proof let a be Object of A; ::_thesis: ( o = a implies t . a = [[((export F1) . a),((export F2) . a)],m] ) assume A5: o = a ; ::_thesis: t . a = [[((export F1) . a),((export F2) . a)],m] export F1 is_transformable_to export F2 by A1, NATTRA_1:def_7; then A6: Hom (((export F1) . a),((export F2) . a)) <> {} by NATTRA_1:def_2; then (export F1) . a = f1 by A3, A5, CAT_1:5; hence t . a = [[((export F1) . a),((export F2) . a)],m] by A4, A5, A6, CAT_1:5; ::_thesis: verum end; end; consider t9 being Function of the carrier of A,(Funcs ( the carrier of B, the carrier' of C)) such that A7: for o being set st o in the carrier of A holds S1[o,t9 . o] from FUNCT_2:sch_1(A2); reconsider u9 = uncurry t9 as Function of the carrier of [:A,B:], the carrier' of C ; A8: now__::_thesis:_for_ab_being_Object_of_[:A,B:]_holds_u9_._ab_in_Hom_((F1_._ab),(F2_._ab)) let ab be Object of [:A,B:]; ::_thesis: u9 . ab in Hom ((F1 . ab),(F2 . ab)) consider a being Object of A, b being Object of B such that A9: ab = [a,b] by DOMAIN_1:1; ( (export F1) . a = F1 ?- a & (export F2) . a = F2 ?- a ) by Th20; then t . a = [[(F1 ?- a),(F2 ?- a)],(t9 . a)] by A7; then [[(F1 ?- a),(F2 ?- a)],(t9 . a)] in the carrier' of (Functors (B,C)) ; then [[(F1 ?- a),(F2 ?- a)],(t9 . a)] in NatTrans (B,C) by NATTRA_1:def_17; then consider G1, G2 being Functor of B,C, t99 being natural_transformation of G1,G2 such that A10: [[(F1 ?- a),(F2 ?- a)],(t9 . a)] = [[G1,G2],t99] and A11: G1 is_naturally_transformable_to G2 by NATTRA_1:def_15; A12: G1 is_transformable_to G2 by A11, NATTRA_1:def_7; A13: [(F1 ?- a),(F2 ?- a)] = [G1,G2] by A10, XTUPLE_0:1; A14: F1 . [a,b] = (F1 ?- a) . b by Th10 .= G1 . b by A13, XTUPLE_0:1 ; A15: Hom ((G1 . b),(G2 . b)) <> {} by A11, ISOCAT_1:25; A16: F2 . [a,b] = (F2 ?- a) . b by Th10 .= G2 . b by A13, XTUPLE_0:1 ; u9 . (a,b) = (t9 . a) . b by Th2 .= t99 . b by A10, XTUPLE_0:1 .= t99 . b by A12, NATTRA_1:def_5 ; hence u9 . ab in Hom ((F1 . ab),(F2 . ab)) by A9, A14, A16, A15, CAT_1:def_5; ::_thesis: verum end; A17: F1 is_transformable_to F2 proof let a be Object of [:A,B:]; :: according to NATTRA_1:def_2 ::_thesis: not Hom ((F1 . a),(F2 . a)) = {} thus not Hom ((F1 . a),(F2 . a)) = {} by A8; ::_thesis: verum end; u9 is transformation of F1,F2 proof thus F1 is_transformable_to F2 by A17; :: according to NATTRA_1:def_3 ::_thesis: for b1 being Element of the carrier of [:A,B:] holds u9 . b1 is Morphism of F1 . b1,F2 . b1 let a be Object of [:A,B:]; ::_thesis: u9 . a is Morphism of F1 . a,F2 . a u9 . a in Hom ((F1 . a),(F2 . a)) by A8; hence u9 . a is Morphism of F1 . a,F2 . a by CAT_1:def_5; ::_thesis: verum end; then reconsider u = u9 as transformation of F1,F2 ; A18: now__::_thesis:_for_ab1,_ab2_being_Object_of_[:A,B:]_st_Hom_(ab1,ab2)_<>_{}_holds_ for_f_being_Morphism_of_ab1,ab2_holds_(u_._ab2)_*_(F1_/._f)_=_(F2_/._f)_*_(u_._ab1) reconsider FF1 = F1, FF2 = F2 as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ; let ab1, ab2 be Object of [:A,B:]; ::_thesis: ( Hom (ab1,ab2) <> {} implies for f being Morphism of ab1,ab2 holds (u . ab2) * (F1 /. f) = (F2 /. f) * (u . ab1) ) assume A19: Hom (ab1,ab2) <> {} ; ::_thesis: for f being Morphism of ab1,ab2 holds (u . ab2) * (F1 /. f) = (F2 /. f) * (u . ab1) A20: Hom ((F2 . ab1),(F2 . ab2)) <> {} by A19, CAT_1:84; consider a2 being Object of A, b2 being Object of B such that A21: ab2 = [a2,b2] by DOMAIN_1:1; ( (export F1) . a2 = F1 ?- a2 & (export F2) . a2 = F2 ?- a2 ) by Th20; then t . a2 = [[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] by A7; then [[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] in the carrier' of (Functors (B,C)) ; then [[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] in NatTrans (B,C) by NATTRA_1:def_17; then consider G2, H2 being Functor of B,C, t2 being natural_transformation of G2,H2 such that A22: [[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] = [[G2,H2],t2] and A23: G2 is_naturally_transformable_to H2 by NATTRA_1:def_15; A24: ( t9 . a2 = t2 & G2 is_transformable_to H2 ) by A22, A23, NATTRA_1:def_7, XTUPLE_0:1; consider a1 being Object of A, b1 being Object of B such that A25: ab1 = [a1,b1] by DOMAIN_1:1; ( (export F1) . a1 = F1 ?- a1 & (export F2) . a1 = F2 ?- a1 ) by Th20; then t . a1 = [[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] by A7; then [[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] in the carrier' of (Functors (B,C)) ; then [[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] in NatTrans (B,C) by NATTRA_1:def_17; then consider G1, H1 being Functor of B,C, t1 being natural_transformation of G1,H1 such that A26: [[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] = [[G1,H1],t1] and A27: G1 is_naturally_transformable_to H1 by NATTRA_1:def_15; A28: ( t9 . a1 = t1 & G1 is_transformable_to H1 ) by A26, A27, NATTRA_1:def_7, XTUPLE_0:1; A29: u . ab1 = u9 . (a1,b1) by A17, A25, NATTRA_1:def_5 .= (t9 . a1) . b1 by Th2 .= t1 . b1 by A28, NATTRA_1:def_5 ; A30: Hom ((G1 . b2),(H1 . b2)) <> {} by A27, ISOCAT_1:25; A31: Hom ((F1 . ab1),(F1 . ab2)) <> {} by A19, CAT_1:84; A32: Hom ((F1 . ab2),(F2 . ab2)) <> {} by A17, NATTRA_1:def_2; ( (export F2) . a1 = F2 ?- a1 & (export F1) . a1 = F1 ?- a1 ) by Th20; then A33: t . a1 = [[G1,H1],t1] by A7, A26; A34: Hom ((G1 . b1),(H1 . b1)) <> {} by A27, ISOCAT_1:25; ( (export F1) . a2 = F1 ?- a2 & (export F2) . a2 = F2 ?- a2 ) by Th20; then A35: t . a2 = [[G2,H2],t2] by A7, A22; A36: Hom (((export F1) . a2),((export F2) . a2)) <> {} by A1, ISOCAT_1:25; A37: Hom (((export F1) . a1),((export F2) . a1)) <> {} by A1, ISOCAT_1:25; let f be Morphism of ab1,ab2; ::_thesis: (u . ab2) * (F1 /. f) = (F2 /. f) * (u . ab1) consider g being Morphism of A, h being Morphism of B such that A38: f = [g,h] by DOMAIN_1:1; reconsider g = g as Morphism of a1,a2 by A19, A25, A21, A38, Th12; A39: Hom (a1,a2) <> {} by A19, A25, A21, Th11; then A40: ( dom g = a1 & cod g = a2 ) by CAT_1:5; reconsider h = h as Morphism of b1,b2 by A19, A25, A21, A38, Th12; reconsider g9 = g as Morphism of A ; reconsider h9 = h as Morphism of B ; reconsider f9 = f as Morphism of [:A,B:] ; A41: dom (id b2) = b2 ; Hom (a1,a1) <> {} ; then A42: g9 (*) (id a1) = g * (id a1) by A39, CAT_1:def_13 .= g by A39, CAT_1:29 ; A43: dom g = a1 by A39, CAT_1:5; A44: Hom (((export F2) . a1),((export F2) . a2)) <> {} by A39, CAT_1:84; reconsider e1 = (export F1) /. g, e2 = (export F2) /. g as Morphism of (Functors (B,C)) ; A45: Hom ((F1 . ab1),(F2 . ab1)) <> {} by A17, NATTRA_1:def_2; A46: Hom (b1,b2) <> {} by A19, A25, A21, Th11; then A47: Hom ((G1 . b1),(G1 . b2)) <> {} by CAT_1:84; A48: [(F1 ?- a1),(F2 ?- a1)] = [G1,H1] by A26, XTUPLE_0:1; then A49: F2 ?- a1 = H1 by XTUPLE_0:1; then A50: H1 /. h = (F2 ?- a1) /. h by A46, CAT_3:def_10 .= F2 . ((id a1),h) by CAT_2:36 ; A51: [(F1 ?- a2),(F2 ?- a2)] = [G2,H2] by A22, XTUPLE_0:1; then A52: F2 ?- a2 = H2 by XTUPLE_0:1; then A53: Hom ((H1 . b2),(H2 . b2)) <> {} by A49, A40, Th16, ISOCAT_1:25; A54: F1 ?- a2 = G2 by A51, XTUPLE_0:1; then reconsider v1 = F1 ?- g as natural_transformation of G1,G2 by A48, A40, XTUPLE_0:1; A55: Hom (((export F1) . a1),((export F1) . a2)) <> {} by A39, CAT_1:84; ( cod (id a1) = a1 & cod h = b2 ) by A46, CAT_1:5; then A56: cod [(id a1),h] = [a1,b2] by CAT_2:28 .= dom [g,(id b2)] by A43, A41, CAT_2:28 ; reconsider v2 = F2 ?- g as natural_transformation of H1,H2 by A48, A52, A40, XTUPLE_0:1; A57: (export F2) . g9 = [[H1,H2],v2] by A49, A52, A40, Def4; A58: id b2 = (IdMap B) . b2 by ISOCAT_1:def_12; A59: H1 is_naturally_transformable_to H2 by A49, A52, A40, Th16; then H1 is_transformable_to H2 by NATTRA_1:def_7; then A60: v2 . b2 = ((curry (F2,g)) * (IdMap B)) . b2 by NATTRA_1:def_5 .= (curry (F2,g)) . ((IdMap B) . b2) by FUNCT_2:15 .= F2 . (g,(id b2)) by FUNCT_5:69, A58 ; A61: F1 ?- a1 = G1 by A48, XTUPLE_0:1; then A62: G1 /. h = (F1 ?- a1) /. h by A46, CAT_3:def_10 .= F1 . ((id a1),h) by CAT_2:36 ; (export F1) . g9 = [[G1,G2],v1] by A61, A54, A40, Def4; then [[G1,H2],(t2 `*` v1)] = (t . a2) (*) ((export F1) . g9) by A35, NATTRA_1:36 .= (t . a2) (*) e1 by A39, CAT_3:def_10 .= (t . a2) * ((export F1) /. g) by A55, A36, CAT_1:def_13 .= ((export F2) /. g) * (t . a1) by A1, A39, NATTRA_1:def_8 .= e2 (*) (t . a1) by A44, A37, CAT_1:def_13 .= ((export F2) . g9) (*) (t . a1) by A39, CAT_3:def_10 .= [[G1,H2],(v2 `*` t1)] by A57, A33, NATTRA_1:36 ; then A63: t2 `*` v1 = v2 `*` t1 by XTUPLE_0:1; A64: id b2 = (IdMap B) . b2 by ISOCAT_1:def_12; A65: G1 is_naturally_transformable_to G2 by A61, A54, A40, Th16; then G1 is_transformable_to G2 by NATTRA_1:def_7; then A66: v1 . b2 = ((curry (F1,g)) * (IdMap B)) . b2 by NATTRA_1:def_5 .= (curry (F1,g)) . ((IdMap B) . b2) by FUNCT_2:15 .= F1 . (g,(id b2)) by FUNCT_5:69, A64 ; A67: u . ab2 = u9 . (a2,b2) by A17, A21, NATTRA_1:def_5 .= (t9 . a2) . b2 by Th2 .= t2 . b2 by A24, NATTRA_1:def_5 ; A68: Hom ((G2 . b2),(H2 . b2)) <> {} by A23, ISOCAT_1:25; Hom (b2,b2) <> {} ; then (id b2) (*) h9 = (id b2) * h by A46, CAT_1:def_13 .= h by A46, CAT_1:28 ; then A69: f = [g,(id b2)] (*) [(id a1),h] by A38, A42, A56, CAT_2:30; A70: Hom ((H1 . b1),(H1 . b2)) <> {} by A46, CAT_1:84; then A71: Hom ((H1 . b1),(H2 . b2)) <> {} by A53, CAT_1:24; A72: F2 /. f = F2 /. f9 by A19, CAT_3:def_10 .= (v2 . b2) (*) (H1 /. h) by A56, A69, A60, A50, CAT_1:64 .= (v2 . b2) * (H1 /. h) by A53, A70, CAT_1:def_13 ; A73: Hom ((G1 . b2),(G2 . b2)) <> {} by A61, A54, A40, Th16, ISOCAT_1:25; then A74: Hom ((G1 . b1),(G2 . b2)) <> {} by A47, CAT_1:24; F1 /. f = F1 /. f9 by A19, CAT_3:def_10 .= (v1 . b2) (*) (G1 /. h) by A56, A69, A66, A62, CAT_1:64 .= (v1 . b2) * (G1 /. h) by A73, A47, CAT_1:def_13 ; hence (u . ab2) * (F1 /. f) = (t2 . b2) (*) ((v1 . b2) * (G1 /. h)) by A31, A32, A67, CAT_1:def_13 .= (t2 . b2) * ((v1 . b2) * (G1 /. h)) by A68, A74, CAT_1:def_13 .= ((t2 . b2) * (v1 . b2)) * (G1 /. h) by A68, A73, A47, CAT_1:25 .= ((v2 `*` t1) . b2) * (G1 /. h) by A23, A65, A63, NATTRA_1:25 .= ((v2 . b2) * (t1 . b2)) * (G1 /. h) by A27, A59, NATTRA_1:25 .= (v2 . b2) * ((t1 . b2) * (G1 /. h)) by A47, A53, A30, CAT_1:25 .= (v2 . b2) * ((H1 /. h) * (t1 . b1)) by A27, A46, NATTRA_1:def_8 .= ((v2 . b2) * (H1 /. h)) * (t1 . b1) by A53, A70, A34, CAT_1:25 .= (F2 /. f) (*) (u . ab1) by A34, A71, A29, A72, CAT_1:def_13 .= (F2 /. f) * (u . ab1) by A45, A20, CAT_1:def_13 ; ::_thesis: verum end; hence A75: F1 is_naturally_transformable_to F2 by A17, NATTRA_1:def_7; ::_thesis: ex u being natural_transformation of F1,F2 st t = export u then reconsider u = u as natural_transformation of F1,F2 by A18, NATTRA_1:def_8; take u ; ::_thesis: t = export u now__::_thesis:_for_s_being_Function_of_[:_the_carrier_of_A,_the_carrier_of_B:],_the_carrier'_of_C_st_u_=_s_holds_ for_a_being_Object_of_A_holds_t_._a_=_[[((export_F1)_._a),((export_F2)_._a)],((curry_s)_._a)] let s be Function of [: the carrier of A, the carrier of B:], the carrier' of C; ::_thesis: ( u = s implies for a being Object of A holds t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) assume A76: u = s ; ::_thesis: for a being Object of A holds t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] let a be Object of A; ::_thesis: t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] t9 = curry u9 by Th1; hence t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] by A7, A76; ::_thesis: verum end; hence t = export u by A75, Def5; ::_thesis: verum end; definition let A, B, C be Category; func export (A,B,C) -> Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) means :Def6: :: ISOCAT_2:def 6 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 it . [[F1,F2],t] = [[(export F1),(export F2)],(export t)]; existence ex b1 being Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) st 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 b1 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] proof defpred S1[ set , set ] 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_set_st_o_in_the_carrier'_of_(Functors_([:A,B:],C))_holds_ ex_m_being_set_st_ (_m_in_the_carrier'_of_(Functors_(A,(Functors_(B,C))))_&_S1[o,m]_) let o be set ; ::_thesis: ( o in the carrier' of (Functors ([:A,B:],C)) implies ex m being set 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 set 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; take m = [[(export F1),(export F2)],(export t)]; ::_thesis: ( m in the carrier' of (Functors (A,(Functors (B,C)))) & S1[o,m] ) export F1 is_naturally_transformable_to export F2 by A3, Th23; 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 set 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 Th7; reconsider d = export F as Object of (Functors (A,(Functors (B,C)))) by Th7; take d ; ::_thesis: FF . (id c) = id d A6: id (export F) = export (id F) by Th24; 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 Th8; 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 Th24 .= 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 Th24 .= 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 Th8; 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 Th8; 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, Th25; 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 end; uniqueness for b1, b2 being Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) st ( 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 b1 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ) & ( 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 b2 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ) holds b1 = b2 proof let IT1, IT2 be Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))); ::_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 IT1 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ) & ( 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 IT2 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ) implies IT1 = IT2 ) assume that A23: 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 IT1 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] and A24: 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 IT2 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ; ::_thesis: IT1 = IT2 now__::_thesis:_for_f_being_Morphism_of_(Functors_([:A,B:],C))_holds_IT1_._f_=_IT2_._f let f be Morphism of (Functors ([:A,B:],C)); ::_thesis: IT1 . f = IT2 . f consider F1, F2 being Functor of [:A,B:],C, t being natural_transformation of F1,F2 such that A25: F1 is_naturally_transformable_to F2 and dom f = F1 and cod f = F2 and A26: f = [[F1,F2],t] by Th8; thus IT1 . f = [[(export F1),(export F2)],(export t)] by A23, A25, A26 .= IT2 . f by A24, A25, A26 ; ::_thesis: verum end; hence IT1 = IT2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def6 defines export ISOCAT_2:def_6_:_ for A, B, C being Category for b4 being Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) holds ( b4 = export (A,B,C) iff 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 b4 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ); registration let A, B, C be Category; cluster export (A,B,C) -> isomorphic ; coherence export (A,B,C) is isomorphic proof thus export (A,B,C) is one-to-one :: according to ISOCAT_1:def_3 ::_thesis: rng (export (A,B,C)) = the carrier' of (Functors (A,(Functors (B,C)))) proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (export (A,B,C)) or not x2 in dom (export (A,B,C)) or not (export (A,B,C)) . x1 = (export (A,B,C)) . x2 or x1 = x2 ) assume x1 in dom (export (A,B,C)) ; ::_thesis: ( not x2 in dom (export (A,B,C)) or not (export (A,B,C)) . x1 = (export (A,B,C)) . x2 or x1 = x2 ) then reconsider f1 = x1 as Morphism of (Functors ([:A,B:],C)) ; consider F1, F2 being Functor of [:A,B:],C, t being natural_transformation of F1,F2 such that A1: F1 is_naturally_transformable_to F2 and dom f1 = F1 and cod f1 = F2 and A2: f1 = [[F1,F2],t] by Th8; assume x2 in dom (export (A,B,C)) ; ::_thesis: ( not (export (A,B,C)) . x1 = (export (A,B,C)) . x2 or x1 = x2 ) then reconsider f2 = x2 as Morphism of (Functors ([:A,B:],C)) ; consider G1, G2 being Functor of [:A,B:],C, u being natural_transformation of G1,G2 such that A3: G1 is_naturally_transformable_to G2 and dom f2 = G1 and cod f2 = G2 and A4: f2 = [[G1,G2],u] by Th8; assume (export (A,B,C)) . x1 = (export (A,B,C)) . x2 ; ::_thesis: x1 = x2 then A5: [[(export F1),(export F2)],(export t)] = (export (A,B,C)) . [[G1,G2],u] by A1, A2, A4, Def6 .= [[(export G1),(export G2)],(export u)] by A3, Def6 ; then A6: [(export F1),(export F2)] = [(export G1),(export G2)] by XTUPLE_0:1; then export F1 = export G1 by XTUPLE_0:1; then A7: F1 = G1 by Th22; export F2 = export G2 by A6, XTUPLE_0:1; then A8: F2 = G2 by Th22; export u = export t by A5, XTUPLE_0:1; hence x1 = x2 by A1, A2, A4, A7, A8, Th26; ::_thesis: verum end; thus rng (export (A,B,C)) c= the carrier' of (Functors (A,(Functors (B,C)))) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier' of (Functors (A,(Functors (B,C)))) c= rng (export (A,B,C)) let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in the carrier' of (Functors (A,(Functors (B,C)))) or m in rng (export (A,B,C)) ) assume m in the carrier' of (Functors (A,(Functors (B,C)))) ; ::_thesis: m in rng (export (A,B,C)) then reconsider f = m as Morphism of (Functors (A,(Functors (B,C)))) ; consider F1, F2 being Functor of A, Functors (B,C), t being natural_transformation of F1,F2 such that A9: F1 is_naturally_transformable_to F2 and dom f = F1 and cod f = F2 and A10: f = [[F1,F2],t] by Th8; consider G1 being Functor of [:A,B:],C such that A11: F1 = export G1 by Th27; consider G2 being Functor of [:A,B:],C such that A12: F2 = export G2 by Th27; consider u being natural_transformation of G1,G2 such that A13: t = export u by A9, A11, A12, Th28; A14: G1 is_naturally_transformable_to G2 by A9, A11, A12, Th28; then ( dom (export (A,B,C)) = the carrier' of (Functors ([:A,B:],C)) & [[G1,G2],u] in NatTrans ([:A,B:],C) ) by FUNCT_2:def_1, NATTRA_1:32; then A15: [[G1,G2],u] in dom (export (A,B,C)) by NATTRA_1:def_17; (export (A,B,C)) . [[G1,G2],u] = f by A10, A11, A12, A14, A13, Def6; hence m in rng (export (A,B,C)) by A15, FUNCT_1:def_3; ::_thesis: verum end; end; theorem :: ISOCAT_2:29 for A, B, C being Category holds Functors ([:A,B:],C) ~= Functors (A,(Functors (B,C))) proof let A, B, C be Category; ::_thesis: Functors ([:A,B:],C) ~= Functors (A,(Functors (B,C))) take export (A,B,C) ; :: according to ISOCAT_1:def_4 ::_thesis: export (A,B,C) is isomorphic thus export (A,B,C) is isomorphic ; ::_thesis: verum end; begin theorem Th30: :: ISOCAT_2:30 for A, B, C being Category for F1, F2 being Functor of A,B for G being Functor of B,C st F1 is_naturally_transformable_to F2 holds for t being natural_transformation of F1,F2 holds G * t = G * t proof let A, B, C be Category; ::_thesis: for F1, F2 being Functor of A,B for G being Functor of B,C st F1 is_naturally_transformable_to F2 holds for t being natural_transformation of F1,F2 holds G * t = G * t let F1, F2 be Functor of A,B; ::_thesis: for G being Functor of B,C st F1 is_naturally_transformable_to F2 holds for t being natural_transformation of F1,F2 holds G * t = G * t let G be Functor of B,C; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds G * t = G * t ) assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2 holds G * t = G * t then A2: F1 is_transformable_to F2 by NATTRA_1:def_7; let t be natural_transformation of F1,F2; ::_thesis: G * t = G * t thus G * t = G * t by A1, ISOCAT_1:def_7 .= G * t by A2, ISOCAT_1:def_5 ; ::_thesis: verum end; definition let A, B, C be Category; let F be Functor of A,B; let G be Functor of A,C; :: original: <: redefine func<:F,G:> -> Functor of A,[:B,C:]; coherence <:F,G:> is Functor of A,[:B,C:] proof thus <:F,G:> is Functor of A,[:B,C:] ; ::_thesis: verum end; end; definition let A, B, C be Category; let F be Functor of A,[:B,C:]; func Pr1 F -> Functor of A,B equals :: ISOCAT_2:def 7 (pr1 (B,C)) * F; correctness coherence (pr1 (B,C)) * F is Functor of A,B; ; func Pr2 F -> Functor of A,C equals :: ISOCAT_2:def 8 (pr2 (B,C)) * F; correctness coherence (pr2 (B,C)) * F is Functor of A,C; ; end; :: deftheorem defines Pr1 ISOCAT_2:def_7_:_ for A, B, C being Category for F being Functor of A,[:B,C:] holds Pr1 F = (pr1 (B,C)) * F; :: deftheorem defines Pr2 ISOCAT_2:def_8_:_ for A, B, C being Category for F being Functor of A,[:B,C:] holds Pr2 F = (pr2 (B,C)) * F; theorem Th31: :: ISOCAT_2:31 for A, B, C being Category for F being Functor of A,B for G being Functor of A,C holds ( Pr1 <:F,G:> = F & Pr2 <:F,G:> = G ) proof let A, B, C be Category; ::_thesis: for F being Functor of A,B for G being Functor of A,C holds ( Pr1 <:F,G:> = F & Pr2 <:F,G:> = G ) let F be Functor of A,B; ::_thesis: for G being Functor of A,C holds ( Pr1 <:F,G:> = F & Pr2 <:F,G:> = G ) let G be Functor of A,C; ::_thesis: ( Pr1 <:F,G:> = F & Pr2 <:F,G:> = G ) thus Pr1 <:F,G:> = (pr1 ( the carrier' of B, the carrier' of C)) * <:F,G:> .= F by FUNCT_3:62 ; ::_thesis: Pr2 <:F,G:> = G thus Pr2 <:F,G:> = (pr2 ( the carrier' of B, the carrier' of C)) * <:F,G:> .= G by FUNCT_3:62 ; ::_thesis: verum end; theorem Th32: :: ISOCAT_2:32 for A, B, C being Category for F, G being Functor of A,[:B,C:] st Pr1 F = Pr1 G & Pr2 F = Pr2 G holds F = G proof let A, B, C be Category; ::_thesis: for F, G being Functor of A,[:B,C:] st Pr1 F = Pr1 G & Pr2 F = Pr2 G holds F = G let F, G be Functor of A,[:B,C:]; ::_thesis: ( Pr1 F = Pr1 G & Pr2 F = Pr2 G implies F = G ) reconsider f = F, g = G as Function of the carrier' of A,[: the carrier' of B, the carrier' of C:] ; assume Pr1 F = Pr1 G ; ::_thesis: ( not Pr2 F = Pr2 G or F = G ) then A1: (pr1 ( the carrier' of B, the carrier' of C)) * f = Pr1 G .= (pr1 ( the carrier' of B, the carrier' of C)) * g ; assume Pr2 F = Pr2 G ; ::_thesis: F = G then (pr2 ( the carrier' of B, the carrier' of C)) * f = Pr2 G .= (pr2 ( the carrier' of B, the carrier' of C)) * g ; hence F = G by A1, FUNCT_3:80; ::_thesis: verum end; definition let A, B, C be Category; let F1, F2 be Functor of A,[:B,C:]; let t be natural_transformation of F1,F2; func Pr1 t -> natural_transformation of Pr1 F1, Pr1 F2 equals :: ISOCAT_2:def 9 (pr1 (B,C)) * t; coherence (pr1 (B,C)) * t is natural_transformation of Pr1 F1, Pr1 F2 ; func Pr2 t -> natural_transformation of Pr2 F1, Pr2 F2 equals :: ISOCAT_2:def 10 (pr2 (B,C)) * t; coherence (pr2 (B,C)) * t is natural_transformation of Pr2 F1, Pr2 F2 ; end; :: deftheorem defines Pr1 ISOCAT_2:def_9_:_ for A, B, C being Category for F1, F2 being Functor of A,[:B,C:] for t being natural_transformation of F1,F2 holds Pr1 t = (pr1 (B,C)) * t; :: deftheorem defines Pr2 ISOCAT_2:def_10_:_ for A, B, C being Category for F1, F2 being Functor of A,[:B,C:] for t being natural_transformation of F1,F2 holds Pr2 t = (pr2 (B,C)) * t; theorem Th33: :: ISOCAT_2:33 for A, B, C being Category for F1, F2, G1, G2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds s = t proof let A, B, C be Category; ::_thesis: for F1, F2, G1, G2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds s = t let F1, F2, G1, G2 be Functor of A,[:B,C:]; ::_thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds s = t ) assume that A1: F1 is_naturally_transformable_to F2 and A2: G1 is_naturally_transformable_to G2 ; ::_thesis: for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds s = t let s be natural_transformation of F1,F2; ::_thesis: for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds s = t let t be natural_transformation of G1,G2; ::_thesis: ( Pr1 s = Pr1 t & Pr2 s = Pr2 t implies s = t ) assume that A3: Pr1 s = Pr1 t and A4: Pr2 s = Pr2 t ; ::_thesis: s = t reconsider S = s, T = t as Function of the carrier of A,[: the carrier' of B, the carrier' of C:] ; A5: (pr2 ( the carrier' of B, the carrier' of C)) * S = (pr2 (B,C)) * S .= Pr2 s by A1, Th30 .= (pr2 (B,C)) * T by A2, A4, Th30 .= (pr2 ( the carrier' of B, the carrier' of C)) * T ; (pr1 ( the carrier' of B, the carrier' of C)) * S = (pr1 (B,C)) * S .= Pr1 s by A1, Th30 .= (pr1 (B,C)) * T by A2, A3, Th30 .= (pr1 ( the carrier' of B, the carrier' of C)) * T ; hence s = t by A5, FUNCT_3:80; ::_thesis: verum end; Lm2: for A, B, C being Category for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] proof let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 implies for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] ) assume that A1: F1 is_transformable_to G1 and A2: F2 is_transformable_to G2 ; ::_thesis: for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] let t1 be transformation of F1,G1; ::_thesis: for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] let t2 be transformation of F2,G2; ::_thesis: for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] let a be Object of A; ::_thesis: <:t1,t2:> . a = [(t1 . a),(t2 . a)] reconsider s1 = t1 as Function of the carrier of A, the carrier' of B ; reconsider s2 = t2 as Function of the carrier of A, the carrier' of C ; thus <:t1,t2:> . a = [(s1 . a),(s2 . a)] by FUNCT_3:59 .= [(t1 . a),(s2 . a)] by A1, NATTRA_1:def_5 .= [(t1 . a),(t2 . a)] by A2, NATTRA_1:def_5 ; ::_thesis: verum end; theorem Th34: :: ISOCAT_2:34 for A, B, C being Category for F being Functor of A,B for G being Functor of A,C for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds <:F,G:> . f = [(F . f),(G . f)] by FUNCT_3:59; theorem Th35: :: ISOCAT_2:35 for A, B, C being Category for F being Functor of A,B for G being Functor of A,C for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)] proof let A, B, C be Category; ::_thesis: for F being Functor of A,B for G being Functor of A,C for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)] let F be Functor of A,B; ::_thesis: for G being Functor of A,C for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)] let G be Functor of A,C; ::_thesis: for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)] let a be Object of A; ::_thesis: <:F,G:> . a = [(F . a),(G . a)] <:F,G:> . (id a) = [(F . (id a)),(G . (id a))] by FUNCT_3:59 .= [(id (F . a)),(G . (id a))] by CAT_1:71 .= [(id (F . a)),(id (G . a))] by CAT_1:71 .= id [(F . a),(G . a)] by CAT_2:31 ; hence <:F,G:> . a = [(F . a),(G . a)] by CAT_1:70; ::_thesis: verum end; Lm3: for A, B, C being Category for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) proof let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 implies for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) ) assume A1: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) ; ::_thesis: for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) let t1 be transformation of F1,G1; ::_thesis: for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) let t2 be transformation of F2,G2; ::_thesis: for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) let a be Object of A; ::_thesis: <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) A2: ( t1 . a in Hom ((F1 . a),(G1 . a)) & t2 . a in Hom ((F2 . a),(G2 . a)) ) by A1, ISOCAT_1:4; A3: ( [(F1 . a),(F2 . a)] = <:F1,F2:> . a & [(G1 . a),(G2 . a)] = <:G1,G2:> . a ) by Th35; [(t1 . a),(t2 . a)] = <:t1,t2:> . a by A1, Lm2; hence <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) by A2, A3, Th14; ::_thesis: verum end; theorem Th36: :: ISOCAT_2:36 for A, B, C being Category for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds <:F1,F2:> is_transformable_to <:G1,G2:> proof let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds <:F1,F2:> is_transformable_to <:G1,G2:> let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds <:F1,F2:> is_transformable_to <:G1,G2:> let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 implies <:F1,F2:> is_transformable_to <:G1,G2:> ) assume A1: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) ; ::_thesis: <:F1,F2:> is_transformable_to <:G1,G2:> let a be Object of A; :: according to NATTRA_1:def_2 ::_thesis: not Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) = {} thus not Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) = {} by A1, Lm3; ::_thesis: verum end; definition let A, B, C be Category; let F1, G1 be Functor of A,B; let F2, G2 be Functor of A,C; assume A1: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) ; let t1 be transformation of F1,G1; let t2 be transformation of F2,G2; func<:t1,t2:> -> transformation of <:F1,F2:>,<:G1,G2:> equals :Def11: :: ISOCAT_2:def 11 <:t1,t2:>; coherence <:t1,t2:> is transformation of <:F1,F2:>,<:G1,G2:> proof reconsider t = <:t1,t2:> as Function of the carrier of A, the carrier' of [:B,C:] ; t is transformation of <:F1,F2:>,<:G1,G2:> proof thus <:F1,F2:> is_transformable_to <:G1,G2:> by A1, Th36; :: according to NATTRA_1:def_3 ::_thesis: for b1 being Element of the carrier of A holds t . b1 is Morphism of <:F1,F2:> . b1,<:G1,G2:> . b1 let a be Object of A; ::_thesis: t . a is Morphism of <:F1,F2:> . a,<:G1,G2:> . a t . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) by A1, Lm3; hence t . a is Morphism of <:F1,F2:> . a,<:G1,G2:> . a by CAT_1:def_5; ::_thesis: verum end; hence <:t1,t2:> is transformation of <:F1,F2:>,<:G1,G2:> ; ::_thesis: verum end; end; :: deftheorem Def11 defines <: ISOCAT_2:def_11_:_ for A, B, C being Category for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 holds <:t1,t2:> = <:t1,t2:>; theorem Th37: :: ISOCAT_2:37 for A, B, C being Category for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] proof let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 implies for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] ) assume A1: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) ; ::_thesis: for t1 being transformation of F1,G1 for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] let t1 be transformation of F1,G1; ::_thesis: for t2 being transformation of F2,G2 for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] let t2 be transformation of F2,G2; ::_thesis: for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] let a be Object of A; ::_thesis: <:t1,t2:> . a = [(t1 . a),(t2 . a)] reconsider s1 = t1 as Function of the carrier of A, the carrier' of B ; reconsider s2 = t2 as Function of the carrier of A, the carrier' of C ; thus <:t1,t2:> . a = <:t1,t2:> . a by A1, Th36, NATTRA_1:def_5 .= <:s1,s2:> . a by A1, Def11 .= [(t1 . a),(t2 . a)] by A1, Lm2 ; ::_thesis: verum end; Lm4: for A, B, C being Category for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds for t1 being natural_transformation of F1,G1 for t2 being natural_transformation of F2,G2 for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) proof let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds for t1 being natural_transformation of F1,G1 for t2 being natural_transformation of F2,G2 for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds for t1 being natural_transformation of F1,G1 for t2 being natural_transformation of F2,G2 for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 implies for t1 being natural_transformation of F1,G1 for t2 being natural_transformation of F2,G2 for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) ) assume that A1: F1 is_naturally_transformable_to G1 and A2: F2 is_naturally_transformable_to G2 ; ::_thesis: for t1 being natural_transformation of F1,G1 for t2 being natural_transformation of F2,G2 for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) let t1 be natural_transformation of F1,G1; ::_thesis: for t2 being natural_transformation of F2,G2 for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) let t2 be natural_transformation of F2,G2; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) ) assume A3: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) A4: Hom ((F1 . a),(F1 . b)) <> {} by A3, CAT_1:84; let f be Morphism of a,b; ::_thesis: (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) A5: ( (t1 . b) * (F1 /. f) = (G1 /. f) * (t1 . a) & (t2 . b) * (F2 /. f) = (G2 /. f) * (t2 . a) ) by A1, A2, A3, NATTRA_1:def_8; A6: ( G1 /. f = G1 . f & G2 /. f = G2 . f ) by A3, CAT_3:def_10; A7: <:G1,G2:> /. f = <:G1,G2:> . f by A3, CAT_3:def_10 .= [(G1 /. f),(G2 /. f)] by A6, A3, Th34 ; A8: ( F1 /. f = F1 . f & F2 /. f = F2 . f ) by A3, CAT_3:def_10; A9: <:F1,F2:> /. f = <:F1,F2:> . f by A3, CAT_3:def_10 .= [(F1 /. f),(F2 /. f)] by A3, Th34, A8 ; A10: F2 is_transformable_to G2 by A2, NATTRA_1:def_7; then A11: Hom ((F2 . b),(G2 . b)) <> {} by NATTRA_1:def_2; A12: F1 is_transformable_to G1 by A1, NATTRA_1:def_7; then A13: <:t1,t2:> . b = [(t1 . b),(t2 . b)] by A10, Th37; A14: <:t1,t2:> . a = [(t1 . a),(t2 . a)] by A12, A10, Th37; A15: Hom ((G2 . a),(G2 . b)) <> {} by A3, CAT_1:84; A16: <:F1,F2:> is_transformable_to <:G1,G2:> by A12, A10, Th36; then A17: Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) <> {} by NATTRA_1:def_2; A18: Hom ((<:G1,G2:> . a),(<:G1,G2:> . b)) <> {} by A3, CAT_1:84; A19: Hom ((G1 . a),(G1 . b)) <> {} by A3, CAT_1:84; A20: Hom ((F2 . a),(F2 . b)) <> {} by A3, CAT_1:84; then A21: (t2 . b) * (F2 /. f) = (t2 . b) (*) (F2 /. f) by A11, CAT_1:def_13; A22: Hom ((F2 . a),(G2 . a)) <> {} by A10, NATTRA_1:def_2; then A23: (G2 /. f) * (t2 . a) = (G2 /. f) (*) (t2 . a) by A15, CAT_1:def_13; A24: cod (t2 . a) = G2 . a by A22, CAT_1:5 .= dom (G2 /. f) by A15, CAT_1:5 ; A25: Hom ((F1 . b),(G1 . b)) <> {} by A12, NATTRA_1:def_2; then A26: dom (t1 . b) = F1 . b by CAT_1:5 .= cod (F1 /. f) by A4, CAT_1:5 ; A27: Hom ((F1 . a),(G1 . a)) <> {} by A12, NATTRA_1:def_2; then A28: (G1 /. f) * (t1 . a) = (G1 /. f) (*) (t1 . a) by A19, CAT_1:def_13; A29: cod (t1 . a) = G1 . a by A27, CAT_1:5 .= dom (G1 /. f) by A19, CAT_1:5 ; A30: dom (t2 . b) = F2 . b by A11, CAT_1:5 .= cod (F2 /. f) by A20, CAT_1:5 ; A31: (t1 . b) * (F1 /. f) = (t1 . b) (*) (F1 /. f) by A25, A4, CAT_1:def_13; A32: Hom ((<:F1,F2:> . b),(<:G1,G2:> . b)) <> {} by A16, NATTRA_1:def_2; Hom ((<:F1,F2:> . a),(<:F1,F2:> . b)) <> {} by A3, CAT_1:84; hence (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:t1,t2:> . b) (*) (<:F1,F2:> /. f) by A32, CAT_1:def_13 .= [((G1 /. f) * (t1 . a)),((G2 /. f) * (t2 . a))] by A5, A13, A9, A26, A30, A31, A21, CAT_2:29 .= (<:G1,G2:> /. f) (*) (<:t1,t2:> . a) by A28, A23, A29, A24, A7, A14, CAT_2:29 .= (<:G1,G2:> /. f) * (<:t1,t2:> . a) by A17, A18, CAT_1:def_13 ; ::_thesis: verum end; theorem Th38: :: ISOCAT_2:38 for A, B, C being Category for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds <:F1,F2:> is_naturally_transformable_to <:G1,G2:> proof let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds <:F1,F2:> is_naturally_transformable_to <:G1,G2:> let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds <:F1,F2:> is_naturally_transformable_to <:G1,G2:> let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 implies <:F1,F2:> is_naturally_transformable_to <:G1,G2:> ) assume A1: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 ) ; ::_thesis: <:F1,F2:> is_naturally_transformable_to <:G1,G2:> ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) by A1, NATTRA_1:def_7; hence <:F1,F2:> is_transformable_to <:G1,G2:> by Th36; :: according to NATTRA_1:def_7 ::_thesis: ex b1 being transformation of <:F1,F2:>,<:G1,G2:> st for b2, b3 being Element of the carrier of A holds ( Hom (b2,b3) = {} or for b4 being Morphism of b2,b3 holds (b1 . b3) * (<:F1,F2:> /. b4) = (<:G1,G2:> /. b4) * (b1 . b2) ) set t1 = the natural_transformation of F1,G1; set t2 = the natural_transformation of F2,G2; take <: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> ; ::_thesis: for b1, b2 being Element of the carrier of A holds ( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (<: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> . b2) * (<:F1,F2:> /. b3) = (<:G1,G2:> /. b3) * (<: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> . b1) ) thus for b1, b2 being Element of the carrier of A holds ( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (<: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> . b2) * (<:F1,F2:> /. b3) = (<:G1,G2:> /. b3) * (<: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> . b1) ) by A1, Lm4; ::_thesis: verum end; definition let A, B, C be Category; let F1, G1 be Functor of A,B; let F2, G2 be Functor of A,C; assume A1: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 ) ; let t1 be natural_transformation of F1,G1; let t2 be natural_transformation of F2,G2; func<:t1,t2:> -> natural_transformation of <:F1,F2:>,<:G1,G2:> equals :Def12: :: ISOCAT_2:def 12 <:t1,t2:>; coherence <:t1,t2:> is natural_transformation of <:F1,F2:>,<:G1,G2:> proof ( <:F1,F2:> is_naturally_transformable_to <:G1,G2:> & ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) ) ) by A1, Lm4, Th38; hence <:t1,t2:> is natural_transformation of <:F1,F2:>,<:G1,G2:> by NATTRA_1:def_8; ::_thesis: verum end; end; :: deftheorem Def12 defines <: ISOCAT_2:def_12_:_ for A, B, C being Category for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds for t1 being natural_transformation of F1,G1 for t2 being natural_transformation of F2,G2 holds <:t1,t2:> = <:t1,t2:>; theorem Th39: :: ISOCAT_2:39 for A, B, C being Category for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds for t1 being natural_transformation of F1,G1 for t2 being natural_transformation of F2,G2 holds ( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 ) proof let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds for t1 being natural_transformation of F1,G1 for t2 being natural_transformation of F2,G2 holds ( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 ) let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds for t1 being natural_transformation of F1,G1 for t2 being natural_transformation of F2,G2 holds ( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 ) let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 implies for t1 being natural_transformation of F1,G1 for t2 being natural_transformation of F2,G2 holds ( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 ) ) assume A1: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 ) ; ::_thesis: for t1 being natural_transformation of F1,G1 for t2 being natural_transformation of F2,G2 holds ( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 ) A2: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) by A1, NATTRA_1:def_7; let t1 be natural_transformation of F1,G1; ::_thesis: for t2 being natural_transformation of F2,G2 holds ( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 ) let t2 be natural_transformation of F2,G2; ::_thesis: ( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 ) reconsider s = t1 as Function of the carrier of A, the carrier' of B ; <:F1,F2:> is_naturally_transformable_to <:G1,G2:> by A1, Th38; then A3: <:F1,F2:> is_transformable_to <:G1,G2:> by NATTRA_1:def_7; thus Pr1 <:t1,t2:> = (pr1 (B,C)) * <:t1,t2:> by A1, Th38, ISOCAT_1:def_7 .= (pr1 (B,C)) * <:t1,t2:> by A3, ISOCAT_1:def_5 .= (pr1 (B,C)) * <:t1,t2:> by A1, Def12 .= (pr1 (B,C)) * <:s,t2:> by A2, Def11 .= (pr1 ( the carrier' of B, the carrier' of C)) * <:s,t2:> .= t1 by FUNCT_3:62 ; ::_thesis: Pr2 <:t1,t2:> = t2 thus Pr2 <:t1,t2:> = (pr2 (B,C)) * <:t1,t2:> by A1, Th38, ISOCAT_1:def_7 .= (pr2 (B,C)) * <:t1,t2:> by A3, ISOCAT_1:def_5 .= (pr2 (B,C)) * <:t1,t2:> by A1, Def12 .= (pr2 (B,C)) * <:s,t2:> by A2, Def11 .= (pr2 ( the carrier' of B, the carrier' of C)) * <:s,t2:> .= t2 by FUNCT_3:62 ; ::_thesis: verum end; definition let A, B, C be Category; func distribute (A,B,C) -> Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] means :Def13: :: ISOCAT_2:def 13 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 it . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]; existence ex b1 being Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] st 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 b1 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] proof defpred S1[ set , set ] 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 = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]; A1: now__::_thesis:_for_f_being_Morphism_of_(Functors_(A,[:B,C:]))_ex_g_being_Element_of_the_carrier'_of_[:(Functors_(A,B)),(Functors_(A,C)):]_st_S1[f,g] let f be Morphism of (Functors (A,[:B,C:])); ::_thesis: ex g being Element of the carrier' of [:(Functors (A,B)),(Functors (A,C)):] st S1[f,g] consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that A2: F1 is_naturally_transformable_to F2 and dom f = F1 and cod f = F2 and A3: f = [[F1,F2],s] by Th8; ( the carrier' of (Functors (A,C)) = NatTrans (A,C) & Pr2 F1 is_naturally_transformable_to Pr2 F2 ) by A2, ISOCAT_1:22, NATTRA_1:def_17; then reconsider PPr2 = [[(Pr2 F1),(Pr2 F2)],(Pr2 s)] as Morphism of (Functors (A,C)) by NATTRA_1:32; ( the carrier' of (Functors (A,B)) = NatTrans (A,B) & Pr1 F1 is_naturally_transformable_to Pr1 F2 ) by A2, ISOCAT_1:22, NATTRA_1:def_17; then reconsider PPr1 = [[(Pr1 F1),(Pr1 F2)],(Pr1 s)] as Morphism of (Functors (A,B)) by NATTRA_1:32; take g = [PPr1,PPr2]; ::_thesis: S1[f,g] thus S1[f,g] ::_thesis: verum proof let G1, G2 be Functor of A,[:B,C:]; ::_thesis: for t being natural_transformation of G1,G2 st f = [[G1,G2],t] holds g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]] let t be natural_transformation of G1,G2; ::_thesis: ( f = [[G1,G2],t] implies g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]] ) assume A4: f = [[G1,G2],t] ; ::_thesis: g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]] then [G1,G2] = [F1,F2] by A3, XTUPLE_0:1; then A5: ( G1 = F1 & G2 = F2 ) by XTUPLE_0:1; t = s by A3, A4, XTUPLE_0:1; hence g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]] by A5; ::_thesis: verum end; end; consider IT being Function of the carrier' of (Functors (A,[:B,C:])), the carrier' of [:(Functors (A,B)),(Functors (A,C)):] such that A6: for f being Morphism of (Functors (A,[:B,C:])) holds S1[f,IT . f] from FUNCT_2:sch_3(A1); IT is Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] proof thus for c being Object of (Functors (A,[:B,C:])) ex d being Object of [:(Functors (A,B)),(Functors (A,C)):] st IT . (id c) = id d :: according to ISOCAT_1:def_1 ::_thesis: ( ( for b1 being Element of the carrier' of (Functors (A,[:B,C:])) holds ( IT . (id (dom b1)) = id (dom (IT . b1)) & IT . (id (cod b1)) = id (cod (IT . b1)) ) ) & ( for b1, b2 being Element of the carrier' of (Functors (A,[:B,C:])) holds ( not dom b2 = cod b1 or IT . (b2 (*) b1) = (IT . b2) (*) (IT . b1) ) ) ) proof let c be Object of (Functors (A,[:B,C:])); ::_thesis: ex d being Object of [:(Functors (A,B)),(Functors (A,C)):] st IT . (id c) = id d reconsider F = c as Functor of A,[:B,C:] by Th7; reconsider d2 = Pr2 F as Object of (Functors (A,C)) by Th7; reconsider d1 = Pr1 F as Object of (Functors (A,B)) by Th7; take [d1,d2] ; ::_thesis: IT . (id c) = id [d1,d2] Pr1 (id F) = id (Pr1 F) by ISOCAT_1:33; then A7: id d1 = [[(Pr1 F),(Pr1 F)],(Pr1 (id F))] by NATTRA_1:def_17; Pr2 (id F) = id (Pr2 F) by ISOCAT_1:33; then A8: id d2 = [[(Pr2 F),(Pr2 F)],(Pr2 (id F))] by NATTRA_1:def_17; id c = [[F,F],(id F)] by NATTRA_1:def_17; hence IT . (id c) = [(id d1),(id d2)] by A6, A7, A8 .= id [d1,d2] by CAT_2:31 ; ::_thesis: verum end; A9: the carrier' of (Functors (A,C)) = NatTrans (A,C) by NATTRA_1:def_17; A10: the carrier' of (Functors (A,B)) = NatTrans (A,B) by NATTRA_1:def_17; thus for f being Morphism of (Functors (A,[:B,C:])) holds ( IT . (id (dom f)) = id (dom (IT . f)) & IT . (id (cod f)) = id (cod (IT . f)) ) ::_thesis: for b1, b2 being Element of the carrier' of (Functors (A,[:B,C:])) holds ( not dom b2 = cod b1 or IT . (b2 (*) b1) = (IT . b2) (*) (IT . b1) ) proof let f be Morphism of (Functors (A,[:B,C:])); ::_thesis: ( IT . (id (dom f)) = id (dom (IT . f)) & IT . (id (cod f)) = id (cod (IT . f)) ) consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that A11: F1 is_naturally_transformable_to F2 and A12: dom f = F1 and A13: cod f = F2 and A14: f = [[F1,F2],s] by Th8; Pr1 F1 is_naturally_transformable_to Pr1 F2 by A11, ISOCAT_1:22; then reconsider f1 = [[(Pr1 F1),(Pr1 F2)],(Pr1 s)] as Morphism of (Functors (A,B)) by A10, NATTRA_1:32; ( dom f1 = Pr1 F1 & Pr1 (id F1) = id (Pr1 F1) ) by ISOCAT_1:33, NATTRA_1:33; then A15: id (dom f1) = [[(Pr1 F1),(Pr1 F1)],(Pr1 (id F1))] by NATTRA_1:def_17; Pr2 F1 is_naturally_transformable_to Pr2 F2 by A11, ISOCAT_1:22; then reconsider f2 = [[(Pr2 F1),(Pr2 F2)],(Pr2 s)] as Morphism of (Functors (A,C)) by A9, NATTRA_1:32; ( dom f2 = Pr2 F1 & Pr2 (id F1) = id (Pr2 F1) ) by ISOCAT_1:33, NATTRA_1:33; then A16: id (dom f2) = [[(Pr2 F1),(Pr2 F1)],(Pr2 (id F1))] by NATTRA_1:def_17; id (dom f) = [[F1,F1],(id F1)] by A12, NATTRA_1:def_17; hence IT . (id (dom f)) = [(id (dom f1)),(id (dom f2))] by A6, A15, A16 .= id [(dom f1),(dom f2)] by CAT_2:31 .= id (dom [f1,f2]) by CAT_2:28 .= id (dom (IT . f)) by A6, A14 ; ::_thesis: IT . (id (cod f)) = id (cod (IT . f)) ( cod f1 = Pr1 F2 & Pr1 (id F2) = id (Pr1 F2) ) by ISOCAT_1:33, NATTRA_1:33; then A17: id (cod f1) = [[(Pr1 F2),(Pr1 F2)],(Pr1 (id F2))] by NATTRA_1:def_17; ( cod f2 = Pr2 F2 & Pr2 (id F2) = id (Pr2 F2) ) by ISOCAT_1:33, NATTRA_1:33; then A18: id (cod f2) = [[(Pr2 F2),(Pr2 F2)],(Pr2 (id F2))] by NATTRA_1:def_17; id (cod f) = [[F2,F2],(id F2)] by A13, NATTRA_1:def_17; hence IT . (id (cod f)) = [(id (cod f1)),(id (cod f2))] by A6, A17, A18 .= id [(cod f1),(cod f2)] by CAT_2:31 .= id (cod [f1,f2]) by CAT_2:28 .= id (cod (IT . f)) by A6, A14 ; ::_thesis: verum end; let f, g be Morphism of (Functors (A,[:B,C:])); ::_thesis: ( not dom g = cod f or IT . (g (*) f) = (IT . g) (*) (IT . f) ) assume A19: dom g = cod f ; ::_thesis: IT . (g (*) f) = (IT . g) (*) (IT . f) consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that A20: F1 is_naturally_transformable_to F2 and dom f = F1 and A21: cod f = F2 and A22: f = [[F1,F2],s] by Th8; consider G1, G2 being Functor of A,[:B,C:], t being natural_transformation of G1,G2 such that A23: G1 is_naturally_transformable_to G2 and A24: dom g = G1 and cod g = G2 and A25: g = [[G1,G2],t] by Th8; reconsider t = t as natural_transformation of F2,G2 by A19, A21, A24; A26: g (*) f = [[F1,G2],(t `*` s)] by A19, A21, A22, A24, A25, NATTRA_1:36; A27: Pr2 F1 is_naturally_transformable_to Pr2 F2 by A20, ISOCAT_1:22; Pr2 F2 is_naturally_transformable_to Pr2 G2 by A19, A21, A23, A24, ISOCAT_1:22; then reconsider g2 = [[(Pr2 F2),(Pr2 G2)],(Pr2 t)], f2 = [[(Pr2 F1),(Pr2 F2)],(Pr2 s)] as Morphism of (Functors (A,C)) by A9, A27, NATTRA_1:32; A28: g2 (*) f2 = [[(Pr2 F1),(Pr2 G2)],((Pr2 t) `*` (Pr2 s))] by NATTRA_1:36 .= [[(Pr2 F1),(Pr2 G2)],(Pr2 (t `*` s))] by A19, A20, A21, A23, A24, ISOCAT_1:27 ; A29: dom g2 = Pr2 F2 by NATTRA_1:33 .= cod f2 by NATTRA_1:33 ; A30: Pr1 F1 is_naturally_transformable_to Pr1 F2 by A20, ISOCAT_1:22; Pr1 F2 is_naturally_transformable_to Pr1 G2 by A19, A21, A23, A24, ISOCAT_1:22; then reconsider g1 = [[(Pr1 F2),(Pr1 G2)],(Pr1 t)], f1 = [[(Pr1 F1),(Pr1 F2)],(Pr1 s)] as Morphism of (Functors (A,B)) by A10, A30, NATTRA_1:32; A31: dom g1 = Pr1 F2 by NATTRA_1:33 .= cod f1 by NATTRA_1:33 ; A32: IT . f = [[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]] by A6, A22; g1 (*) f1 = [[(Pr1 F1),(Pr1 G2)],((Pr1 t) `*` (Pr1 s))] by NATTRA_1:36 .= [[(Pr1 F1),(Pr1 G2)],(Pr1 (t `*` s))] by A19, A20, A21, A23, A24, ISOCAT_1:27 ; hence IT . (g (*) f) = [(g1 (*) f1),(g2 (*) f2)] by A6, A28, A26 .= [g1,g2] (*) [f1,f2] by A31, A29, CAT_2:29 .= (IT . g) (*) (IT . f) by A6, A19, A21, A24, A25, A32 ; ::_thesis: verum end; then reconsider IT = IT as Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] ; take IT ; ::_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 IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 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 IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) assume A33: F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2 holds IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] let t be natural_transformation of F1,F2; ::_thesis: IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] set f = [[F1,F2],t]; [[F1,F2],t] in NatTrans (A,[:B,C:]) by A33, NATTRA_1:32; then reconsider f = [[F1,F2],t] as Morphism of (Functors (A,[:B,C:])) by NATTRA_1:def_17; thus IT . [[F1,F2],t] = IT . f .= [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] by A6 ; ::_thesis: verum end; uniqueness for b1, b2 being Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] st ( 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 b1 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) & ( 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 b2 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) holds b1 = b2 proof let IT1, IT2 be Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):]; ::_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 IT1 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) & ( 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 IT2 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) implies IT1 = IT2 ) assume that A34: 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 IT1 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] and A35: 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 IT2 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ; ::_thesis: IT1 = IT2 now__::_thesis:_for_f_being_Morphism_of_(Functors_(A,[:B,C:]))_holds_IT1_._f_=_IT2_._f let f be Morphism of (Functors (A,[:B,C:])); ::_thesis: IT1 . f = IT2 . f consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that A36: F1 is_naturally_transformable_to F2 and dom f = F1 and cod f = F2 and A37: f = [[F1,F2],s] by Th8; thus IT1 . f = [[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]] by A34, A36, A37 .= IT2 . f by A35, A36, A37 ; ::_thesis: verum end; hence IT1 = IT2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def13 defines distribute ISOCAT_2:def_13_:_ for A, B, C being Category for b4 being Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] holds ( b4 = distribute (A,B,C) iff 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 b4 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ); registration let A, B, C be Category; cluster distribute (A,B,C) -> isomorphic ; coherence distribute (A,B,C) is isomorphic proof thus distribute (A,B,C) is one-to-one :: according to ISOCAT_1:def_3 ::_thesis: rng (distribute (A,B,C)) = the carrier' of [:(Functors (A,B)),(Functors (A,C)):] proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (distribute (A,B,C)) or not x2 in dom (distribute (A,B,C)) or not (distribute (A,B,C)) . x1 = (distribute (A,B,C)) . x2 or x1 = x2 ) assume x1 in dom (distribute (A,B,C)) ; ::_thesis: ( not x2 in dom (distribute (A,B,C)) or not (distribute (A,B,C)) . x1 = (distribute (A,B,C)) . x2 or x1 = x2 ) then reconsider f1 = x1 as Morphism of (Functors (A,[:B,C:])) ; consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that A1: F1 is_naturally_transformable_to F2 and dom f1 = F1 and cod f1 = F2 and A2: f1 = [[F1,F2],s] by Th8; assume x2 in dom (distribute (A,B,C)) ; ::_thesis: ( not (distribute (A,B,C)) . x1 = (distribute (A,B,C)) . x2 or x1 = x2 ) then reconsider f2 = x2 as Morphism of (Functors (A,[:B,C:])) ; consider G1, G2 being Functor of A,[:B,C:], t being natural_transformation of G1,G2 such that A3: G1 is_naturally_transformable_to G2 and dom f2 = G1 and cod f2 = G2 and A4: f2 = [[G1,G2],t] by Th8; assume (distribute (A,B,C)) . x1 = (distribute (A,B,C)) . x2 ; ::_thesis: x1 = x2 then A5: [[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]] = (distribute (A,B,C)) . [[G1,G2],t] by A1, A2, A4, Def13 .= [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]] by A3, Def13 ; then A6: [[(Pr1 F1),(Pr1 F2)],(Pr1 s)] = [[(Pr1 G1),(Pr1 G2)],(Pr1 t)] by XTUPLE_0:1; A7: [[(Pr2 F1),(Pr2 F2)],(Pr2 s)] = [[(Pr2 G1),(Pr2 G2)],(Pr2 t)] by A5, XTUPLE_0:1; then A8: Pr2 s = Pr2 t by XTUPLE_0:1; A9: [(Pr2 F1),(Pr2 F2)] = [(Pr2 G1),(Pr2 G2)] by A7, XTUPLE_0:1; then A10: Pr2 F1 = Pr2 G1 by XTUPLE_0:1; A11: [(Pr1 F1),(Pr1 F2)] = [(Pr1 G1),(Pr1 G2)] by A6, XTUPLE_0:1; then Pr1 F1 = Pr1 G1 by XTUPLE_0:1; then A12: F1 = G1 by A10, Th32; Pr1 s = Pr1 t by A6, XTUPLE_0:1; then A13: s = t by A1, A3, A8, Th33; A14: Pr2 F2 = Pr2 G2 by A9, XTUPLE_0:1; Pr1 F2 = Pr1 G2 by A11, XTUPLE_0:1; hence x1 = x2 by A2, A4, A14, A13, A12, Th32; ::_thesis: verum end; thus rng (distribute (A,B,C)) c= the carrier' of [:(Functors (A,B)),(Functors (A,C)):] ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier' of [:(Functors (A,B)),(Functors (A,C)):] c= rng (distribute (A,B,C)) let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in the carrier' of [:(Functors (A,B)),(Functors (A,C)):] or o in rng (distribute (A,B,C)) ) assume o in the carrier' of [:(Functors (A,B)),(Functors (A,C)):] ; ::_thesis: o in rng (distribute (A,B,C)) then consider o1 being Morphism of (Functors (A,B)), o2 being Morphism of (Functors (A,C)) such that A15: o = [o1,o2] by CAT_2:27; consider G1, G2 being Functor of A,C, t being natural_transformation of G1,G2 such that A16: G1 is_naturally_transformable_to G2 and dom o2 = G1 and cod o2 = G2 and A17: o2 = [[G1,G2],t] by Th8; consider F1, F2 being Functor of A,B, s being natural_transformation of F1,F2 such that A18: F1 is_naturally_transformable_to F2 and dom o1 = F1 and cod o1 = F2 and A19: o1 = [[F1,F2],s] by Th8; set f = [[<:F1,G1:>,<:F2,G2:>],<:s,t:>]; A20: <:F1,G1:> is_naturally_transformable_to <:F2,G2:> by A18, A16, Th38; then [[<:F1,G1:>,<:F2,G2:>],<:s,t:>] in NatTrans (A,[:B,C:]) by NATTRA_1:32; then reconsider f = [[<:F1,G1:>,<:F2,G2:>],<:s,t:>] as Morphism of (Functors (A,[:B,C:])) by NATTRA_1:def_17; A21: ( Pr1 <:F1,G1:> = F1 & Pr1 <:F2,G2:> = F2 ) by Th31; A22: ( Pr2 <:F1,G1:> = G1 & Pr2 <:F2,G2:> = G2 ) by Th31; ( Pr1 <:s,t:> = s & Pr2 <:s,t:> = t ) by A18, A16, Th39; then (distribute (A,B,C)) . f = o by A15, A19, A17, A20, A21, A22, Def13; hence o in rng (distribute (A,B,C)) by FUNCT_2:112; ::_thesis: verum end; end; theorem :: ISOCAT_2:40 for A, B, C being Category holds Functors (A,[:B,C:]) ~= [:(Functors (A,B)),(Functors (A,C)):] proof let A, B, C be Category; ::_thesis: Functors (A,[:B,C:]) ~= [:(Functors (A,B)),(Functors (A,C)):] take distribute (A,B,C) ; :: according to ISOCAT_1:def_4 ::_thesis: distribute (A,B,C) is isomorphic thus distribute (A,B,C) is isomorphic ; ::_thesis: verum end;