:: FUNCTOR2 semantic presentation begin registration let A be non empty transitive with_units AltCatStr ; let B be non empty with_units AltCatStr ; cluster -> feasible id-preserving for Functor of A,B; coherence for b1 being Functor of A,B holds ( b1 is feasible & b1 is id-preserving ) by FUNCTOR0:def_25; end; registration let A be non empty transitive with_units AltCatStr ; let B be non empty with_units AltCatStr ; cluster covariant -> Covariant comp-preserving for Functor of A,B; coherence for b1 being Functor of A,B st b1 is covariant holds ( b1 is Covariant & b1 is comp-preserving ) by FUNCTOR0:def_26; cluster Covariant comp-preserving -> covariant for Functor of A,B; coherence for b1 being Functor of A,B st b1 is Covariant & b1 is comp-preserving holds b1 is covariant by FUNCTOR0:def_26; cluster contravariant -> Contravariant comp-reversing for Functor of A,B; coherence for b1 being Functor of A,B st b1 is contravariant holds ( b1 is Contravariant & b1 is comp-reversing ) by FUNCTOR0:def_27; cluster Contravariant comp-reversing -> contravariant for Functor of A,B; coherence for b1 being Functor of A,B st b1 is Contravariant & b1 is comp-reversing holds b1 is contravariant by FUNCTOR0:def_27; end; theorem Th1: :: FUNCTOR2:1 for A, B being non empty transitive with_units AltCatStr for F being covariant Functor of A,B for a being object of A holds F . (idm a) = idm (F . a) proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being covariant Functor of A,B for a being object of A holds F . (idm a) = idm (F . a) let F be covariant Functor of A,B; ::_thesis: for a being object of A holds F . (idm a) = idm (F . a) let a be object of A; ::_thesis: F . (idm a) = idm (F . a) ( <^a,a^> <> {} & <^(F . a),(F . a)^> <> {} ) by ALTCAT_2:def_7; hence F . (idm a) = (Morph-Map (F,a,a)) . (idm a) by FUNCTOR0:def_15 .= idm (F . a) by FUNCTOR0:def_20 ; ::_thesis: verum end; begin definition let A, B be non empty transitive with_units AltCatStr ; let F1, F2 be Functor of A,B; predF1 is_transformable_to F2 means :Def1: :: FUNCTOR2:def 1 for a being object of A holds <^(F1 . a),(F2 . a)^> <> {} ; reflexivity for F1 being Functor of A,B for a being object of A holds <^(F1 . a),(F1 . a)^> <> {} by ALTCAT_2:def_7; end; :: deftheorem Def1 defines is_transformable_to FUNCTOR2:def_1_:_ for A, B being non empty transitive with_units AltCatStr for F1, F2 being Functor of A,B holds ( F1 is_transformable_to F2 iff for a being object of A holds <^(F1 . a),(F2 . a)^> <> {} ); theorem Th2: :: FUNCTOR2:2 for A, B being non empty transitive with_units AltCatStr for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds F is_transformable_to F2 proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds F is_transformable_to F2 let F, F1, F2 be Functor of A,B; ::_thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 implies F is_transformable_to F2 ) assume A1: ( F is_transformable_to F1 & F1 is_transformable_to F2 ) ; ::_thesis: F is_transformable_to F2 let a be object of A; :: according to FUNCTOR2:def_1 ::_thesis: <^(F . a),(F2 . a)^> <> {} ( <^(F . a),(F1 . a)^> <> {} & <^(F1 . a),(F2 . a)^> <> {} ) by A1, Def1; hence <^(F . a),(F2 . a)^> <> {} by ALTCAT_1:def_2; ::_thesis: verum end; definition let A, B be non empty transitive with_units AltCatStr ; let F1, F2 be Functor of A,B; assume A1: F1 is_transformable_to F2 ; mode transformation of F1,F2 -> ManySortedSet of the carrier of A means :Def2: :: FUNCTOR2:def 2 for a being object of A holds it . a is Morphism of (F1 . a),(F2 . a); existence ex b1 being ManySortedSet of the carrier of A st for a being object of A holds b1 . a is Morphism of (F1 . a),(F2 . a) proof defpred S1[ object of A, set ] means \$2 in <^(F1 . \$1),(F2 . \$1)^>; A2: for a being Element of A ex j being set st S1[a,j] proof let a be Element of A; ::_thesis: ex j being set st S1[a,j] reconsider o = a as object of A ; <^(F1 . o),(F2 . o)^> <> {} by A1, Def1; hence ex j being set st S1[a,j] by XBOOLE_0:def_1; ::_thesis: verum end; consider t being ManySortedSet of the carrier of A such that A3: for a being Element of A holds S1[a,t . a] from PBOOLE:sch_6(A2); take t ; ::_thesis: for a being object of A holds t . a is Morphism of (F1 . a),(F2 . a) thus for a being object of A holds t . a is Morphism of (F1 . a),(F2 . a) by A3; ::_thesis: verum end; end; :: deftheorem Def2 defines transformation FUNCTOR2:def_2_:_ for A, B being non empty transitive with_units AltCatStr for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for b5 being ManySortedSet of the carrier of A holds ( b5 is transformation of F1,F2 iff for a being object of A holds b5 . a is Morphism of (F1 . a),(F2 . a) ); definition let A, B be non empty transitive with_units AltCatStr ; let F be Functor of A,B; func idt F -> transformation of F,F means :Def3: :: FUNCTOR2:def 3 for a being object of A holds it . a = idm (F . a); existence ex b1 being transformation of F,F st for a being object of A holds b1 . a = idm (F . a) proof defpred S1[ object of A, set ] means \$2 = idm (F . \$1); A1: for a being Element of A ex j being set st S1[a,j] ; consider t being ManySortedSet of the carrier of A such that A2: for a being Element of A holds S1[a,t . a] from PBOOLE:sch_6(A1); for a being object of A holds t . a is Morphism of (F . a),(F . a) proof let a be Element of A; ::_thesis: t . a is Morphism of (F . a),(F . a) S1[a,t . a] by A2; hence t . a is Morphism of (F . a),(F . a) ; ::_thesis: verum end; then t is transformation of F,F by Def2; hence ex b1 being transformation of F,F st for a being object of A holds b1 . a = idm (F . a) by A2; ::_thesis: verum end; uniqueness for b1, b2 being transformation of F,F st ( for a being object of A holds b1 . a = idm (F . a) ) & ( for a being object of A holds b2 . a = idm (F . a) ) holds b1 = b2 proof let it1, it2 be transformation of F,F; ::_thesis: ( ( for a being object of A holds it1 . a = idm (F . a) ) & ( for a being object of A holds it2 . a = idm (F . a) ) implies it1 = it2 ) assume that A3: for a being object of A holds it1 . a = idm (F . a) and A4: for a being object of A holds it2 . a = idm (F . a) ; ::_thesis: it1 = it2 now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_A_holds_ it1_._a_=_it2_._a let a be set ; ::_thesis: ( a in the carrier of A implies it1 . a = it2 . a ) assume a in the carrier of A ; ::_thesis: it1 . a = it2 . a then reconsider o = a as object of A ; thus it1 . a = idm (F . o) by A3 .= it2 . a by A4 ; ::_thesis: verum end; hence it1 = it2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def3 defines idt FUNCTOR2:def_3_:_ for A, B being non empty transitive with_units AltCatStr for F being Functor of A,B for b4 being transformation of F,F holds ( b4 = idt F iff for a being object of A holds b4 . a = idm (F . a) ); definition let A, B be non empty transitive with_units AltCatStr ; let F1, F2 be Functor of A,B; assume A1: F1 is_transformable_to F2 ; let t be transformation of F1,F2; let a be object of A; funct ! a -> Morphism of (F1 . a),(F2 . a) means :Def4: :: FUNCTOR2:def 4 it = t . a; existence ex b1 being Morphism of (F1 . a),(F2 . a) st b1 = t . a proof t . a is Morphism of (F1 . a),(F2 . a) by A1, Def2; hence ex b1 being Morphism of (F1 . a),(F2 . a) st b1 = t . a ; ::_thesis: verum end; correctness uniqueness for b1, b2 being Morphism of (F1 . a),(F2 . a) st b1 = t . a & b2 = t . a holds b1 = b2; ; end; :: deftheorem Def4 defines ! FUNCTOR2:def_4_:_ for A, B being non empty transitive with_units AltCatStr 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 for b7 being Morphism of (F1 . a),(F2 . a) holds ( b7 = t ! a iff b7 = t . a ); definition let A, B be non empty transitive with_units AltCatStr ; let F, F1, F2 be Functor of A,B; assume A1: ( F is_transformable_to F1 & F1 is_transformable_to F2 ) ; let t1 be transformation of F,F1; let t2 be transformation of F1,F2; funct2 `*` t1 -> transformation of F,F2 means :Def5: :: FUNCTOR2:def 5 for a being object of A holds it ! a = (t2 ! a) * (t1 ! a); existence ex b1 being transformation of F,F2 st for a being object of A holds b1 ! a = (t2 ! a) * (t1 ! a) proof defpred S1[ object of A, set ] means \$2 = (t2 ! \$1) * (t1 ! \$1); A2: for a being Element of A ex j being set st S1[a,j] ; consider t being ManySortedSet of the carrier of A such that A3: for a being Element of A holds S1[a,t . a] from PBOOLE:sch_6(A2); A4: F is_transformable_to F2 by A1, Th2; for a being object of A holds t . a is Morphism of (F . a),(F2 . a) proof let o be Element of A; ::_thesis: t . o is Morphism of (F . o),(F2 . o) S1[o,t . o] by A3; hence t . o is Morphism of (F . o),(F2 . o) ; ::_thesis: verum end; then reconsider t9 = t as transformation of F,F2 by A4, Def2; take t9 ; ::_thesis: for a being object of A holds t9 ! a = (t2 ! a) * (t1 ! a) let a be Element of A; ::_thesis: t9 ! a = (t2 ! a) * (t1 ! a) S1[a,t . a] by A3; hence t9 ! a = (t2 ! a) * (t1 ! a) by A4, Def4; ::_thesis: verum end; uniqueness for b1, b2 being transformation of F,F2 st ( for a being object of A holds b1 ! a = (t2 ! a) * (t1 ! a) ) & ( for a being object of A holds b2 ! a = (t2 ! a) * (t1 ! a) ) holds b1 = b2 proof let it1, it2 be transformation of F,F2; ::_thesis: ( ( for a being object of A holds it1 ! a = (t2 ! a) * (t1 ! a) ) & ( for a being object of A holds it2 ! a = (t2 ! a) * (t1 ! a) ) implies it1 = it2 ) assume that A5: for a being object of A holds it1 ! a = (t2 ! a) * (t1 ! a) and A6: for a being object of A holds it2 ! a = (t2 ! a) * (t1 ! a) ; ::_thesis: it1 = it2 A7: F is_transformable_to F2 by A1, Th2; now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_A_holds_ it1_._a_=_it2_._a let a be set ; ::_thesis: ( a in the carrier of A implies it1 . a = it2 . a ) assume a in the carrier of A ; ::_thesis: it1 . a = it2 . a then reconsider o = a as object of A ; thus it1 . a = it1 ! o by A7, Def4 .= (t2 ! o) * (t1 ! o) by A5 .= it2 ! o by A6 .= it2 . a by A7, Def4 ; ::_thesis: verum end; hence it1 = it2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def5 defines `*` FUNCTOR2:def_5_:_ for A, B being non empty transitive with_units AltCatStr for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds for t1 being transformation of F,F1 for t2 being transformation of F1,F2 for b8 being transformation of F,F2 holds ( b8 = t2 `*` t1 iff for a being object of A holds b8 ! a = (t2 ! a) * (t1 ! a) ); theorem Th3: :: FUNCTOR2:3 for A, B being non empty transitive with_units AltCatStr for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t1, t2 being transformation of F1,F2 st ( for a being object of A holds t1 ! a = t2 ! a ) holds t1 = t2 proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t1, t2 being transformation of F1,F2 st ( for a being object of A holds t1 ! a = t2 ! a ) holds t1 = t2 let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t1, t2 being transformation of F1,F2 st ( for a being object of A holds t1 ! a = t2 ! a ) holds t1 = t2 ) assume A1: F1 is_transformable_to F2 ; ::_thesis: for t1, t2 being transformation of F1,F2 st ( for a being object of A holds t1 ! a = t2 ! a ) holds t1 = t2 let t1, t2 be transformation of F1,F2; ::_thesis: ( ( for a being object of A holds t1 ! a = t2 ! a ) implies t1 = t2 ) assume A2: for a being object of A holds t1 ! a = t2 ! a ; ::_thesis: t1 = t2 now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_A_holds_ t1_._a_=_t2_._a let a be set ; ::_thesis: ( a in the carrier of A implies t1 . a = t2 . a ) assume a in the carrier of A ; ::_thesis: t1 . a = t2 . a then reconsider o = a as object of A ; thus t1 . a = t1 ! o by A1, Def4 .= t2 ! o by A2 .= t2 . a by A1, Def4 ; ::_thesis: verum end; hence t1 = t2 by PBOOLE:3; ::_thesis: verum end; theorem Th4: :: FUNCTOR2:4 for A, B being non empty transitive with_units AltCatStr for F being Functor of A,B for a being object of A holds (idt F) ! a = idm (F . a) proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being Functor of A,B for a being object of A holds (idt F) ! a = idm (F . a) let F be Functor of A,B; ::_thesis: for a being object of A holds (idt F) ! a = idm (F . a) let a be object of A; ::_thesis: (idt F) ! a = idm (F . a) thus (idt F) ! a = (idt F) . a by Def4 .= idm (F . a) by Def3 ; ::_thesis: verum end; theorem Th5: :: FUNCTOR2:5 for A, B being non empty transitive with_units AltCatStr for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 holds ( (idt F2) `*` t = t & t `*` (idt F1) = t ) proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 holds ( (idt F2) `*` t = t & t `*` (idt F1) = t ) let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2 holds ( (idt F2) `*` t = t & t `*` (idt F1) = t ) ) assume A1: F1 is_transformable_to F2 ; ::_thesis: for t being transformation of F1,F2 holds ( (idt F2) `*` t = t & t `*` (idt F1) = t ) let t be transformation of F1,F2; ::_thesis: ( (idt F2) `*` t = t & t `*` (idt F1) = t ) now__::_thesis:_for_a_being_object_of_A_holds_((idt_F2)_`*`_t)_!_a_=_t_!_a let a be object of A; ::_thesis: ((idt F2) `*` t) ! a = t ! a A2: <^(F1 . a),(F2 . a)^> <> {} by A1, Def1; thus ((idt F2) `*` t) ! a = ((idt F2) ! a) * (t ! a) by A1, Def5 .= (idm (F2 . a)) * (t ! a) by Th4 .= t ! a by A2, ALTCAT_1:20 ; ::_thesis: verum end; hence (idt F2) `*` t = t by A1, Th3; ::_thesis: t `*` (idt F1) = t now__::_thesis:_for_a_being_object_of_A_holds_(t_`*`_(idt_F1))_!_a_=_t_!_a let a be object of A; ::_thesis: (t `*` (idt F1)) ! a = t ! a A3: <^(F1 . a),(F2 . a)^> <> {} by A1, Def1; thus (t `*` (idt F1)) ! a = (t ! a) * ((idt F1) ! a) by A1, Def5 .= (t ! a) * (idm (F1 . a)) by Th4 .= t ! a by A3, ALTCAT_1:def_17 ; ::_thesis: verum end; hence t `*` (idt F1) = t by A1, Th3; ::_thesis: verum end; theorem Th6: :: FUNCTOR2:6 for A, B being category for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 holds for t1 being transformation of F,F1 for t2 being transformation of F1,F2 for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) proof let A, B be category; ::_thesis: for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 holds for t1 being transformation of F,F1 for t2 being transformation of F1,F2 for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) let F, F1, F2, F3 be Functor of A,B; ::_thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 implies for t1 being transformation of F,F1 for t2 being transformation of F1,F2 for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) ) assume that A1: F is_transformable_to F1 and A2: F1 is_transformable_to F2 and A3: F2 is_transformable_to F3 ; ::_thesis: for t1 being transformation of F,F1 for t2 being transformation of F1,F2 for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) let t1 be transformation of F,F1; ::_thesis: for t2 being transformation of F1,F2 for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) let t2 be transformation of F1,F2; ::_thesis: for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) let t3 be transformation of F2,F3; ::_thesis: (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) A4: F1 is_transformable_to F3 by A2, A3, Th2; A5: F is_transformable_to F2 by A1, A2, Th2; now__::_thesis:_for_a_being_object_of_A_holds_((t3_`*`_t2)_`*`_t1)_!_a_=_(t3_`*`_(t2_`*`_t1))_!_a let a be object of A; ::_thesis: ((t3 `*` t2) `*` t1) ! a = (t3 `*` (t2 `*` t1)) ! a A6: <^(F2 . a),(F3 . a)^> <> {} by A3, Def1; A7: ( <^(F . a),(F1 . a)^> <> {} & <^(F1 . a),(F2 . a)^> <> {} ) by A1, A2, Def1; thus ((t3 `*` t2) `*` t1) ! a = ((t3 `*` t2) ! a) * (t1 ! a) by A1, A4, Def5 .= ((t3 ! a) * (t2 ! a)) * (t1 ! a) by A2, A3, Def5 .= (t3 ! a) * ((t2 ! a) * (t1 ! a)) by A7, A6, ALTCAT_1:21 .= (t3 ! a) * ((t2 `*` t1) ! a) by A1, A2, Def5 .= (t3 `*` (t2 `*` t1)) ! a by A3, A5, Def5 ; ::_thesis: verum end; hence (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) by A1, A4, Th2, Th3; ::_thesis: verum end; begin Lm1: for A, B being non empty transitive with_units AltCatStr for F, G being covariant Functor of A,B for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F, G being covariant Functor of A,B for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) let F, G be covariant Functor of A,B; ::_thesis: for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) ) assume A1: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) let f be Morphism of a,b; ::_thesis: ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) A2: <^a,a^> <> {} by ALTCAT_2:def_7; A3: <^b,b^> <> {} by ALTCAT_2:def_7; thus ((idt F) ! b) * (F . f) = (idm (F . b)) * (F . f) by Th4 .= (F . (idm b)) * (F . f) by Th1 .= F . ((idm b) * f) by A1, A3, FUNCTOR0:def_23 .= F . f by A1, ALTCAT_1:20 .= F . (f * (idm a)) by A1, ALTCAT_1:def_17 .= (F . f) * (F . (idm a)) by A1, A2, FUNCTOR0:def_23 .= (F . f) * (idm (F . a)) by Th1 .= (F . f) * ((idt F) ! a) by Th4 ; ::_thesis: verum end; definition let A, B be non empty transitive with_units AltCatStr ; let F1, F2 be covariant Functor of A,B; predF1 is_naturally_transformable_to F2 means :Def6: :: FUNCTOR2:def 6 ( F1 is_transformable_to F2 & ex t being transformation of F1,F2 st for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t ! b) * (F1 . f) = (F2 . f) * (t ! a) ); reflexivity for F1 being covariant Functor of A,B holds ( F1 is_transformable_to F1 & ex t being transformation of F1,F1 st for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t ! b) * (F1 . f) = (F1 . f) * (t ! a) ) proof let F be covariant Functor of A,B; ::_thesis: ( F is_transformable_to F & ex t being transformation of F,F st for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t ! b) * (F . f) = (F . f) * (t ! a) ) thus F is_transformable_to F ; ::_thesis: ex t being transformation of F,F st for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t ! b) * (F . f) = (F . f) * (t ! a) take idt F ; ::_thesis: for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) thus for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) by Lm1; ::_thesis: verum end; end; :: deftheorem Def6 defines is_naturally_transformable_to FUNCTOR2:def_6_:_ for A, B being non empty transitive with_units AltCatStr for F1, F2 being covariant Functor of A,B holds ( F1 is_naturally_transformable_to F2 iff ( F1 is_transformable_to F2 & ex t being transformation of F1,F2 st for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t ! b) * (F1 . f) = (F2 . f) * (t ! a) ) ); theorem :: FUNCTOR2:7 for A, B being non empty transitive with_units AltCatStr for F being covariant Functor of A,B holds F is_naturally_transformable_to F ; Lm2: for A, B being category for F, F1, F2 being covariant Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds for t1 being transformation of F,F1 st ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ) holds for t2 being transformation of F1,F2 st ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) proof let A, B be category; ::_thesis: for F, F1, F2 being covariant Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds for t1 being transformation of F,F1 st ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ) holds for t2 being transformation of F1,F2 st ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) let F, F1, F2 be covariant Functor of A,B; ::_thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 implies for t1 being transformation of F,F1 st ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ) holds for t2 being transformation of F1,F2 st ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) ) assume that A1: F is_transformable_to F1 and A2: F1 is_transformable_to F2 ; ::_thesis: for t1 being transformation of F,F1 st ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ) holds for t2 being transformation of F1,F2 st ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) let t1 be transformation of F,F1; ::_thesis: ( ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ) implies for t2 being transformation of F1,F2 st ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) ) assume A3: for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ; ::_thesis: for t2 being transformation of F1,F2 st ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) let t2 be transformation of F1,F2; ::_thesis: ( ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) implies for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) ) assume A4: for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ; ::_thesis: for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) ) A5: <^(F . b),(F1 . b)^> <> {} by A1, Def1; A6: <^(F . a),(F1 . a)^> <> {} by A1, Def1; A7: <^(F1 . b),(F2 . b)^> <> {} by A2, Def1; A8: <^(F1 . a),(F2 . a)^> <> {} by A2, Def1; assume A9: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) then A10: <^(F . a),(F . b)^> <> {} by FUNCTOR0:def_18; let f be Morphism of a,b; ::_thesis: ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) A11: <^(F2 . a),(F2 . b)^> <> {} by A9, FUNCTOR0:def_18; A12: <^(F1 . a),(F1 . b)^> <> {} by A9, FUNCTOR0:def_18; thus ((t2 `*` t1) ! b) * (F . f) = ((t2 ! b) * (t1 ! b)) * (F . f) by A1, A2, Def5 .= (t2 ! b) * ((t1 ! b) * (F . f)) by A10, A5, A7, ALTCAT_1:21 .= (t2 ! b) * ((F1 . f) * (t1 ! a)) by A3, A9 .= ((t2 ! b) * (F1 . f)) * (t1 ! a) by A6, A7, A12, ALTCAT_1:21 .= ((F2 . f) * (t2 ! a)) * (t1 ! a) by A4, A9 .= (F2 . f) * ((t2 ! a) * (t1 ! a)) by A6, A8, A11, ALTCAT_1:21 .= (F2 . f) * ((t2 `*` t1) ! a) by A1, A2, Def5 ; ::_thesis: verum end; theorem Th8: :: FUNCTOR2:8 for A, B being category for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds F is_naturally_transformable_to F2 proof let A, B be category; ::_thesis: for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds F is_naturally_transformable_to F2 let F, F1, F2 be covariant Functor of A,B; ::_thesis: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies F is_naturally_transformable_to F2 ) assume A1: F is_transformable_to F1 ; :: according to FUNCTOR2:def_6 ::_thesis: ( for t being transformation of F,F1 ex a, b being object of A st ( <^a,b^> <> {} & not for f being Morphism of a,b holds (t ! b) * (F . f) = (F1 . f) * (t ! a) ) or not F1 is_naturally_transformable_to F2 or F is_naturally_transformable_to F2 ) given t1 being transformation of F,F1 such that A2: for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ; ::_thesis: ( not F1 is_naturally_transformable_to F2 or F is_naturally_transformable_to F2 ) assume A3: F1 is_transformable_to F2 ; :: according to FUNCTOR2:def_6 ::_thesis: ( for t being transformation of F1,F2 ex a, b being object of A st ( <^a,b^> <> {} & not for f being Morphism of a,b holds (t ! b) * (F1 . f) = (F2 . f) * (t ! a) ) or F is_naturally_transformable_to F2 ) given t2 being transformation of F1,F2 such that A4: for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ; ::_thesis: F is_naturally_transformable_to F2 thus F is_transformable_to F2 by A1, A3, Th2; :: according to FUNCTOR2:def_6 ::_thesis: ex t being transformation of F,F2 st for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t ! b) * (F . f) = (F2 . f) * (t ! a) take t2 `*` t1 ; ::_thesis: for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) thus for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) by A1, A2, A3, A4, Lm2; ::_thesis: verum end; definition let A, B be non empty transitive with_units AltCatStr ; let F1, F2 be covariant Functor of A,B; assume A1: F1 is_naturally_transformable_to F2 ; mode natural_transformation of F1,F2 -> transformation of F1,F2 means :Def7: :: FUNCTOR2:def 7 for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (it ! b) * (F1 . f) = (F2 . f) * (it ! a); existence ex b1 being transformation of F1,F2 st for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (b1 ! b) * (F1 . f) = (F2 . f) * (b1 ! a) by A1, Def6; end; :: deftheorem Def7 defines natural_transformation FUNCTOR2:def_7_:_ for A, B being non empty transitive with_units AltCatStr for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 holds for b5 being transformation of F1,F2 holds ( b5 is natural_transformation of F1,F2 iff for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (b5 ! b) * (F1 . f) = (F2 . f) * (b5 ! a) ); definition let A, B be non empty transitive with_units AltCatStr ; let F be covariant Functor of A,B; :: original: idt redefine func idt F -> natural_transformation of F,F; coherence idt F is natural_transformation of F,F proof ( F is_naturally_transformable_to F & ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) ) ) by Lm1; hence idt F is natural_transformation of F,F by Def7; ::_thesis: verum end; end; definition let A, B be category; let F, F1, F2 be covariant Functor of A,B; assume B1: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 ) ; let t1 be natural_transformation of F,F1; let t2 be natural_transformation of F1,F2; funct2 `*` t1 -> natural_transformation of F,F2 means :Def8: :: FUNCTOR2:def 8 it = t2 `*` t1; existence ex b1 being natural_transformation of F,F2 st b1 = t2 `*` t1 proof A1: F is_naturally_transformable_to F2 by B1, Th8; A2: ( ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ) & ( for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) ) by B1, Def7; ( F is_transformable_to F1 & F1 is_transformable_to F2 ) by B1, Def6; then for a, b being object of A st <^a,b^> <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) by A2, Lm2; then t2 `*` t1 is natural_transformation of F,F2 by A1, Def7; hence ex b1 being natural_transformation of F,F2 st b1 = t2 `*` t1 ; ::_thesis: verum end; correctness uniqueness for b1, b2 being natural_transformation of F,F2 st b1 = t2 `*` t1 & b2 = t2 `*` t1 holds b1 = b2; ; end; :: deftheorem Def8 defines `*` FUNCTOR2:def_8_:_ for A, B being category for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds for t1 being natural_transformation of F,F1 for t2 being natural_transformation of F1,F2 for b8 being natural_transformation of F,F2 holds ( b8 = t2 `*` t1 iff b8 = t2 `*` t1 ); theorem :: FUNCTOR2:9 for A, B being non empty transitive with_units AltCatStr for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 holds for t being natural_transformation of F1,F2 holds ( (idt F2) `*` t = t & t `*` (idt F1) = t ) proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 holds for t being natural_transformation of F1,F2 holds ( (idt F2) `*` t = t & t `*` (idt F1) = t ) let F1, F2 be covariant Functor of A,B; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds ( (idt F2) `*` t = t & t `*` (idt F1) = t ) ) assume F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2 holds ( (idt F2) `*` t = t & t `*` (idt F1) = t ) then A1: F1 is_transformable_to F2 by Def6; let t be natural_transformation of F1,F2; ::_thesis: ( (idt F2) `*` t = t & t `*` (idt F1) = t ) thus (idt F2) `*` t = t by A1, Th5; ::_thesis: t `*` (idt F1) = t thus t `*` (idt F1) = t by A1, Th5; ::_thesis: verum end; theorem :: FUNCTOR2:10 for A, B being non empty transitive with_units AltCatStr for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds for t1 being natural_transformation of F,F1 for t2 being natural_transformation of F1,F2 for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a) proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds for t1 being natural_transformation of F,F1 for t2 being natural_transformation of F1,F2 for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a) let F, F1, F2 be covariant Functor of A,B; ::_thesis: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies for t1 being natural_transformation of F,F1 for t2 being natural_transformation of F1,F2 for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a) ) assume A1: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 ) ; ::_thesis: for t1 being natural_transformation of F,F1 for t2 being natural_transformation of F1,F2 for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a) let t1 be natural_transformation of F,F1; ::_thesis: for t2 being natural_transformation of F1,F2 for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a) let t2 be natural_transformation of F1,F2; ::_thesis: for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a) let a be object of A; ::_thesis: (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a) ( F is_transformable_to F1 & F1 is_transformable_to F2 ) by A1, Def6; hence (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a) by Def5; ::_thesis: verum end; theorem :: FUNCTOR2:11 for A, B being category for F, F1, F2, F3 being covariant Functor of A,B for t being natural_transformation of F,F1 for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) proof let A, B be category; ::_thesis: for F, F1, F2, F3 being covariant Functor of A,B for t being natural_transformation of F,F1 for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) let F, F1, F2, F3 be covariant Functor of A,B; ::_thesis: for t being natural_transformation of F,F1 for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) let t be natural_transformation of F,F1; ::_thesis: for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) let t1 be natural_transformation of F1,F2; ::_thesis: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) ) assume that A1: F is_naturally_transformable_to F1 and A2: F1 is_naturally_transformable_to F2 and A3: F2 is_naturally_transformable_to F3 ; ::_thesis: for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) A4: F is_naturally_transformable_to F2 by A1, A2, Th8; let t3 be natural_transformation of F2,F3; ::_thesis: (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) A5: F2 is_transformable_to F3 by A3, Def6; A6: ( F is_transformable_to F1 & F1 is_transformable_to F2 ) by A1, A2, Def6; F1 is_naturally_transformable_to F3 by A2, A3, Th8; hence (t3 `*` t1) `*` t = (t3 `*` t1) `*` t by A1, Def8 .= (t3 `*` t1) `*` t by A2, A3, Def8 .= t3 `*` (t1 `*` t) by A6, A5, Th6 .= t3 `*` (t1 `*` t) by A1, A2, Def8 .= t3 `*` (t1 `*` t) by A3, A4, Def8 ; ::_thesis: verum end; begin definition let I be set ; let A, B be ManySortedSet of I; func Funcs (A,B) -> set means :Def9: :: FUNCTOR2:def 9 for x being set holds ( x in it iff x is ManySortedFunction of A,B ) if for i being set st i in I & B . i = {} holds A . i = {} otherwise it = {} ; existence ( ( ( for i being set st i in I & B . i = {} holds A . i = {} ) implies ex b1 being set st for x being set holds ( x in b1 iff x is ManySortedFunction of A,B ) ) & ( ex i being set st ( i in I & B . i = {} & not A . i = {} ) implies ex b1 being set st b1 = {} ) ) proof thus ( ( for i being set st i in I & B . i = {} holds A . i = {} ) implies ex IT being set st for x being set holds ( x in IT iff x is ManySortedFunction of A,B ) ) ::_thesis: ( ex i being set st ( i in I & B . i = {} & not A . i = {} ) implies ex b1 being set st b1 = {} ) proof deffunc H1( set ) -> set = Funcs ((A . \$1),(B . \$1)); assume A1: for i being set st i in I & B . i = {} holds A . i = {} ; ::_thesis: ex IT being set st for x being set holds ( x in IT iff x is ManySortedFunction of A,B ) consider F being ManySortedSet of I such that A2: for i being set st i in I holds F . i = H1(i) from PBOOLE:sch_4(); take product F ; ::_thesis: for x being set holds ( x in product F iff x is ManySortedFunction of A,B ) let x be set ; ::_thesis: ( x in product F iff x is ManySortedFunction of A,B ) thus ( x in product F implies x is ManySortedFunction of A,B ) ::_thesis: ( x is ManySortedFunction of A,B implies x in product F ) proof assume x in product F ; ::_thesis: x is ManySortedFunction of A,B then consider g being Function such that A3: x = g and A4: dom g = dom F and A5: for i being set st i in dom F holds g . i in F . i by CARD_3:def_5; A6: for i being set st i in I holds g . i is Function of (A . i),(B . i) proof let i be set ; ::_thesis: ( i in I implies g . i is Function of (A . i),(B . i) ) assume A7: i in I ; ::_thesis: g . i is Function of (A . i),(B . i) ( dom F = I & F . i = Funcs ((A . i),(B . i)) ) by A2, A7, PARTFUN1:def_2; hence g . i is Function of (A . i),(B . i) by A5, A7, FUNCT_2:66; ::_thesis: verum end; dom F = I by PARTFUN1:def_2; then reconsider g = g as ManySortedSet of I by A4, PARTFUN1:def_2, RELAT_1:def_18; g is ManySortedFunction of A,B by A6, PBOOLE:def_15; hence x is ManySortedFunction of A,B by A3; ::_thesis: verum end; assume A8: x is ManySortedFunction of A,B ; ::_thesis: x in product F then reconsider g = x as ManySortedSet of I ; A9: for i being set st i in I holds g . i in Funcs ((A . i),(B . i)) proof let i be set ; ::_thesis: ( i in I implies g . i in Funcs ((A . i),(B . i)) ) assume A10: i in I ; ::_thesis: g . i in Funcs ((A . i),(B . i)) then A11: ( B . i = {} implies A . i = {} ) by A1; g . i is Function of (A . i),(B . i) by A8, A10, PBOOLE:def_15; hence g . i in Funcs ((A . i),(B . i)) by A11, FUNCT_2:8; ::_thesis: verum end; A12: for i being set st i in I holds g . i in F . i proof let i be set ; ::_thesis: ( i in I implies g . i in F . i ) assume A13: i in I ; ::_thesis: g . i in F . i then F . i = Funcs ((A . i),(B . i)) by A2; hence g . i in F . i by A9, A13; ::_thesis: verum end; A14: for i being set st i in dom F holds g . i in F . i proof A15: dom F = I by PARTFUN1:def_2; let i be set ; ::_thesis: ( i in dom F implies g . i in F . i ) assume i in dom F ; ::_thesis: g . i in F . i hence g . i in F . i by A12, A15; ::_thesis: verum end; dom g = I by PARTFUN1:def_2; then dom g = dom F by PARTFUN1:def_2; hence x in product F by A14, CARD_3:def_5; ::_thesis: verum end; thus ( ex i being set st ( i in I & B . i = {} & not A . i = {} ) implies ex b1 being set st b1 = {} ) ; ::_thesis: verum end; uniqueness for b1, b2 being set holds ( ( ( for i being set st i in I & B . i = {} holds A . i = {} ) & ( for x being set holds ( x in b1 iff x is ManySortedFunction of A,B ) ) & ( for x being set holds ( x in b2 iff x is ManySortedFunction of A,B ) ) implies b1 = b2 ) & ( ex i being set st ( i in I & B . i = {} & not A . i = {} ) & b1 = {} & b2 = {} implies b1 = b2 ) ) proof let it1, it2 be set ; ::_thesis: ( ( ( for i being set st i in I & B . i = {} holds A . i = {} ) & ( for x being set holds ( x in it1 iff x is ManySortedFunction of A,B ) ) & ( for x being set holds ( x in it2 iff x is ManySortedFunction of A,B ) ) implies it1 = it2 ) & ( ex i being set st ( i in I & B . i = {} & not A . i = {} ) & it1 = {} & it2 = {} implies it1 = it2 ) ) hereby ::_thesis: ( ex i being set st ( i in I & B . i = {} & not A . i = {} ) & it1 = {} & it2 = {} implies it1 = it2 ) assume for i being set st i in I & B . i = {} holds A . i = {} ; ::_thesis: ( ( for x being set holds ( x in it1 iff x is ManySortedFunction of A,B ) ) & ( for x being set holds ( x in it2 iff x is ManySortedFunction of A,B ) ) implies it1 = it2 ) assume that A16: for x being set holds ( x in it1 iff x is ManySortedFunction of A,B ) and A17: for x being set holds ( x in it2 iff x is ManySortedFunction of A,B ) ; ::_thesis: it1 = it2 now__::_thesis:_for_x_being_set_holds_ (_x_in_it1_iff_x_in_it2_) let x be set ; ::_thesis: ( x in it1 iff x in it2 ) ( x in it1 iff x is ManySortedFunction of A,B ) by A16; hence ( x in it1 iff x in it2 ) by A17; ::_thesis: verum end; hence it1 = it2 by TARSKI:1; ::_thesis: verum end; thus ( ex i being set st ( i in I & B . i = {} & not A . i = {} ) & it1 = {} & it2 = {} implies it1 = it2 ) ; ::_thesis: verum end; consistency for b1 being set holds verum ; end; :: deftheorem Def9 defines Funcs FUNCTOR2:def_9_:_ for I being set for A, B being ManySortedSet of I for b4 being set holds ( ( ( for i being set st i in I & B . i = {} holds A . i = {} ) implies ( b4 = Funcs (A,B) iff for x being set holds ( x in b4 iff x is ManySortedFunction of A,B ) ) ) & ( ex i being set st ( i in I & B . i = {} & not A . i = {} ) implies ( b4 = Funcs (A,B) iff b4 = {} ) ) ); definition let A, B be non empty transitive with_units AltCatStr ; func Funct (A,B) -> set means :Def10: :: FUNCTOR2:def 10 for x being set holds ( x in it iff x is strict covariant Functor of A,B ); existence ex b1 being set st for x being set holds ( x in b1 iff x is strict covariant Functor of A,B ) proof set A9 = Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]); set sAA = { ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum } ; set f = the Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]); the Arrows of B * the Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) in { ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum } ; then reconsider sAA = { ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum } as non empty set ; defpred S1[ set , set ] means ex f being Covariant bifunction of the carrier of A, the carrier of B ex m being MSUnTrans of f, the Arrows of A, the Arrows of B st ( \$1 = [f,m] & \$2 = FunctorStr(# f,m #) & \$2 is covariant Functor of A,B ); defpred S2[ set , set ] means ex AA being ManySortedSet of [: the carrier of A, the carrier of A:] st ( \$1 = AA & \$2 = Funcs ( the Arrows of A,AA) ); A1: for x, y, z being set st S2[x,y] & S2[x,z] holds y = z ; consider XX being set such that A2: for x being set holds ( x in XX iff ex y being set st ( y in sAA & S2[y,x] ) ) from TARSKI:sch_1(A1); A3: for x, y, z being set st S1[x,y] & S1[x,z] holds y = z proof let x, y, z be set ; ::_thesis: ( S1[x,y] & S1[x,z] implies y = z ) given f being Covariant bifunction of the carrier of A, the carrier of B, m being MSUnTrans of f, the Arrows of A, the Arrows of B such that A4: x = [f,m] and A5: y = FunctorStr(# f,m #) and y is covariant Functor of A,B ; ::_thesis: ( not S1[x,z] or y = z ) given f1 being Covariant bifunction of the carrier of A, the carrier of B, m1 being MSUnTrans of f1, the Arrows of A, the Arrows of B such that A6: x = [f1,m1] and A7: z = FunctorStr(# f1,m1 #) and z is covariant Functor of A,B ; ::_thesis: y = z f = f1 by A4, A6, XTUPLE_0:1; hence y = z by A4, A5, A6, A7, XTUPLE_0:1; ::_thesis: verum end; consider X being set such that A8: for x being set holds ( x in X iff ex y being set st ( y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] & S1[y,x] ) ) from TARSKI:sch_1(A3); take X ; ::_thesis: for x being set holds ( x in X iff x is strict covariant Functor of A,B ) let x be set ; ::_thesis: ( x in X iff x is strict covariant Functor of A,B ) thus ( x in X implies x is strict covariant Functor of A,B ) ::_thesis: ( x is strict covariant Functor of A,B implies x in X ) proof assume x in X ; ::_thesis: x is strict covariant Functor of A,B then ex y being set st ( y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] & ex f being Covariant bifunction of the carrier of A, the carrier of B ex m being MSUnTrans of f, the Arrows of A, the Arrows of B st ( y = [f,m] & x = FunctorStr(# f,m #) & x is covariant Functor of A,B ) ) by A8; hence x is strict covariant Functor of A,B ; ::_thesis: verum end; assume x is strict covariant Functor of A,B ; ::_thesis: x in X then reconsider F = x as strict covariant Functor of A,B ; reconsider f = the ObjectMap of F as Covariant bifunction of the carrier of A, the carrier of B by FUNCTOR0:def_12; reconsider m = the MorphMap of F as MSUnTrans of f, the Arrows of A, the Arrows of B ; reconsider y = [f,m] as set ; A9: for o1, o2 being object of A st the Arrows of A . (o1,o2) <> {} holds the Arrows of B . (f . (o1,o2)) <> {} proof let o1, o2 be object of A; ::_thesis: ( the Arrows of A . (o1,o2) <> {} implies the Arrows of B . (f . (o1,o2)) <> {} ) assume A10: the Arrows of A . (o1,o2) <> {} ; ::_thesis: the Arrows of B . (f . (o1,o2)) <> {} the Arrows of A . (o1,o2) = <^o1,o2^> ; hence the Arrows of B . (f . (o1,o2)) <> {} by A10, FUNCTOR0:def_11; ::_thesis: verum end; A11: for o1, o2 being object of A st the Arrows of A . (o1,o2) <> {} holds the Arrows of B . [(F . o1),(F . o2)] <> {} proof let o1, o2 be object of A; ::_thesis: ( the Arrows of A . (o1,o2) <> {} implies the Arrows of B . [(F . o1),(F . o2)] <> {} ) assume A12: the Arrows of A . (o1,o2) <> {} ; ::_thesis: the Arrows of B . [(F . o1),(F . o2)] <> {} f . (o1,o2) = [(F . o1),(F . o2)] by FUNCTOR0:22; hence the Arrows of B . [(F . o1),(F . o2)] <> {} by A9, A12; ::_thesis: verum end; y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] proof set I = [: the carrier of A, the carrier of A:]; reconsider AA = the Arrows of B * f as ManySortedSet of [: the carrier of A, the carrier of A:] ; A13: for i being set st i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} holds the Arrows of B . (f . i) <> {} proof let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} implies the Arrows of B . (f . i) <> {} ) assume that A14: i in [: the carrier of A, the carrier of A:] and A15: the Arrows of A . i <> {} ; ::_thesis: the Arrows of B . (f . i) <> {} consider o1, o2 being set such that A16: ( o1 in the carrier of A & o2 in the carrier of A ) and A17: i = [o1,o2] by A14, ZFMISC_1:def_2; reconsider a1 = o1, a2 = o2 as object of A by A16; A18: the Arrows of B . (f . i) = the Arrows of B . (f . (o1,o2)) by A17 .= the Arrows of B . [(F . a1),(F . a2)] by FUNCTOR0:22 ; the Arrows of A . (o1,o2) <> {} by A15, A17; hence the Arrows of B . (f . i) <> {} by A11, A18; ::_thesis: verum end; for i being set st i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} holds AA . i <> {} proof let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} implies AA . i <> {} ) assume A19: i in [: the carrier of A, the carrier of A:] ; ::_thesis: ( not the Arrows of A . i <> {} or AA . i <> {} ) assume A20: the Arrows of A . i <> {} ; ::_thesis: AA . i <> {} AA . i = the Arrows of B . (f . i) by A19, FUNCT_2:15; hence AA . i <> {} by A13, A19, A20; ::_thesis: verum end; then ( m is ManySortedFunction of the Arrows of A,AA & ( for i being set st i in [: the carrier of A, the carrier of A:] & AA . i = {} holds the Arrows of A . i = {} ) ) by FUNCTOR0:def_4; then A21: m in Funcs ( the Arrows of A,AA) by Def9; A22: f in Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) by FUNCT_2:8; then the Arrows of B * f in sAA ; then Funcs ( the Arrows of A,AA) in XX by A2; then m in union XX by A21, TARSKI:def_4; hence y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] by A22, ZFMISC_1:def_2; ::_thesis: verum end; hence x in X by A8; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is strict covariant Functor of A,B ) ) & ( for x being set holds ( x in b2 iff x is strict covariant Functor of A,B ) ) holds b1 = b2 proof let it1, it2 be set ; ::_thesis: ( ( for x being set holds ( x in it1 iff x is strict covariant Functor of A,B ) ) & ( for x being set holds ( x in it2 iff x is strict covariant Functor of A,B ) ) implies it1 = it2 ) assume that A23: for x being set holds ( x in it1 iff x is strict covariant Functor of A,B ) and A24: for x being set holds ( x in it2 iff x is strict covariant Functor of A,B ) ; ::_thesis: it1 = it2 now__::_thesis:_for_x_being_set_holds_ (_x_in_it1_iff_x_in_it2_) let x be set ; ::_thesis: ( x in it1 iff x in it2 ) ( x in it1 iff x is strict covariant Functor of A,B ) by A23; hence ( x in it1 iff x in it2 ) by A24; ::_thesis: verum end; hence it1 = it2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def10 defines Funct FUNCTOR2:def_10_:_ for A, B being non empty transitive with_units AltCatStr for b3 being set holds ( b3 = Funct (A,B) iff for x being set holds ( x in b3 iff x is strict covariant Functor of A,B ) ); definition let A, B be category; func Functors (A,B) -> non empty transitive strict AltCatStr means :: FUNCTOR2:def 11 ( the carrier of it = Funct (A,B) & ( for F, G being strict covariant Functor of A,B for x being set holds ( x in the Arrows of it . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 being natural_transformation of F,G for t2 being natural_transformation of G,H ex f being Function st ( f = the Comp of it . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) ); existence ex b1 being non empty transitive strict AltCatStr st ( the carrier of b1 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B for x being set holds ( x in the Arrows of b1 . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 being natural_transformation of F,G for t2 being natural_transformation of G,H ex f being Function st ( f = the Comp of b1 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) ) proof defpred S1[ set , set , set ] means for f, g, h being strict covariant Functor of A,B st [f,g,h] = \$3 holds for t1 being natural_transformation of f,g for t2 being natural_transformation of g,h st [t2,t1] = \$2 & ex v being Function st v . \$2 = \$1 holds \$1 = t2 `*` t1; defpred S2[ set , set ] means for f, g being strict covariant Functor of A,B st [f,g] = \$1 holds for x being set holds ( x in \$2 iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ); A1: for i being set st i in [:(Funct (A,B)),(Funct (A,B)):] holds ex j being set st S2[i,j] proof let i be set ; ::_thesis: ( i in [:(Funct (A,B)),(Funct (A,B)):] implies ex j being set st S2[i,j] ) assume i in [:(Funct (A,B)),(Funct (A,B)):] ; ::_thesis: ex j being set st S2[i,j] then consider f, g being set such that A2: ( f in Funct (A,B) & g in Funct (A,B) ) and A3: i = [f,g] by ZFMISC_1:def_2; reconsider f = f, g = g as strict covariant Functor of A,B by A2, Def10; defpred S3[ object of A, set ] means \$2 = <^(f . \$1),(g . \$1)^>; defpred S4[ set ] means ( f is_naturally_transformable_to g & \$1 is natural_transformation of f,g ); A4: for a being Element of A ex j being set st S3[a,j] ; consider N being ManySortedSet of the carrier of A such that A5: for a being Element of A holds S3[a,N . a] from PBOOLE:sch_6(A4); consider j being set such that A6: for x being set holds ( x in j iff ( x in product N & S4[x] ) ) from XBOOLE_0:sch_1(); take j ; ::_thesis: S2[i,j] let f9, g9 be strict covariant Functor of A,B; ::_thesis: ( [f9,g9] = i implies for x being set holds ( x in j iff ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) ) ) assume A7: [f9,g9] = i ; ::_thesis: for x being set holds ( x in j iff ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) ) let x be set ; ::_thesis: ( x in j iff ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) ) thus ( x in j implies ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) ) ::_thesis: ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 implies x in j ) proof assume A8: x in j ; ::_thesis: ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) ( f9 = f & g9 = g ) by A3, A7, XTUPLE_0:1; hence ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) by A6, A8; ::_thesis: verum end; thus ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 implies x in j ) ::_thesis: verum proof A9: ( f9 = f & g9 = g ) by A3, A7, XTUPLE_0:1; set I = the carrier of A; assume that A10: f9 is_naturally_transformable_to g9 and A11: x is natural_transformation of f9,g9 ; ::_thesis: x in j reconsider h = x as ManySortedSet of the carrier of A by A11; A12: f9 is_transformable_to g9 by A10, Def6; A13: for i9 being set st i9 in the carrier of A holds h . i9 in N . i9 proof let i9 be set ; ::_thesis: ( i9 in the carrier of A implies h . i9 in N . i9 ) assume i9 in the carrier of A ; ::_thesis: h . i9 in N . i9 then reconsider i9 = i9 as Element of A ; A14: S3[i9,N . i9] by A5; ( <^(f . i9),(g . i9)^> <> {} & h . i9 is Element of <^(f . i9),(g . i9)^> ) by A11, A12, A9, Def1, Def2; hence h . i9 in N . i9 by A14; ::_thesis: verum end; A15: for i9 being set st i9 in dom N holds h . i9 in N . i9 proof A16: dom N = the carrier of A by PARTFUN1:def_2; let i9 be set ; ::_thesis: ( i9 in dom N implies h . i9 in N . i9 ) assume i9 in dom N ; ::_thesis: h . i9 in N . i9 hence h . i9 in N . i9 by A13, A16; ::_thesis: verum end; dom h = the carrier of A by PARTFUN1:def_2; then dom h = dom N by PARTFUN1:def_2; then x in product N by A15, CARD_3:9; hence x in j by A6, A10, A11, A9; ::_thesis: verum end; end; consider a being ManySortedSet of [:(Funct (A,B)),(Funct (A,B)):] such that A17: for i being set st i in [:(Funct (A,B)),(Funct (A,B)):] holds S2[i,a . i] from PBOOLE:sch_3(A1); A18: for o being set st o in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] holds for x being set st x in {|a,a|} . o holds ex y being set st ( y in {|a|} . o & S1[y,x,o] ) proof let o be set ; ::_thesis: ( o in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] implies for x being set st x in {|a,a|} . o holds ex y being set st ( y in {|a|} . o & S1[y,x,o] ) ) assume o in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] ; ::_thesis: for x being set st x in {|a,a|} . o holds ex y being set st ( y in {|a|} . o & S1[y,x,o] ) then o in [:[:(Funct (A,B)),(Funct (A,B)):],(Funct (A,B)):] by ZFMISC_1:def_3; then consider ff, h being set such that A19: ff in [:(Funct (A,B)),(Funct (A,B)):] and A20: h in Funct (A,B) and A21: o = [ff,h] by ZFMISC_1:def_2; consider f, g being set such that A22: ( f in Funct (A,B) & g in Funct (A,B) ) and A23: ff = [f,g] by A19, ZFMISC_1:def_2; A24: o = [f,g,h] by A21, A23; reconsider T = Funct (A,B) as non empty set by A20; reconsider i = f, j = g, k = h as Element of T by A20, A22; A25: {|a|} . [i,j,k] = {|a|} . (i,j,k) by MULTOP_1:def_1 .= a . (i,k) by ALTCAT_1:def_3 ; A26: {|a,a|} . [i,j,k] = {|a,a|} . (i,j,k) by MULTOP_1:def_1 .= [:(a . (j,k)),(a . (i,j)):] by ALTCAT_1:def_4 ; for x being set st x in {|a,a|} . o holds ex y being set st ( y in {|a|} . o & S1[y,x,o] ) proof reconsider i9 = i, j9 = j, k9 = k as strict covariant Functor of A,B by Def10; let x be set ; ::_thesis: ( x in {|a,a|} . o implies ex y being set st ( y in {|a|} . o & S1[y,x,o] ) ) A27: [i9,k9] in [:(Funct (A,B)),(Funct (A,B)):] by ZFMISC_1:def_2; assume x in {|a,a|} . o ; ::_thesis: ex y being set st ( y in {|a|} . o & S1[y,x,o] ) then consider x2, x1 being set such that A28: x2 in a . (j,k) and A29: x1 in a . (i,j) and A30: x = [x2,x1] by A24, A26, ZFMISC_1:def_2; A31: x2 in a . [j,k] by A28; then A32: j9 is_naturally_transformable_to k9 by A17; reconsider x2 = x2 as natural_transformation of j9,k9 by A17, A31; A33: x1 in a . [i,j] by A29; then reconsider x1 = x1 as natural_transformation of i9,j9 by A17; reconsider vv = x2 `*` x1 as natural_transformation of i9,k9 ; A34: for f, g, h being strict covariant Functor of A,B st [f,g,h] = o holds for t1 being natural_transformation of f,g for t2 being natural_transformation of g,h st [t2,t1] = x & ex v being Function st v . x = vv holds vv = t2 `*` t1 proof let f, g, h be strict covariant Functor of A,B; ::_thesis: ( [f,g,h] = o implies for t1 being natural_transformation of f,g for t2 being natural_transformation of g,h st [t2,t1] = x & ex v being Function st v . x = vv holds vv = t2 `*` t1 ) assume A35: [f,g,h] = o ; ::_thesis: for t1 being natural_transformation of f,g for t2 being natural_transformation of g,h st [t2,t1] = x & ex v being Function st v . x = vv holds vv = t2 `*` t1 A36: j9 = g by A24, A35, XTUPLE_0:3; then reconsider x2 = x2 as natural_transformation of g,h by A24, A35, XTUPLE_0:3; A37: ( i9 = f & k9 = h ) by A24, A35, XTUPLE_0:3; let t1 be natural_transformation of f,g; ::_thesis: for t2 being natural_transformation of g,h st [t2,t1] = x & ex v being Function st v . x = vv holds vv = t2 `*` t1 let t2 be natural_transformation of g,h; ::_thesis: ( [t2,t1] = x & ex v being Function st v . x = vv implies vv = t2 `*` t1 ) assume that A38: [t2,t1] = x and ex v being Function st v . x = vv ; ::_thesis: vv = t2 `*` t1 x2 = t2 by A30, A38, XTUPLE_0:1; hence vv = t2 `*` t1 by A30, A38, A36, A37, XTUPLE_0:1; ::_thesis: verum end; i9 is_naturally_transformable_to j9 by A17, A33; then i9 is_naturally_transformable_to k9 by A32, Th8; then vv in a . [i9,k9] by A17, A27; hence ex y being set st ( y in {|a|} . o & S1[y,x,o] ) by A24, A25, A34; ::_thesis: verum end; hence for x being set st x in {|a,a|} . o holds ex y being set st ( y in {|a|} . o & S1[y,x,o] ) ; ::_thesis: verum end; consider c being ManySortedFunction of {|a,a|},{|a|} such that A39: for i being set st i in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] holds ex v being Function of ({|a,a|} . i),({|a|} . i) st ( v = c . i & ( for x being set st x in {|a,a|} . i holds S1[v . x,x,i] ) ) from MSSUBFAM:sch_1(A18); set F = AltCatStr(# (Funct (A,B)),a,c #); A40: not Funct (A,B) is empty proof set f = the strict covariant Functor of A,B; the strict covariant Functor of A,B in Funct (A,B) by Def10; hence not Funct (A,B) is empty ; ::_thesis: verum end; AltCatStr(# (Funct (A,B)),a,c #) is transitive proof let o1, o2, o3 be object of AltCatStr(# (Funct (A,B)),a,c #); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} ) reconsider a1 = o1, a2 = o2, a3 = o3 as strict covariant Functor of A,B by A40, Def10; assume that A41: <^o1,o2^> <> {} and A42: <^o2,o3^> <> {} ; ::_thesis: not <^o1,o3^> = {} consider x being set such that A43: x in a . [o2,o3] by A42, XBOOLE_0:def_1; A44: [o2,o3] in [:(Funct (A,B)),(Funct (A,B)):] by A40, ZFMISC_1:def_2; then A45: a2 is_naturally_transformable_to a3 by A17, A43; reconsider x = x as natural_transformation of a2,a3 by A17, A44, A43; consider y being set such that A46: y in a . [o1,o2] by A41, XBOOLE_0:def_1; A47: [o1,o2] in [:(Funct (A,B)),(Funct (A,B)):] by A40, ZFMISC_1:def_2; then reconsider y = y as natural_transformation of a1,a2 by A17, A46; a1 is_naturally_transformable_to a2 by A17, A47, A46; then A48: a1 is_naturally_transformable_to a3 by A45, Th8; ( x `*` y is natural_transformation of a1,a3 & [o1,o3] in [:(Funct (A,B)),(Funct (A,B)):] ) by A40, ZFMISC_1:def_2; hence not <^o1,o3^> = {} by A17, A48; ::_thesis: verum end; then reconsider F = AltCatStr(# (Funct (A,B)),a,c #) as non empty transitive strict AltCatStr by A40; take F ; ::_thesis: ( the carrier of F = Funct (A,B) & ( for F, G being strict covariant Functor of A,B for x being set holds ( x in the Arrows of F . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 being natural_transformation of F,G for t2 being natural_transformation of G,H ex f being Function st ( f = the Comp of F . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) ) thus the carrier of F = Funct (A,B) ; ::_thesis: ( ( for F, G being strict covariant Functor of A,B for x being set holds ( x in the Arrows of F . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 being natural_transformation of F,G for t2 being natural_transformation of G,H ex f being Function st ( f = the Comp of F . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) ) thus for f, g being strict covariant Functor of A,B for x being set holds ( x in the Arrows of F . (f,g) iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) ::_thesis: for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 being natural_transformation of F,G for t2 being natural_transformation of G,H ex f being Function st ( f = the Comp of F . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) proof let f, g be strict covariant Functor of A,B; ::_thesis: for x being set holds ( x in the Arrows of F . (f,g) iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) let x be set ; ::_thesis: ( x in the Arrows of F . (f,g) iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) thus ( x in the Arrows of F . (f,g) implies ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) ::_thesis: ( f is_naturally_transformable_to g & x is natural_transformation of f,g implies x in the Arrows of F . (f,g) ) proof ( f in Funct (A,B) & g in Funct (A,B) ) by Def10; then A49: [f,g] in [:(Funct (A,B)),(Funct (A,B)):] by ZFMISC_1:def_2; assume x in the Arrows of F . (f,g) ; ::_thesis: ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) hence ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) by A17, A49; ::_thesis: verum end; thus ( f is_naturally_transformable_to g & x is natural_transformation of f,g implies x in the Arrows of F . (f,g) ) ::_thesis: verum proof ( f in Funct (A,B) & g in Funct (A,B) ) by Def10; then A50: [f,g] in [:(Funct (A,B)),(Funct (A,B)):] by ZFMISC_1:87; assume ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ; ::_thesis: x in the Arrows of F . (f,g) hence x in the Arrows of F . (f,g) by A17, A50; ::_thesis: verum end; end; let f, g, h be strict covariant Functor of A,B; ::_thesis: ( f is_naturally_transformable_to g & g is_naturally_transformable_to h implies for t1 being natural_transformation of f,g for t2 being natural_transformation of g,h ex f being Function st ( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 ) ) assume that A51: f is_naturally_transformable_to g and A52: g is_naturally_transformable_to h ; ::_thesis: for t1 being natural_transformation of f,g for t2 being natural_transformation of g,h ex f being Function st ( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 ) let t1 be natural_transformation of f,g; ::_thesis: for t2 being natural_transformation of g,h ex f being Function st ( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 ) let t2 be natural_transformation of g,h; ::_thesis: ex f being Function st ( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 ) A53: f in Funct (A,B) by Def10; then reconsider T = Funct (A,B) as non empty set ; A54: g in Funct (A,B) by Def10; then A55: [f,g] in [:(Funct (A,B)),(Funct (A,B)):] by A53, ZFMISC_1:87; A56: h in Funct (A,B) by Def10; then [g,h] in [:(Funct (A,B)),(Funct (A,B)):] by A54, ZFMISC_1:87; then A57: t2 in a . [g,h] by A17, A52; reconsider i = f, j = g, k = h as Element of T by Def10; A58: {|a,a|} . [i,j,k] = {|a,a|} . (i,j,k) by MULTOP_1:def_1 .= [:(a . (j,k)),(a . (i,j)):] by ALTCAT_1:def_4 ; ( [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] = [:[:(Funct (A,B)),(Funct (A,B)):],(Funct (A,B)):] & [f,g,h] = [[f,g],h] ) by ZFMISC_1:def_3; then [f,g,h] in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] by A56, A55, ZFMISC_1:87; then consider v being Function of ({|a,a|} . [f,g,h]),({|a|} . [f,g,h]) such that A59: v = c . [f,g,h] and A60: for x being set st x in {|a,a|} . [f,g,h] holds S1[v . x,x,[f,g,h]] by A39; t1 in a . [f,g] by A17, A51, A55; then [t2,t1] in {|a,a|} . [f,g,h] by A58, A57, ZFMISC_1:87; then A61: v . (t2,t1) = t2 `*` t1 by A60; v = c . (f,g,h) by A59, MULTOP_1:def_1; hence ex f being Function st ( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 ) by A61; ::_thesis: verum end; uniqueness for b1, b2 being non empty transitive strict AltCatStr st the carrier of b1 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B for x being set holds ( x in the Arrows of b1 . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 being natural_transformation of F,G for t2 being natural_transformation of G,H ex f being Function st ( f = the Comp of b1 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) & the carrier of b2 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B for x being set holds ( x in the Arrows of b2 . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 being natural_transformation of F,G for t2 being natural_transformation of G,H ex f being Function st ( f = the Comp of b2 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) holds b1 = b2 proof let C1, C2 be non empty transitive strict AltCatStr ; ::_thesis: ( the carrier of C1 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B for x being set holds ( x in the Arrows of C1 . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 being natural_transformation of F,G for t2 being natural_transformation of G,H ex f being Function st ( f = the Comp of C1 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) & the carrier of C2 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B for x being set holds ( x in the Arrows of C2 . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 being natural_transformation of F,G for t2 being natural_transformation of G,H ex f being Function st ( f = the Comp of C2 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) implies C1 = C2 ) assume that A62: the carrier of C1 = Funct (A,B) and A63: for F, G being strict covariant Functor of A,B for x being set holds ( x in the Arrows of C1 . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) and A64: for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 being natural_transformation of F,G for t2 being natural_transformation of G,H ex f being Function st ( f = the Comp of C1 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) and A65: the carrier of C2 = Funct (A,B) and A66: for F, G being strict covariant Functor of A,B for x being set holds ( x in the Arrows of C2 . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) and A67: for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 being natural_transformation of F,G for t2 being natural_transformation of G,H ex f being Function st ( f = the Comp of C2 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ; ::_thesis: C1 = C2 set R = the carrier of C1; set T = the carrier of C2; set N = the Arrows of C1; set M = the Arrows of C2; set O = the Comp of C1; set P = the Comp of C2; A68: for i, j being set st i in the carrier of C1 & j in the carrier of C2 holds the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j) proof let i, j be set ; ::_thesis: ( i in the carrier of C1 & j in the carrier of C2 implies the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j) ) assume that A69: i in the carrier of C1 and A70: j in the carrier of C2 ; ::_thesis: the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j) reconsider g = j as strict covariant Functor of A,B by A65, A70, Def10; reconsider f = i as strict covariant Functor of A,B by A62, A69, Def10; now__::_thesis:_for_x_being_set_holds_ (_x_in_the_Arrows_of_C1_._(i,j)_iff_x_in_the_Arrows_of_C2_._(i,j)_) let x be set ; ::_thesis: ( x in the Arrows of C1 . (i,j) iff x in the Arrows of C2 . (i,j) ) ( x in the Arrows of C1 . (i,j) iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) by A63; hence ( x in the Arrows of C1 . (i,j) iff x in the Arrows of C2 . (i,j) ) by A66; ::_thesis: verum end; hence the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j) by TARSKI:1; ::_thesis: verum end; then A71: the Arrows of C1 = the Arrows of C2 by A62, A65, ALTCAT_1:6; for i, j, k being set st i in the carrier of C1 & j in the carrier of C1 & k in the carrier of C1 holds the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) proof let i, j, k be set ; ::_thesis: ( i in the carrier of C1 & j in the carrier of C1 & k in the carrier of C1 implies the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) ) assume that A72: i in the carrier of C1 and A73: j in the carrier of C1 and A74: k in the carrier of C1 ; ::_thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) reconsider h = k as strict covariant Functor of A,B by A62, A74, Def10; reconsider g = j as strict covariant Functor of A,B by A62, A73, Def10; reconsider f = i as strict covariant Functor of A,B by A62, A72, Def10; percases ( the Arrows of C1 . (i,j) = {} or the Arrows of C1 . (j,k) = {} or ( the Arrows of C1 . (i,j) <> {} & the Arrows of C1 . (j,k) <> {} ) ) ; supposeA75: ( the Arrows of C1 . (i,j) = {} or the Arrows of C1 . (j,k) = {} ) ; ::_thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) thus the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) ::_thesis: verum proof percases ( the Arrows of C1 . (i,j) = {} or the Arrows of C1 . (j,k) = {} ) by A75; supposeA76: the Arrows of C1 . (i,j) = {} ; ::_thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) reconsider T = the carrier of C2 as non empty set ; reconsider i9 = i, j9 = j, k9 = k as Element of T by A62, A65, A72, A73, A74; the Arrows of C2 . (i,j) = {} by A62, A65, A68, A76, ALTCAT_1:6; then A77: [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] = {} by ZFMISC_1:90; A78: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1 .= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def_4 ; A79: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1 .= the Arrows of C2 . (i9,k9) by ALTCAT_1:def_3 ; the Comp of C2 . [i9,j9,k9] = the Comp of C2 . (i9,j9,k9) by MULTOP_1:def_1; then A80: the Comp of C2 . (i9,j9,k9) is Function of [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)) by A78, A79, PBOOLE:def_15; A81: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1 .= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def_4 ; A82: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1 .= the Arrows of C2 . (i9,k9) by ALTCAT_1:def_3 ; the Comp of C1 . [i9,j9,k9] = the Comp of C1 . (i9,j9,k9) by MULTOP_1:def_1; then the Comp of C1 . (i9,j9,k9) is Function of [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)) by A62, A65, A71, A81, A82, PBOOLE:def_15; hence the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by A77, A80; ::_thesis: verum end; supposeA83: the Arrows of C1 . (j,k) = {} ; ::_thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) reconsider T = the carrier of C2 as non empty set ; reconsider i9 = i, j9 = j, k9 = k as Element of T by A62, A65, A72, A73, A74; the Arrows of C2 . (j,k) = {} by A62, A65, A68, A83, ALTCAT_1:6; then A84: [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] = {} by ZFMISC_1:90; A85: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1 .= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def_4 ; A86: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1 .= the Arrows of C2 . (i9,k9) by ALTCAT_1:def_3 ; the Comp of C2 . [i9,j9,k9] = the Comp of C2 . (i9,j9,k9) by MULTOP_1:def_1; then A87: the Comp of C2 . (i9,j9,k9) is Function of [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)) by A85, A86, PBOOLE:def_15; A88: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1 .= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def_4 ; A89: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1 .= the Arrows of C2 . (i9,k9) by ALTCAT_1:def_3 ; the Comp of C1 . [i9,j9,k9] = the Comp of C1 . (i9,j9,k9) by MULTOP_1:def_1; then the Comp of C1 . (i9,j9,k9) is Function of [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)) by A62, A65, A71, A88, A89, PBOOLE:def_15; hence the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by A84, A87; ::_thesis: verum end; end; end; end; supposethat A90: the Arrows of C1 . (i,j) <> {} and A91: the Arrows of C1 . (j,k) <> {} ; ::_thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) reconsider T = the carrier of C2 as non empty set ; reconsider i9 = i, j9 = j, k9 = k as Element of T by A62, A65, A72, A73, A74; A92: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1 .= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def_4 ; A93: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1 .= the Arrows of C2 . (i9,k9) by ALTCAT_1:def_3 ; the Comp of C2 . [i9,j9,k9] = the Comp of C2 . (i9,j9,k9) by MULTOP_1:def_1; then reconsider t2 = the Comp of C2 . (i,j,k) as Function of [:( the Arrows of C2 . (j,k)),( the Arrows of C2 . (i,j)):],( the Arrows of C2 . (i,k)) by A92, A93, PBOOLE:def_15; A94: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1 .= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def_4 ; A95: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1 .= the Arrows of C2 . (i9,k9) by ALTCAT_1:def_3 ; the Comp of C1 . [i9,j9,k9] = the Comp of C1 . (i9,j9,k9) by MULTOP_1:def_1; then reconsider t1 = the Comp of C1 . (i,j,k) as Function of [:( the Arrows of C2 . (j,k)),( the Arrows of C2 . (i,j)):],( the Arrows of C2 . (i,k)) by A62, A65, A71, A94, A95, PBOOLE:def_15; A96: the Arrows of C2 . (j,k) <> {} by A62, A65, A68, A91, ALTCAT_1:6; A97: the Arrows of C2 . (i,j) <> {} by A62, A65, A68, A90, ALTCAT_1:6; for a being Element of the Arrows of C2 . (j,k) for b being Element of the Arrows of C2 . (i,j) holds t1 . (a,b) = t2 . (a,b) proof let a be Element of the Arrows of C2 . (j,k); ::_thesis: for b being Element of the Arrows of C2 . (i,j) holds t1 . (a,b) = t2 . (a,b) let b be Element of the Arrows of C2 . (i,j); ::_thesis: t1 . (a,b) = t2 . (a,b) a in the Arrows of C2 . (j,k) by A96; then A98: g is_naturally_transformable_to h by A66; reconsider a = a as natural_transformation of g,h by A66, A96; b in the Arrows of C2 . (i,j) by A97; then A99: f is_naturally_transformable_to g by A66; reconsider b = b as natural_transformation of f,g by A66, A97; ( ex t19 being Function st ( t19 = the Comp of C1 . (f,g,h) & t19 . (a,b) = a `*` b ) & ex t29 being Function st ( t29 = the Comp of C2 . (f,g,h) & t29 . (a,b) = a `*` b ) ) by A64, A67, A98, A99; hence t1 . (a,b) = t2 . (a,b) ; ::_thesis: verum end; hence the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by BINOP_1:2; ::_thesis: verum end; end; end; hence C1 = C2 by A62, A65, A71, ALTCAT_1:8; ::_thesis: verum end; end; :: deftheorem defines Functors FUNCTOR2:def_11_:_ for A, B being category for b3 being non empty transitive strict AltCatStr holds ( b3 = Functors (A,B) iff ( the carrier of b3 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B for x being set holds ( x in the Arrows of b3 . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 being natural_transformation of F,G for t2 being natural_transformation of G,H ex f being Function st ( f = the Comp of b3 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) ) );