functor3.miz

    begin

    registration

      cluster transitive associative with_units strict for non empty AltCatStr;

      existence

      proof

        set A = the transitive associative with_units strict non empty AltCatStr;

        take A;

        thus thesis;

      end;

    end

    registration

      let A be non empty transitive AltCatStr, B be with_units non empty AltCatStr;

      cluster strict comp-preserving comp-reversing Covariant Contravariant feasible for FunctorStr over A, B;

      existence

      proof

        set o = the Object of B;

        take (A --> ( idm o));

        thus thesis;

      end;

    end

    registration

      let A be with_units transitive non empty AltCatStr, B be with_units non empty AltCatStr;

      cluster strict comp-preserving comp-reversing Covariant Contravariant feasible id-preserving for FunctorStr over A, B;

      existence

      proof

        set o = the Object of B;

        take (A --> ( idm o));

        thus thesis;

      end;

    end

    registration

      let A be with_units transitive non empty AltCatStr, B be with_units non empty AltCatStr;

      cluster strict feasible covariant contravariant for Functor of A, B;

      existence

      proof

        set o = the Object of B;

        set I = (A --> ( idm o));

        reconsider I as Functor of A, B by FUNCTOR0:def 25;

        take I;

        thus I is strict feasible;

        thus I is covariant;

        thus thesis;

      end;

    end

    theorem :: FUNCTOR3:1

    for C be category, o1,o2,o3,o4 be Object of C holds for a be Morphism of o1, o2, b be Morphism of o2, o3 holds for c be Morphism of o1, o4, d be Morphism of o4, o3 st (b * a) = (d * c) & (a * (a " )) = ( idm o2) & ((d " ) * d) = ( idm o4) & <^o1, o2^> <> {} & <^o2, o1^> <> {} & <^o2, o3^> <> {} & <^o3, o4^> <> {} & <^o4, o3^> <> {} holds (c * (a " )) = ((d " ) * b)

    proof

      let C be category, o1,o2,o3,o4 be Object of C, a be Morphism of o1, o2, b be Morphism of o2, o3, c be Morphism of o1, o4, d be Morphism of o4, o3 such that

       A1: (b * a) = (d * c) and

       A2: (a * (a " )) = ( idm o2) and

       A3: ((d " ) * d) = ( idm o4) and

       A4: <^o1, o2^> <> {} and

       A5: <^o2, o1^> <> {} and

       A6: <^o2, o3^> <> {} and

       A7: <^o3, o4^> <> {} and

       A8: <^o4, o3^> <> {} ;



       A9: <^o2, o4^> <> {} by A6, A7, ALTCAT_1:def 2;

       <^o1, o3^> <> {} by A4, A6, ALTCAT_1:def 2;

      then

       A10: <^o1, o4^> <> {} by A7, ALTCAT_1:def 2;

      b = (b * ( idm o2)) by A6, ALTCAT_1:def 17

      .= ((b * a) * (a " )) by A2, A4, A5, A6, ALTCAT_1: 21;



      hence ((d " ) * b) = ((d " ) * (d * (c * (a " )))) by A1, A5, A8, A10, ALTCAT_1: 21

      .= (((d " ) * d) * (c * (a " ))) by A7, A8, A9, ALTCAT_1: 21

      .= (c * (a " )) by A3, A9, ALTCAT_1: 20;

    end;

    theorem :: FUNCTOR3:2

    for A be non empty transitive AltCatStr holds for B,C be with_units non empty AltCatStr holds for F be feasible Covariant FunctorStr over A, B holds for G be FunctorStr over B, C, o,o1 be Object of A holds ( Morph-Map ((G * F),o,o1)) = (( Morph-Map (G,(F . o),(F . o1))) * ( Morph-Map (F,o,o1)))

    proof

      let A be non empty transitive AltCatStr, B,C be with_units non empty AltCatStr, F be feasible Covariant FunctorStr over A, B, G be FunctorStr over B, C, o,o1 be Object of A;

      ( dom the MorphMap of G) = [:the carrier of B, the carrier of B:] & ( rng the ObjectMap of F) c= [:the carrier of B, the carrier of B:] by PARTFUN1:def 2;



      then ( dom (the MorphMap of G * the ObjectMap of F)) = ( dom the ObjectMap of F) by RELAT_1: 27

      .= [:the carrier of A, the carrier of A:] by FUNCT_2:def 1;

      then

       A1: [o, o1] in ( dom (the MorphMap of G * the ObjectMap of F)) by ZFMISC_1: 87;



      then

       A2: ((the MorphMap of G * the ObjectMap of F) . [o, o1]) = (the MorphMap of G . (the ObjectMap of F . (o,o1))) by FUNCT_1: 12

      .= ( Morph-Map (G,(F . o),(F . o1))) by FUNCTOR0: 22;

      ( dom the MorphMap of F) = [:the carrier of A, the carrier of A:] by PARTFUN1:def 2;

      then [o, o1] in ( dom the MorphMap of F) by ZFMISC_1: 87;

      then [o, o1] in (( dom (the MorphMap of G * the ObjectMap of F)) /\ ( dom the MorphMap of F)) by A1, XBOOLE_0:def 4;

      then

       A3: [o, o1] in ( dom ((the MorphMap of G * the ObjectMap of F) ** the MorphMap of F)) by PBOOLE:def 19;



      thus ( Morph-Map ((G * F),o,o1)) = (((the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o,o1)) by FUNCTOR0:def 36

      .= (( Morph-Map (G,(F . o),(F . o1))) * ( Morph-Map (F,o,o1))) by A3, A2, PBOOLE:def 19;

    end;

    theorem :: FUNCTOR3:3

    for A be non empty transitive AltCatStr holds for B,C be with_units non empty AltCatStr holds for F be feasible Contravariant FunctorStr over A, B holds for G be FunctorStr over B, C, o,o1 be Object of A holds ( Morph-Map ((G * F),o,o1)) = (( Morph-Map (G,(F . o1),(F . o))) * ( Morph-Map (F,o,o1)))

    proof

      let A be non empty transitive AltCatStr, B,C be with_units non empty AltCatStr, F be feasible Contravariant FunctorStr over A, B, G be FunctorStr over B, C, o,o1 be Object of A;

      ( dom the MorphMap of G) = [:the carrier of B, the carrier of B:] & ( rng the ObjectMap of F) c= [:the carrier of B, the carrier of B:] by PARTFUN1:def 2;



      then ( dom (the MorphMap of G * the ObjectMap of F)) = ( dom the ObjectMap of F) by RELAT_1: 27

      .= [:the carrier of A, the carrier of A:] by FUNCT_2:def 1;

      then

       A1: [o, o1] in ( dom (the MorphMap of G * the ObjectMap of F)) by ZFMISC_1: 87;



      then

       A2: ((the MorphMap of G * the ObjectMap of F) . [o, o1]) = (the MorphMap of G . (the ObjectMap of F . (o,o1))) by FUNCT_1: 12

      .= ( Morph-Map (G,(F . o1),(F . o))) by FUNCTOR0: 23;

      ( dom the MorphMap of F) = [:the carrier of A, the carrier of A:] by PARTFUN1:def 2;

      then [o, o1] in ( dom the MorphMap of F) by ZFMISC_1: 87;

      then [o, o1] in (( dom (the MorphMap of G * the ObjectMap of F)) /\ ( dom the MorphMap of F)) by A1, XBOOLE_0:def 4;

      then

       A3: [o, o1] in ( dom ((the MorphMap of G * the ObjectMap of F) ** the MorphMap of F)) by PBOOLE:def 19;



      thus ( Morph-Map ((G * F),o,o1)) = (((the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o,o1)) by FUNCTOR0:def 36

      .= (( Morph-Map (G,(F . o1),(F . o))) * ( Morph-Map (F,o,o1))) by A3, A2, PBOOLE:def 19;

    end;



     Lm1: for I1 be set, I2 be non empty set, f be Function of I1, I2 holds for A be ManySortedSet of I1, B be ManySortedSet of I2 holds for M be ManySortedFunction of A, (B * f) holds ((( id B) * f) ** M) = M

    proof

      let I1 be set, I2 be non empty set, f be Function of I1, I2;

      let A be ManySortedSet of I1, B be ManySortedSet of I2;

      let M be ManySortedFunction of A, (B * f);

       A1:

      now

        let i be object;

        assume

         A2: i in I1;

        hence

         A3: ((B * f) . i) = (B . (f . i)) by FUNCT_2: 15;

        ((( id B) * f) . i) = (( id B) . (f . i)) & (f . i) in I2 by A2, FUNCT_2: 5, FUNCT_2: 15;

        hence ((( id B) * f) . i) = ( id ((B * f) . i)) by A3, MSUALG_3:def 1;

      end;

      now



         A4: (( id B) * f) is ManySortedFunction of (B * f), (B * f)

        proof

          let i be object;

          assume i in I1;

          then ((( id B) * f) . i) = ( id ((B * f) . i)) by A1;

          hence thesis;

        end;

        let i be object;

        assume

         A5: i in I1;

        then

         A6: (M . i) is Function of (A . i), ((B * f) . i) by PBOOLE:def 15;

        ((( id B) * f) . i) = (( id B) . (f . i)) & (f . i) in I2 by A5, FUNCT_2: 5, FUNCT_2: 15;

        then

         A7: ((( id B) * f) . i) = ( id (B . (f . i))) by MSUALG_3:def 1;

        ((B * f) . i) = (B . (f . i)) by A1, A5;



        hence (((( id B) * f) ** M) . i) = (( id ((B * f) . i)) * (M . i)) by A5, A4, A7, MSUALG_3: 2

        .= (M . i) by A6, FUNCT_2: 17;

      end;

      hence thesis;

    end;

    theorem :: FUNCTOR3:4

    for A be non empty transitive AltCatStr holds for B be with_units non empty AltCatStr holds for F be feasible FunctorStr over A, B holds (( id B) * F) = the FunctorStr of F

    proof

      let A be non empty transitive AltCatStr, B be with_units non empty AltCatStr, F be feasible FunctorStr over A, B;



       A1: the ObjectMap of (( id B) * F) = (the ObjectMap of ( id B) * the ObjectMap of F) by FUNCTOR0:def 36

      .= (( id [:the carrier of B, the carrier of B:]) * the ObjectMap of F) by FUNCTOR0:def 29

      .= the ObjectMap of F by FUNCT_2: 17;



       A2: the MorphMap of F is ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) by FUNCTOR0:def 4;

      the MorphMap of (( id B) * F) = ((the MorphMap of ( id B) * the ObjectMap of F) ** the MorphMap of F) by FUNCTOR0:def 36

      .= ((( id the Arrows of B) * the ObjectMap of F) ** the MorphMap of F) by FUNCTOR0:def 29

      .= the MorphMap of F by A2, Lm1;

      hence thesis by A1;

    end;

    theorem :: FUNCTOR3:5

    for A be with_units transitive non empty AltCatStr holds for B be with_units non empty AltCatStr holds for F be feasible FunctorStr over A, B holds (F * ( id A)) = the FunctorStr of F

    proof

      let A be with_units transitive non empty AltCatStr, B be with_units non empty AltCatStr, F be feasible FunctorStr over A, B;



       A1: the ObjectMap of (F * ( id A)) = (the ObjectMap of F * the ObjectMap of ( id A)) by FUNCTOR0:def 36

      .= (the ObjectMap of F * ( id [:the carrier of A, the carrier of A:])) by FUNCTOR0:def 29

      .= the ObjectMap of F by FUNCT_2: 17;



       A2: the MorphMap of F is ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) by FUNCTOR0:def 4;

      the MorphMap of (F * ( id A)) = ((the MorphMap of F * the ObjectMap of ( id A)) ** the MorphMap of ( id A)) by FUNCTOR0:def 36

      .= ((the MorphMap of F * ( id [:the carrier of A, the carrier of A:])) ** the MorphMap of ( id A)) by FUNCTOR0:def 29

      .= (the MorphMap of F ** the MorphMap of ( id A)) by FUNCTOR0: 2

      .= (the MorphMap of F ** ( id the Arrows of A)) by FUNCTOR0:def 29

      .= the MorphMap of F by A2, MSUALG_3: 3;

      hence thesis by A1;

    end;

    reserve A for non empty AltCatStr,

B,C for non empty reflexive AltCatStr,

F for feasible Covariant FunctorStr over A, B,

G for feasible Covariant FunctorStr over B, C,

M for feasible Contravariant FunctorStr over A, B,

N for feasible Contravariant FunctorStr over B, C,

o1,o2 for Object of A,

m for Morphism of o1, o2;

    theorem :: FUNCTOR3:6



     Th6: <^o1, o2^> <> {} implies ((G * F) . m) = (G . (F . m))

    proof

      set I = the carrier of A;

      reconsider s = (the MorphMap of F . (o1,o2)) as Function;

      reconsider r = (((the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o1,o2)) as Function;

      reconsider t = ((the MorphMap of G * the ObjectMap of F) . (o1,o2)) as Function;



       A1: ( dom ((the MorphMap of G * the ObjectMap of F) ** the MorphMap of F)) = (( dom (the MorphMap of G * the ObjectMap of F)) /\ ( dom the MorphMap of F)) by PBOOLE:def 19

      .= ( [:I, I:] /\ ( dom the MorphMap of F)) by PARTFUN1:def 2

      .= ( [:I, I:] /\ [:I, I:]) by PARTFUN1:def 2

      .= [:I, I:];



       A2: ( dom the ObjectMap of F) = [:I, I:] by FUNCT_2:def 1;



       A3: [o1, o2] in [:I, I:] by ZFMISC_1:def 2;

      assume

       A4: <^o1, o2^> <> {} ;

      then

       A5: <^(F . o1), (F . o2)^> <> {} by FUNCTOR0:def 18;

      then

       A6: ( dom ( Morph-Map (F,o1,o2))) = <^o1, o2^> by FUNCT_2:def 1;



       A7: <^(G . (F . o1)), (G . (F . o2))^> <> {} by A5, FUNCTOR0:def 18;

      ((G * F) . o1) = (G . (F . o1)) & ((G * F) . o2) = (G . (F . o2)) by FUNCTOR0: 33;



      hence ((G * F) . m) = (( Morph-Map ((G * F),o1,o2)) . m) by A4, A7, FUNCTOR0:def 15

      .= (r . m) by FUNCTOR0:def 36

      .= ((t * s) . m) by A1, A3, PBOOLE:def 19

      .= (t . (( Morph-Map (F,o1,o2)) . m)) by A4, A6, FUNCT_1: 13

      .= (t . (F . m)) by A4, A5, FUNCTOR0:def 15

      .= ((the MorphMap of G . (the ObjectMap of F . (o1,o2))) . (F . m)) by A2, A3, FUNCT_1: 13

      .= (( Morph-Map (G,(F . o1),(F . o2))) . (F . m)) by FUNCTOR0: 22

      .= (G . (F . m)) by A5, A7, FUNCTOR0:def 15;

    end;

    theorem :: FUNCTOR3:7



     Th7: <^o1, o2^> <> {} implies ((N * M) . m) = (N . (M . m))

    proof

      set I = the carrier of A;

      reconsider s = (the MorphMap of M . (o1,o2)) as Function;

      reconsider r = (((the MorphMap of N * the ObjectMap of M) ** the MorphMap of M) . (o1,o2)) as Function;

      reconsider t = ((the MorphMap of N * the ObjectMap of M) . (o1,o2)) as Function;



       A1: ( dom ((the MorphMap of N * the ObjectMap of M) ** the MorphMap of M)) = (( dom (the MorphMap of N * the ObjectMap of M)) /\ ( dom the MorphMap of M)) by PBOOLE:def 19

      .= ( [:I, I:] /\ ( dom the MorphMap of M)) by PARTFUN1:def 2

      .= ( [:I, I:] /\ [:I, I:]) by PARTFUN1:def 2

      .= [:I, I:];



       A2: ( dom the ObjectMap of M) = [:I, I:] by FUNCT_2:def 1;



       A3: [o1, o2] in [:I, I:] by ZFMISC_1:def 2;

      assume

       A4: <^o1, o2^> <> {} ;

      then

       A5: <^(M . o2), (M . o1)^> <> {} by FUNCTOR0:def 19;

      then

       A6: ( dom ( Morph-Map (M,o1,o2))) = <^o1, o2^> by FUNCT_2:def 1;



       A7: <^(N . (M . o1)), (N . (M . o2))^> <> {} by A5, FUNCTOR0:def 19;

      ((N * M) . o1) = (N . (M . o1)) & ((N * M) . o2) = (N . (M . o2)) by FUNCTOR0: 33;



      hence ((N * M) . m) = (( Morph-Map ((N * M),o1,o2)) . m) by A4, A7, FUNCTOR0:def 15

      .= (r . m) by FUNCTOR0:def 36

      .= ((t * s) . m) by A1, A3, PBOOLE:def 19

      .= (t . (( Morph-Map (M,o1,o2)) . m)) by A4, A6, FUNCT_1: 13

      .= (t . (M . m)) by A4, A5, FUNCTOR0:def 16

      .= ((the MorphMap of N . (the ObjectMap of M . (o1,o2))) . (M . m)) by A2, A3, FUNCT_1: 13

      .= (( Morph-Map (N,(M . o2),(M . o1))) . (M . m)) by FUNCTOR0: 23

      .= (N . (M . m)) by A5, A7, FUNCTOR0:def 16;

    end;

    theorem :: FUNCTOR3:8



     Th8: <^o1, o2^> <> {} implies ((N * F) . m) = (N . (F . m))

    proof

      set I = the carrier of A;

      reconsider s = (the MorphMap of F . (o1,o2)) as Function;

      reconsider r = (((the MorphMap of N * the ObjectMap of F) ** the MorphMap of F) . (o1,o2)) as Function;

      reconsider t = ((the MorphMap of N * the ObjectMap of F) . (o1,o2)) as Function;



       A1: ( dom ((the MorphMap of N * the ObjectMap of F) ** the MorphMap of F)) = (( dom (the MorphMap of N * the ObjectMap of F)) /\ ( dom the MorphMap of F)) by PBOOLE:def 19

      .= ( [:I, I:] /\ ( dom the MorphMap of F)) by PARTFUN1:def 2

      .= ( [:I, I:] /\ [:I, I:]) by PARTFUN1:def 2

      .= [:I, I:];



       A2: ( dom the ObjectMap of F) = [:I, I:] by FUNCT_2:def 1;



       A3: [o1, o2] in [:I, I:] by ZFMISC_1:def 2;

      assume

       A4: <^o1, o2^> <> {} ;

      then

       A5: <^(F . o1), (F . o2)^> <> {} by FUNCTOR0:def 18;

      then

       A6: ( dom ( Morph-Map (F,o1,o2))) = <^o1, o2^> by FUNCT_2:def 1;



       A7: <^(N . (F . o2)), (N . (F . o1))^> <> {} by A5, FUNCTOR0:def 19;

      ((N * F) . o1) = (N . (F . o1)) & ((N * F) . o2) = (N . (F . o2)) by FUNCTOR0: 33;



      hence ((N * F) . m) = (( Morph-Map ((N * F),o1,o2)) . m) by A4, A7, FUNCTOR0:def 16

      .= (r . m) by FUNCTOR0:def 36

      .= ((t * s) . m) by A1, A3, PBOOLE:def 19

      .= (t . (( Morph-Map (F,o1,o2)) . m)) by A4, A6, FUNCT_1: 13

      .= (t . (F . m)) by A4, A5, FUNCTOR0:def 15

      .= ((the MorphMap of N . (the ObjectMap of F . (o1,o2))) . (F . m)) by A2, A3, FUNCT_1: 13

      .= (( Morph-Map (N,(F . o1),(F . o2))) . (F . m)) by FUNCTOR0: 22

      .= (N . (F . m)) by A5, A7, FUNCTOR0:def 16;

    end;

    theorem :: FUNCTOR3:9



     Th9: <^o1, o2^> <> {} implies ((G * M) . m) = (G . (M . m))

    proof

      set I = the carrier of A;

      reconsider s = (the MorphMap of M . (o1,o2)) as Function;

      reconsider r = (((the MorphMap of G * the ObjectMap of M) ** the MorphMap of M) . (o1,o2)) as Function;

      reconsider t = ((the MorphMap of G * the ObjectMap of M) . (o1,o2)) as Function;



       A1: ( dom ((the MorphMap of G * the ObjectMap of M) ** the MorphMap of M)) = (( dom (the MorphMap of G * the ObjectMap of M)) /\ ( dom the MorphMap of M)) by PBOOLE:def 19

      .= ( [:I, I:] /\ ( dom the MorphMap of M)) by PARTFUN1:def 2

      .= ( [:I, I:] /\ [:I, I:]) by PARTFUN1:def 2

      .= [:I, I:];



       A2: ( dom the ObjectMap of M) = [:I, I:] by FUNCT_2:def 1;



       A3: [o1, o2] in [:I, I:] by ZFMISC_1:def 2;

      assume

       A4: <^o1, o2^> <> {} ;

      then

       A5: <^(M . o2), (M . o1)^> <> {} by FUNCTOR0:def 19;

      then

       A6: ( dom ( Morph-Map (M,o1,o2))) = <^o1, o2^> by FUNCT_2:def 1;



       A7: <^(G . (M . o2)), (G . (M . o1))^> <> {} by A5, FUNCTOR0:def 18;

      ((G * M) . o1) = (G . (M . o1)) & ((G * M) . o2) = (G . (M . o2)) by FUNCTOR0: 33;



      hence ((G * M) . m) = (( Morph-Map ((G * M),o1,o2)) . m) by A4, A7, FUNCTOR0:def 16

      .= (r . m) by FUNCTOR0:def 36

      .= ((t * s) . m) by A1, A3, PBOOLE:def 19

      .= (t . (( Morph-Map (M,o1,o2)) . m)) by A4, A6, FUNCT_1: 13

      .= (t . (M . m)) by A4, A5, FUNCTOR0:def 16

      .= ((the MorphMap of G . (the ObjectMap of M . (o1,o2))) . (M . m)) by A2, A3, FUNCT_1: 13

      .= (( Morph-Map (G,(M . o2),(M . o1))) . (M . m)) by FUNCTOR0: 23

      .= (G . (M . m)) by A5, A7, FUNCTOR0:def 15;

    end;

    registration

      let A be non empty transitive AltCatStr, B be transitive with_units non empty AltCatStr, C be with_units non empty AltCatStr, F be feasible Covariant comp-preserving FunctorStr over A, B, G be feasible Covariant comp-preserving FunctorStr over B, C;

      cluster (G * F) -> comp-preserving;

      coherence

      proof

        let o1,o2,o3 be Object of A such that

         A1: <^o1, o2^> <> {} and

         A2: <^o2, o3^> <> {} ;



         A3: <^(F . o1), (F . o2)^> <> {} & <^(F . o2), (F . o3)^> <> {} by A1, A2, FUNCTOR0:def 18;

        let f be Morphism of o1, o2, g be Morphism of o2, o3;



         A4: ((G * F) . o1) = (G . (F . o1)) & ((G * F) . o3) = (G . (F . o3)) by FUNCTOR0: 33;



         A5: ((G * F) . o2) = (G . (F . o2)) by FUNCTOR0: 33;

        then

        reconsider GFg = ((G * F) . g) as Morphism of (G . (F . o2)), (G . (F . o3)) by FUNCTOR0: 33;

         <^o1, o3^> <> {} by A1, A2, ALTCAT_1:def 2;



        hence ((G * F) . (g * f)) = (G . (F . (g * f))) by Th6

        .= (G . ((F . g) * (F . f))) by A1, A2, FUNCTOR0:def 23

        .= ((G . (F . g)) * (G . (F . f))) by A3, FUNCTOR0:def 23

        .= (GFg * (G . (F . f))) by A2, Th6

        .= (((G * F) . g) * ((G * F) . f)) by A1, A5, A4, Th6;

      end;

    end

    registration

      let A be non empty transitive AltCatStr, B be transitive with_units non empty AltCatStr, C be with_units non empty AltCatStr, F be feasible Contravariant comp-reversing FunctorStr over A, B, G be feasible Contravariant comp-reversing FunctorStr over B, C;

      cluster (G * F) -> comp-preserving;

      coherence

      proof

        let o1,o2,o3 be Object of A such that

         A1: <^o1, o2^> <> {} and

         A2: <^o2, o3^> <> {} ;



         A3: <^(F . o2), (F . o1)^> <> {} & <^(F . o3), (F . o2)^> <> {} by A1, A2, FUNCTOR0:def 19;

        let f be Morphism of o1, o2, g be Morphism of o2, o3;



         A4: ((G * F) . o1) = (G . (F . o1)) & ((G * F) . o3) = (G . (F . o3)) by FUNCTOR0: 33;



         A5: ((G * F) . o2) = (G . (F . o2)) by FUNCTOR0: 33;

        then

        reconsider GFg = ((G * F) . g) as Morphism of (G . (F . o2)), (G . (F . o3)) by FUNCTOR0: 33;

         <^o1, o3^> <> {} by A1, A2, ALTCAT_1:def 2;



        hence ((G * F) . (g * f)) = (G . (F . (g * f))) by Th7

        .= (G . ((F . f) * (F . g))) by A1, A2, FUNCTOR0:def 24

        .= ((G . (F . g)) * (G . (F . f))) by A3, FUNCTOR0:def 24

        .= (GFg * (G . (F . f))) by A2, Th7

        .= (((G * F) . g) * ((G * F) . f)) by A1, A5, A4, Th7;

      end;

    end

    registration

      let A be non empty transitive AltCatStr, B be transitive with_units non empty AltCatStr, C be with_units non empty AltCatStr, F be feasible Covariant comp-preserving FunctorStr over A, B, G be feasible Contravariant comp-reversing FunctorStr over B, C;

      cluster (G * F) -> comp-reversing;

      coherence

      proof

        let o1,o2,o3 be Object of A such that

         A1: <^o1, o2^> <> {} and

         A2: <^o2, o3^> <> {} ;



         A3: <^(F . o1), (F . o2)^> <> {} & <^(F . o2), (F . o3)^> <> {} by A1, A2, FUNCTOR0:def 18;

        let f be Morphism of o1, o2, g be Morphism of o2, o3;



         A4: ((G * F) . o2) = (G . (F . o2)) & ((G * F) . o3) = (G . (F . o3)) by FUNCTOR0: 33;



         A5: ((G * F) . o1) = (G . (F . o1)) by FUNCTOR0: 33;

        then

        reconsider GFf = ((G * F) . f) as Morphism of (G . (F . o2)), (G . (F . o1)) by FUNCTOR0: 33;

         <^o1, o3^> <> {} by A1, A2, ALTCAT_1:def 2;



        hence ((G * F) . (g * f)) = (G . (F . (g * f))) by Th8

        .= (G . ((F . g) * (F . f))) by A1, A2, FUNCTOR0:def 23

        .= ((G . (F . f)) * (G . (F . g))) by A3, FUNCTOR0:def 24

        .= (GFf * (G . (F . g))) by A1, Th8

        .= (((G * F) . f) * ((G * F) . g)) by A2, A5, A4, Th8;

      end;

    end

    registration

      let A be non empty transitive AltCatStr, B be transitive with_units non empty AltCatStr, C be with_units non empty AltCatStr, F be feasible Contravariant comp-reversing FunctorStr over A, B, G be feasible Covariant comp-preserving FunctorStr over B, C;

      cluster (G * F) -> comp-reversing;

      coherence

      proof

        let o1,o2,o3 be Object of A such that

         A1: <^o1, o2^> <> {} and

         A2: <^o2, o3^> <> {} ;



         A3: <^(F . o2), (F . o1)^> <> {} & <^(F . o3), (F . o2)^> <> {} by A1, A2, FUNCTOR0:def 19;

        let f be Morphism of o1, o2, g be Morphism of o2, o3;



         A4: ((G * F) . o2) = (G . (F . o2)) & ((G * F) . o3) = (G . (F . o3)) by FUNCTOR0: 33;



         A5: ((G * F) . o1) = (G . (F . o1)) by FUNCTOR0: 33;

        then

        reconsider GFf = ((G * F) . f) as Morphism of (G . (F . o2)), (G . (F . o1)) by FUNCTOR0: 33;

         <^o1, o3^> <> {} by A1, A2, ALTCAT_1:def 2;



        hence ((G * F) . (g * f)) = (G . (F . (g * f))) by Th9

        .= (G . ((F . f) * (F . g))) by A1, A2, FUNCTOR0:def 24

        .= ((G . (F . f)) * (G . (F . g))) by A3, FUNCTOR0:def 23

        .= (GFf * (G . (F . g))) by A1, Th9

        .= (((G * F) . f) * ((G * F) . g)) by A2, A5, A4, Th9;

      end;

    end

    definition

      let A,B be transitive with_units non empty AltCatStr, C be with_units non empty AltCatStr, F be covariant Functor of A, B, G be covariant Functor of B, C;

      :: original: *

      redefine

      func G * F -> strict covariant Functor of A, C ;

      coherence by FUNCTOR0:def 25;

    end

    definition

      let A,B be transitive with_units non empty AltCatStr, C be with_units non empty AltCatStr, F be contravariant Functor of A, B, G be contravariant Functor of B, C;

      :: original: *

      redefine

      func G * F -> strict covariant Functor of A, C ;

      coherence by FUNCTOR0:def 25;

    end

    definition

      let A,B be transitive with_units non empty AltCatStr, C be with_units non empty AltCatStr, F be covariant Functor of A, B, G be contravariant Functor of B, C;

      :: original: *

      redefine

      func G * F -> strict contravariant Functor of A, C ;

      coherence by FUNCTOR0:def 25;

    end

    definition

      let A,B be transitive with_units non empty AltCatStr, C be with_units non empty AltCatStr, F be contravariant Functor of A, B, G be covariant Functor of B, C;

      :: original: *

      redefine

      func G * F -> strict contravariant Functor of A, C ;

      coherence by FUNCTOR0:def 25;

    end

    reserve A,B,C,D for transitive with_units non empty AltCatStr,

F1,F2,F3 for covariant Functor of A, B,

G1,G2,G3 for covariant Functor of B, C,

H1,H2 for covariant Functor of C, D,

p for transformation of F1, F2,

p1 for transformation of F2, F3,

q for transformation of G1, G2,

q1 for transformation of G2, G3,

r for transformation of H1, H2;

    theorem :: FUNCTOR3:10



     Th10: F1 is_transformable_to F2 & G1 is_transformable_to G2 implies (G1 * F1) is_transformable_to (G2 * F2)

    proof

      assume

       A1: for a be Object of A holds <^(F1 . a), (F2 . a)^> <> {} ;

      assume

       A2: for a be Object of B holds <^(G1 . a), (G2 . a)^> <> {} ;

      let a be Object of A;

       <^(F1 . a), (F2 . a)^> <> {} by A1;

      then

       A3: <^(G1 . (F1 . a)), (G1 . (F2 . a))^> <> {} by FUNCTOR0:def 18;



       A4: ((G1 * F1) . a) = (G1 . (F1 . a)) & ((G2 * F2) . a) = (G2 . (F2 . a)) by FUNCTOR0: 33;

       <^(G1 . (F2 . a)), (G2 . (F2 . a))^> <> {} by A2;

      hence thesis by A4, A3, ALTCAT_1:def 2;

    end;

    begin

    definition

      let A,B,C be transitive with_units non empty AltCatStr, F1,F2 be covariant Functor of A, B, t be transformation of F1, F2, G be covariant Functor of B, C;

      :: FUNCTOR3:def1

      func G * t -> transformation of (G * F1), (G * F2) means

      : Def1: for o be Object of A holds (it . o) = (G . (t ! o));

      existence

      proof

        defpred P[ object, object] means ex o be Object of A st $1 = o & $2 = (G . (t ! o));

        set I = the carrier of A;



         A2: for i be object st i in I holds ex j be object st P[i, j]

        proof

          let i be object;

          assume i in I;

          then

          reconsider o = i as Object of A;

          take (G . (t ! o));

          thus thesis;

        end;

        consider IT be ManySortedSet of I such that

         A3: for o be object st o in I holds P[o, (IT . o)] from PBOOLE:sch 3( A2);

        IT is transformation of (G * F1), (G * F2)

        proof

          thus (G * F1) is_transformable_to (G * F2) by A1, Th10;

          let o be Object of A;

           P[o, (IT . o)] & (G . (F1 . o)) = ((G * F1) . o) by A3, FUNCTOR0: 33;

          hence thesis by FUNCTOR0: 33;

        end;

        then

        reconsider IT as transformation of (G * F1), (G * F2);

        take IT;

        let o be Object of A;

         P[o, (IT . o)] by A3;

        hence thesis;

      end;

      uniqueness

      proof

        let X,Y be transformation of (G * F1), (G * F2) such that

         A4: for o be Object of A holds (X . o) = (G . (t ! o)) and

         A5: for o be Object of A holds (Y . o) = (G . (t ! o));



         A6: (G * F1) is_transformable_to (G * F2) by A1, Th10;

        now

          let o be Object of A;



          thus (X ! o) = (X . o) by A6, FUNCTOR2:def 4

          .= (G . (t ! o)) by A4

          .= (Y . o) by A5

          .= (Y ! o) by A6, FUNCTOR2:def 4;

        end;

        hence thesis by A1, Th10, FUNCTOR2: 3;

      end;

    end

    theorem :: FUNCTOR3:11



     Th11: for o be Object of A st F1 is_transformable_to F2 holds ((G1 * p) ! o) = (G1 . (p ! o))

    proof

      let o be Object of A;

      assume

       A1: F1 is_transformable_to F2;

      then (G1 * F1) is_transformable_to (G1 * F2) by Th10;



      hence ((G1 * p) ! o) = ((G1 * p) . o) by FUNCTOR2:def 4

      .= (G1 . (p ! o)) by A1, Def1;

    end;

    definition

      let A,B,C be transitive with_units non empty AltCatStr, G1,G2 be covariant Functor of B, C, F be covariant Functor of A, B, s be transformation of G1, G2;

      :: FUNCTOR3:def2

      func s * F -> transformation of (G1 * F), (G2 * F) means

      : Def2: for o be Object of A holds (it . o) = (s ! (F . o));

      existence

      proof

        defpred P[ object, object] means ex o be Object of A st $1 = o & $2 = (s ! (F . o));

        set I = the carrier of A;



         A2: for i be object st i in I holds ex j be object st P[i, j]

        proof

          let i be object;

          assume i in I;

          then

          reconsider o = i as Object of A;

          take (s ! (F . o));

          thus thesis;

        end;

        consider IT be ManySortedSet of I such that

         A3: for o be object st o in I holds P[o, (IT . o)] from PBOOLE:sch 3( A2);

        IT is transformation of (G1 * F), (G2 * F)

        proof

          thus (G1 * F) is_transformable_to (G2 * F) by A1, Th10;

          let o be Object of A;

           P[o, (IT . o)] & (G1 . (F . o)) = ((G1 * F) . o) by A3, FUNCTOR0: 33;

          hence thesis by FUNCTOR0: 33;

        end;

        then

        reconsider IT as transformation of (G1 * F), (G2 * F);

        take IT;

        let o be Object of A;

         P[o, (IT . o)] by A3;

        hence thesis;

      end;

      uniqueness

      proof

        let X,Y be transformation of (G1 * F), (G2 * F) such that

         A4: for o be Object of A holds (X . o) = (s ! (F . o)) and

         A5: for o be Object of A holds (Y . o) = (s ! (F . o));



         A6: (G1 * F) is_transformable_to (G2 * F) by A1, Th10;

        now

          let o be Object of A;



          thus (X ! o) = (X . o) by A6, FUNCTOR2:def 4

          .= (s ! (F . o)) by A4

          .= (Y . o) by A5

          .= (Y ! o) by A6, FUNCTOR2:def 4;

        end;

        hence thesis by A1, Th10, FUNCTOR2: 3;

      end;

    end

    theorem :: FUNCTOR3:12



     Th12: for o be Object of A st G1 is_transformable_to G2 holds ((q * F1) ! o) = (q ! (F1 . o))

    proof

      let o be Object of A;

      assume

       A1: G1 is_transformable_to G2;

      then (G1 * F1) is_transformable_to (G2 * F1) by Th10;



      hence ((q * F1) ! o) = ((q * F1) . o) by FUNCTOR2:def 4

      .= (q ! (F1 . o)) by A1, Def2;

    end;

    theorem :: FUNCTOR3:13



     Th13: F1 is_transformable_to F2 & F2 is_transformable_to F3 implies (G1 * (p1 `*` p)) = ((G1 * p1) `*` (G1 * p))

    proof

      assume that

       A1: F1 is_transformable_to F2 and

       A2: F2 is_transformable_to F3;



       A3: (G1 * F1) is_transformable_to (G1 * F2) & (G1 * F2) is_transformable_to (G1 * F3) by A1, A2, Th10;

       A4:

      now

        let a be Object of A;



         A5: (G1 . (F2 . a)) = ((G1 * F2) . a) & (G1 . (F3 . a)) = ((G1 * F3) . a) by FUNCTOR0: 33;



         A6: (G1 . (F1 . a)) = ((G1 * F1) . a) by FUNCTOR0: 33;

        then

        reconsider G1ta = ((G1 * p) ! a) as Morphism of (G1 . (F1 . a)), (G1 . (F2 . a)) by FUNCTOR0: 33;



         A7: <^(F1 . a), (F2 . a)^> <> {} & <^(F2 . a), (F3 . a)^> <> {} by A1, A2;



        thus ((G1 * (p1 `*` p)) ! a) = (G1 . ((p1 `*` p) ! a)) by A1, A2, Th11, FUNCTOR2: 2

        .= (G1 . ((p1 ! a) * (p ! a))) by A1, A2, FUNCTOR2:def 5

        .= ((G1 . (p1 ! a)) * (G1 . (p ! a))) by A7, FUNCTOR0:def 23

        .= ((G1 . (p1 ! a)) * G1ta) by A1, Th11

        .= (((G1 * p1) ! a) * ((G1 * p) ! a)) by A2, A6, A5, Th11

        .= (((G1 * p1) `*` (G1 * p)) ! a) by A3, FUNCTOR2:def 5;

      end;

      F1 is_transformable_to F3 by A1, A2, FUNCTOR2: 2;

      hence thesis by A4, Th10, FUNCTOR2: 3;

    end;

    theorem :: FUNCTOR3:14



     Th14: G1 is_transformable_to G2 & G2 is_transformable_to G3 implies ((q1 `*` q) * F1) = ((q1 * F1) `*` (q * F1))

    proof

      assume that

       A1: G1 is_transformable_to G2 and

       A2: G2 is_transformable_to G3;



       A3: (G1 * F1) is_transformable_to (G2 * F1) & (G2 * F1) is_transformable_to (G3 * F1) by A1, A2, Th10;

       A4:

      now

        let a be Object of A;



         A5: (G1 . (F1 . a)) = ((G1 * F1) . a) & (G3 . (F1 . a)) = ((G3 * F1) . a) by FUNCTOR0: 33;



         A6: (G2 . (F1 . a)) = ((G2 * F1) . a) by FUNCTOR0: 33;

        then

        reconsider s1F1a = ((q1 * F1) ! a) as Morphism of (G2 . (F1 . a)), (G3 . (F1 . a)) by FUNCTOR0: 33;



        thus (((q1 `*` q) * F1) ! a) = ((q1 `*` q) ! (F1 . a)) by A1, A2, Th12, FUNCTOR2: 2

        .= ((q1 ! (F1 . a)) * (q ! (F1 . a))) by A1, A2, FUNCTOR2:def 5

        .= (s1F1a * (q ! (F1 . a))) by A2, Th12

        .= (((q1 * F1) ! a) * ((q * F1) ! a)) by A1, A6, A5, Th12

        .= (((q1 * F1) `*` (q * F1)) ! a) by A3, FUNCTOR2:def 5;

      end;

      G1 is_transformable_to G3 by A1, A2, FUNCTOR2: 2;

      hence thesis by A4, Th10, FUNCTOR2: 3;

    end;

    theorem :: FUNCTOR3:15



     Th15: H1 is_transformable_to H2 implies ((r * G1) * F1) = (r * (G1 * F1))

    proof



       A1: ((H2 * G1) * F1) = (H2 * (G1 * F1)) by FUNCTOR0: 32;

      then

      reconsider m = (r * (G1 * F1)) as transformation of ((H1 * G1) * F1), ((H2 * G1) * F1) by FUNCTOR0: 32;

      assume

       A2: H1 is_transformable_to H2;

       A3:

      now

        let a be Object of A;



        thus (((r * G1) * F1) ! a) = ((r * G1) ! (F1 . a)) by A2, Th10, Th12

        .= (r ! (G1 . (F1 . a))) by A2, Th12

        .= (r ! ((G1 * F1) . a)) by FUNCTOR0: 33

        .= ((r * (G1 * F1)) ! a) by A2, Th12

        .= (m ! a) by A1, FUNCTOR0: 32;

      end;

      (H1 * G1) is_transformable_to (H2 * G1) by A2, Th10;

      hence thesis by A3, Th10, FUNCTOR2: 3;

    end;

    theorem :: FUNCTOR3:16



     Th16: G1 is_transformable_to G2 implies ((H1 * q) * F1) = (H1 * (q * F1))

    proof



       A1: ((H1 * G2) * F1) = (H1 * (G2 * F1)) by FUNCTOR0: 32;

      then

      reconsider m = (H1 * (q * F1)) as transformation of ((H1 * G1) * F1), ((H1 * G2) * F1) by FUNCTOR0: 32;

      assume

       A2: G1 is_transformable_to G2;

       A3:

      now

        let a be Object of A;



         A4: ((G1 * F1) . a) = (G1 . (F1 . a)) & ((G2 * F1) . a) = (G2 . (F1 . a)) by FUNCTOR0: 33;



        thus (((H1 * q) * F1) ! a) = ((H1 * q) ! (F1 . a)) by A2, Th10, Th12

        .= (H1 . (q ! (F1 . a))) by A2, Th11

        .= (H1 . ((q * F1) ! a)) by A2, A4, Th12

        .= ((H1 * (q * F1)) ! a) by A2, Th10, Th11

        .= (m ! a) by A1, FUNCTOR0: 32;

      end;

      (H1 * G1) is_transformable_to (H1 * G2) by A2, Th10;

      hence thesis by A3, Th10, FUNCTOR2: 3;

    end;

    theorem :: FUNCTOR3:17



     Th17: F1 is_transformable_to F2 implies ((H1 * G1) * p) = (H1 * (G1 * p))

    proof



       A1: ((H1 * G1) * F2) = (H1 * (G1 * F2)) by FUNCTOR0: 32;

      then

      reconsider m = (H1 * (G1 * p)) as transformation of ((H1 * G1) * F1), ((H1 * G1) * F2) by FUNCTOR0: 32;

      assume

       A2: F1 is_transformable_to F2;

      now

        let a be Object of A;



         A3: ((G1 * F1) . a) = (G1 . (F1 . a)) & ((G1 * F2) . a) = (G1 . (F2 . a)) by FUNCTOR0: 33;



         A4: <^(F1 . a), (F2 . a)^> <> {} by A2;



        thus (((H1 * G1) * p) ! a) = ((H1 * G1) . (p ! a)) by A2, Th11

        .= (H1 . (G1 . (p ! a))) by A4, Th6

        .= (H1 . ((G1 * p) ! a)) by A2, A3, Th11

        .= ((H1 * (G1 * p)) ! a) by A2, Th10, Th11

        .= (m ! a) by A1, FUNCTOR0: 32;

      end;

      hence thesis by A2, Th10, FUNCTOR2: 3;

    end;

    theorem :: FUNCTOR3:18



     Th18: (( idt G1) * F1) = ( idt (G1 * F1))

    proof

      now

        let a be Object of A;



        thus ((( idt G1) * F1) ! a) = (( idt G1) ! (F1 . a)) by Th12

        .= ( idm (G1 . (F1 . a))) by FUNCTOR2: 4

        .= ( idm ((G1 * F1) . a)) by FUNCTOR0: 33

        .= (( idt (G1 * F1)) ! a) by FUNCTOR2: 4;

      end;

      hence thesis by FUNCTOR2: 3;

    end;

    theorem :: FUNCTOR3:19



     Th19: (G1 * ( idt F1)) = ( idt (G1 * F1))

    proof

      now

        let a be Object of A;



        thus ((G1 * ( idt F1)) ! a) = (G1 . (( idt F1) ! a)) by Th11

        .= (G1 . ( idm (F1 . a))) by FUNCTOR2: 4

        .= ( idm (G1 . (F1 . a))) by FUNCTOR2: 1

        .= ( idm ((G1 * F1) . a)) by FUNCTOR0: 33

        .= (( idt (G1 * F1)) ! a) by FUNCTOR2: 4;

      end;

      hence thesis by FUNCTOR2: 3;

    end;

    theorem :: FUNCTOR3:20



     Th20: F1 is_transformable_to F2 implies (( id B) * p) = p

    proof

      assume

       A1: F1 is_transformable_to F2;

      now

        let i be object;

        assume i in the carrier of A;

        then

        reconsider a = i as Object of A;



         A2: <^(F1 . a), (F2 . a)^> <> {} by A1;



        thus ((( id B) * p) . i) = (( id B) . (p ! a)) by A1, Def1

        .= (p ! a) by A2, FUNCTOR0: 31

        .= (p . i) by A1, FUNCTOR2:def 4;

      end;

      hence thesis;

    end;

    theorem :: FUNCTOR3:21



     Th21: G1 is_transformable_to G2 implies (q * ( id B)) = q

    proof

      assume

       A1: G1 is_transformable_to G2;

      now

        let i be object;

        assume i in the carrier of B;

        then

        reconsider a = i as Object of B;



        thus ((q * ( id B)) . i) = (q ! (( id B) . a)) by A1, Def2

        .= (q ! a) by FUNCTOR0: 29

        .= (q . i) by A1, FUNCTOR2:def 4;

      end;

      hence thesis;

    end;

    begin

    definition

      let A,B,C be transitive with_units non empty AltCatStr, F1,F2 be covariant Functor of A, B, G1,G2 be covariant Functor of B, C, t be transformation of F1, F2, s be transformation of G1, G2;

      :: FUNCTOR3:def3

      func s (#) t -> transformation of (G1 * F1), (G2 * F2) equals ((s * F2) `*` (G1 * t));

      coherence ;

    end

    theorem :: FUNCTOR3:22



     Th22: for q be natural_transformation of G1, G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds (q (#) p) = ((G2 * p) `*` (q * F1))

    proof

      let q be natural_transformation of G1, G2;

      assume that

       A1: F1 is_transformable_to F2 and

       A2: G1 is_naturally_transformable_to G2;



       A3: (G1 * F1) is_transformable_to (G1 * F2) by A1, Th10;



       A4: (G2 * F1) is_transformable_to (G2 * F2) by A1, Th10;



       A5: G1 is_transformable_to G2 by A2;

      then

       A6: (G1 * F1) is_transformable_to (G2 * F1) by Th10;



       A7: (G1 * F2) is_transformable_to (G2 * F2) by A5, Th10;

      now

        let a be Object of A;



         A8: (G1 . (F1 . a)) = ((G1 * F1) . a) by FUNCTOR0: 33;



         A9: (G2 . (F2 . a)) = ((G2 * F2) . a) by FUNCTOR0: 33;

        then

        reconsider sF2a = (q ! (F2 . a)) as Morphism of ((G1 * F2) . a), ((G2 * F2) . a) by FUNCTOR0: 33;

        reconsider G2ta = ((G2 * p) ! a) as Morphism of (G2 . (F1 . a)), (G2 . (F2 . a)) by A9, FUNCTOR0: 33;



         A10: (G1 . (F2 . a)) = ((G1 * F2) . a) by FUNCTOR0: 33;



         A11: <^(F1 . a), (F2 . a)^> <> {} by A1;



         A12: (G2 . (F1 . a)) = ((G2 * F1) . a) by FUNCTOR0: 33;



        thus (((q * F2) `*` (G1 * p)) ! a) = (((q * F2) ! a) * ((G1 * p) ! a)) by A7, A3, FUNCTOR2:def 5

        .= (sF2a * ((G1 * p) ! a)) by A5, Th12

        .= ((q ! (F2 . a)) * (G1 . (p ! a))) by A1, A8, A10, A9, Th11

        .= ((G2 . (p ! a)) * (q ! (F1 . a))) by A2, A11, FUNCTOR2:def 7

        .= (G2ta * (q ! (F1 . a))) by A1, Th11

        .= (((G2 * p) ! a) * ((q * F1) ! a)) by A5, A8, A12, A9, Th12

        .= (((G2 * p) `*` (q * F1)) ! a) by A6, A4, FUNCTOR2:def 5;

      end;

      hence thesis by A1, A5, Th10, FUNCTOR2: 3;

    end;

    theorem :: FUNCTOR3:23

    F1 is_transformable_to F2 implies (( idt ( id B)) (#) p) = p

    proof

      assume

       A1: F1 is_transformable_to F2;

      then

       A2: (( id B) * F1) is_transformable_to (( id B) * F2) by Th10;



      thus (( idt ( id B)) (#) p) = (( idt (( id B) * F2)) `*` (( id B) * p)) by Th18

      .= (( id B) * p) by A2, FUNCTOR2: 5

      .= p by A1, Th20;

    end;

    theorem :: FUNCTOR3:24

    G1 is_transformable_to G2 implies (q (#) ( idt ( id B))) = q

    proof

      assume

       A1: G1 is_transformable_to G2;

      then

       A2: (G1 * ( id B)) is_transformable_to (G2 * ( id B)) by Th10;



      thus (q (#) ( idt ( id B))) = ((q * ( id B)) `*` ( idt (G1 * ( id B)))) by Th19

      .= (q * ( id B)) by A2, FUNCTOR2: 5

      .= q by A1, Th21;

    end;

    theorem :: FUNCTOR3:25

    F1 is_transformable_to F2 implies (G1 * p) = (( idt G1) (#) p)

    proof

      assume F1 is_transformable_to F2;

      then (G1 * F1) is_transformable_to (G1 * F2) by Th10;



      hence (G1 * p) = (( idt (G1 * F2)) `*` (G1 * p)) by FUNCTOR2: 5

      .= (( idt G1) (#) p) by Th18;

    end;

    theorem :: FUNCTOR3:26

    G1 is_transformable_to G2 implies (q * F1) = (q (#) ( idt F1))

    proof

      assume G1 is_transformable_to G2;

      then (G1 * F1) is_transformable_to (G2 * F1) by Th10;



      hence (q * F1) = ((q * F1) `*` ( idt (G1 * F1))) by FUNCTOR2: 5

      .= (q (#) ( idt F1)) by Th19;

    end;

    reserve A,B,C,D for category,

F1,F2,F3 for covariant Functor of A, B,

G1,G2,G3 for covariant Functor of B, C;

    theorem :: FUNCTOR3:27

    for H1,H2 be covariant Functor of C, D holds for t be transformation of F1, F2, s be transformation of G1, G2 holds for u be transformation of H1, H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds ((u (#) s) (#) t) = (u (#) (s (#) t))

    proof

      let H1,H2 be covariant Functor of C, D, t be transformation of F1, F2, s be transformation of G1, G2, u be transformation of H1, H2;

      assume that

       A1: F1 is_transformable_to F2 and

       A2: G1 is_transformable_to G2 and

       A3: H1 is_transformable_to H2;



       A4: (G1 * F2) is_transformable_to (G2 * F2) & (G1 * F1) is_transformable_to (G1 * F2) by A1, A2, Th10;



       A5: ((H1 * s) * F2) = (H1 * (s * F2)) & ((H1 * G1) * t) = (H1 * (G1 * t)) by A1, A2, Th16, Th17;



       A6: ((H1 * G2) * F2) = (H1 * (G2 * F2)) & ((H2 * G2) * F2) = (H2 * (G2 * F2)) by FUNCTOR0: 32;



       A7: ((H1 * G1) * F1) is_transformable_to ((H1 * G1) * F2) & ((u * G2) * F2) = (u * (G2 * F2)) by A1, A3, Th10, Th15;



       A8: ((H1 * G1) * F1) = (H1 * (G1 * F1)) & ((H1 * G1) * F2) = (H1 * (G1 * F2)) by FUNCTOR0: 32;



       A9: (H1 * G1) is_transformable_to (H1 * G2) by A2, Th10;

      then

       A10: ((H1 * G1) * F2) is_transformable_to ((H1 * G2) * F2) by Th10;



       A11: (H1 * G2) is_transformable_to (H2 * G2) by A3, Th10;

      then

       A12: ((H1 * G2) * F2) is_transformable_to ((H2 * G2) * F2) by Th10;



      thus ((u (#) s) (#) t) = ((((u * G2) * F2) `*` ((H1 * s) * F2)) `*` ((H1 * G1) * t)) by A11, A9, Th14

      .= ((u * (G2 * F2)) `*` ((H1 * (s * F2)) `*` (H1 * (G1 * t)))) by A12, A10, A7, A5, A8, A6, FUNCTOR2: 6

      .= (u (#) (s (#) t)) by A4, Th13;

    end;

    reserve t for natural_transformation of F1, F2,

s for natural_transformation of G1, G2,

s1 for natural_transformation of G2, G3;

     Lm2:

    now

      let A, B, C, F1, F2, G1, G2, s, t;

      set k = (s (#) t);

      assume

       A1: F1 is_naturally_transformable_to F2;

      then

       A2: F1 is_transformable_to F2;

      assume

       A3: G1 is_naturally_transformable_to G2;

      then

       A4: G1 is_transformable_to G2;

       A5:

      now

        let a,b be Object of A such that

         A6: <^a, b^> <> {} ;



         A7: <^((G1 * F1) . a), ((G1 * F1) . b)^> <> {} by A6, FUNCTOR0:def 18;



         A8: ((G2 * F2) . a) = (G2 . (F2 . a)) by FUNCTOR0: 33;

        then

        reconsider sF2a = (s ! (F2 . a)) as Morphism of ((G1 * F2) . a), ((G2 * F2) . a) by FUNCTOR0: 33;



         A9: ((G2 * F2) . b) = (G2 . (F2 . b)) by FUNCTOR0: 33;

        then

        reconsider sF2b = (s ! (F2 . b)) as Morphism of ((G1 * F2) . b), ((G2 * F2) . b) by FUNCTOR0: 33;

         <^(G1 . (F2 . b)), (G2 . (F2 . b))^> <> {} by A4;

        then

         A10: <^((G1 * F2) . b), ((G2 * F2) . b)^> <> {} by A9, FUNCTOR0: 33;

        let f be Morphism of a, b;



         A11: ((G1 * F1) . a) = (G1 . (F1 . a)) by FUNCTOR0: 33;

        then

        reconsider G1tbF1f = (G1 . ((t ! b) * (F1 . f))) as Morphism of ((G1 * F1) . a), ((G1 * F2) . b) by FUNCTOR0: 33;

        reconsider G1ta = (G1 . (t ! a)) as Morphism of ((G1 * F1) . a), ((G1 * F2) . a) by A11, FUNCTOR0: 33;



         A12: <^(G1 . (F1 . a)), (G2 . (F1 . a))^> <> {} by A4;



         A13: ((G1 * F1) . b) = (G1 . (F1 . b)) by FUNCTOR0: 33;

        then

        reconsider G1tb = (G1 . (t ! b)) as Morphism of ((G1 * F1) . b), ((G1 * F2) . b) by FUNCTOR0: 33;



         A14: <^(F1 . b), (F2 . b)^> <> {} by A2;

        then <^(G1 . (F1 . b)), (G1 . (F2 . b))^> <> {} by FUNCTOR0:def 18;

        then

         A15: <^((G1 * F1) . b), ((G1 * F2) . b)^> <> {} by A13, FUNCTOR0: 33;



         A16: <^(F1 . a), (F1 . b)^> <> {} by A6, FUNCTOR0:def 18;

        then

         A17: <^(F1 . a), (F2 . b)^> <> {} by A14, ALTCAT_1:def 2;

        reconsider G1F1f = (G1 . (F1 . f)) as Morphism of ((G1 * F1) . a), ((G1 * F1) . b) by A13, FUNCTOR0: 33;



         A18: (s ! (F2 . a)) = ((s * F2) . a) by A4, Def2;



         A19: (G1 . ((t ! b) * (F1 . f))) = ((G1 . (t ! b)) * (G1 . (F1 . f))) by A14, A16, FUNCTOR0:def 23

        .= (G1tb * G1F1f) by A11, A13, FUNCTOR0: 33;

        reconsider G2F2f = (G2 . (F2 . f)) as Morphism of ((G2 * F2) . a), ((G2 * F2) . b) by A8, FUNCTOR0: 33;



         A20: (s ! (F2 . b)) = ((s * F2) . b) by A4, Def2;



         A21: (G1 * F2) is_transformable_to (G2 * F2) by A4, Th10;



         A22: <^(F2 . a), (F2 . b)^> <> {} by A6, FUNCTOR0:def 18;

        then

         A23: <^(G2 . (F2 . a)), (G2 . (F2 . b))^> <> {} by FUNCTOR0:def 18;



         A24: <^(F1 . a), (F2 . a)^> <> {} by A2;

        then

         A25: <^(G2 . (F1 . a)), (G2 . (F2 . a))^> <> {} by FUNCTOR0:def 18;



         A26: (G1 * F1) is_transformable_to (G1 * F2) by A2, Th10;



        hence ((k ! b) * ((G1 * F1) . f)) = ((((s * F2) ! b) * ((G1 * t) ! b)) * ((G1 * F1) . f)) by A21, FUNCTOR2:def 5

        .= ((sF2b * ((G1 * t) ! b)) * ((G1 * F1) . f)) by A21, A20, FUNCTOR2:def 4

        .= ((sF2b * G1tb) * ((G1 * F1) . f)) by A2, Th11

        .= ((sF2b * G1tb) * G1F1f) by A6, Th6

        .= (sF2b * G1tbF1f) by A7, A15, A10, A19, ALTCAT_1: 21

        .= ((s ! (F2 . b)) * (G1 . ((t ! b) * (F1 . f)))) by A11, A9, FUNCTOR0: 33

        .= ((G2 . ((t ! b) * (F1 . f))) * (s ! (F1 . a))) by A3, A17, FUNCTOR2:def 7

        .= ((G2 . ((F2 . f) * (t ! a))) * (s ! (F1 . a))) by A1, A6, FUNCTOR2:def 7

        .= (((G2 . (F2 . f)) * (G2 . (t ! a))) * (s ! (F1 . a))) by A22, A24, FUNCTOR0:def 23

        .= ((G2 . (F2 . f)) * ((G2 . (t ! a)) * (s ! (F1 . a)))) by A12, A25, A23, ALTCAT_1: 21

        .= ((G2 . (F2 . f)) * ((s ! (F2 . a)) * (G1 . (t ! a)))) by A3, A24, FUNCTOR2:def 7

        .= (G2F2f * (sF2a * G1ta)) by A11, A8, A9, FUNCTOR0: 33

        .= (((G2 * F2) . f) * (sF2a * G1ta)) by A6, Th6

        .= (((G2 * F2) . f) * (((s * F2) ! a) * G1ta)) by A21, A18, FUNCTOR2:def 4

        .= (((G2 * F2) . f) * (((s * F2) ! a) * ((G1 * t) ! a))) by A2, Th11

        .= (((G2 * F2) . f) * (k ! a)) by A21, A26, FUNCTOR2:def 5;

      end;

      thus (G1 * F1) is_naturally_transformable_to (G2 * F2) by A2, A4, Th10, A5;

      hence (s (#) t) is natural_transformation of (G1 * F1), (G2 * F2) by A5, FUNCTOR2:def 7;

    end;

    theorem :: FUNCTOR3:28



     Th28: F1 is_naturally_transformable_to F2 implies (G1 * t) is natural_transformation of (G1 * F1), (G1 * F2)

    proof

      assume

       A1: F1 is_naturally_transformable_to F2;

      then

       A2: F1 is_transformable_to F2;

      thus (G1 * F1) is_naturally_transformable_to (G1 * F2) by A1, Lm2;

      let a,b be Object of A such that

       A3: <^a, b^> <> {} ;



       A4: ((G1 * F1) . b) = (G1 . (F1 . b)) & <^(F1 . a), (F1 . b)^> <> {} by A3, FUNCTOR0: 33, FUNCTOR0:def 18;



       A5: <^(F1 . b), (F2 . b)^> <> {} by A2;



       A6: <^(F1 . a), (F2 . a)^> <> {} by A2;

      reconsider G1ta = (G1 . (t ! a)) as Morphism of (G1 . (F1 . a)), ((G1 * F2) . a) by FUNCTOR0: 33;

      reconsider G1tb = (G1 . (t ! b)) as Morphism of ((G1 * F1) . b), (G1 . (F2 . b)) by FUNCTOR0: 33;

      let f be Morphism of a, b;



       A7: ((G1 * F2) . a) = (G1 . (F2 . a)) by FUNCTOR0: 33;



       A8: <^(F2 . a), (F2 . b)^> <> {} by A3, FUNCTOR0:def 18;



       A9: ((G1 * F1) . a) = (G1 . (F1 . a)) by FUNCTOR0: 33;

      then

      reconsider G1F1f = (G1 . (F1 . f)) as Morphism of ((G1 * F1) . a), ((G1 * F1) . b) by FUNCTOR0: 33;



       A10: ((G1 * F2) . b) = (G1 . (F2 . b)) by FUNCTOR0: 33;



      hence (((G1 * t) ! b) * ((G1 * F1) . f)) = (G1tb * ((G1 * F1) . f)) by A2, Th11

      .= (G1tb * G1F1f) by A3, Th6

      .= (G1 . ((t ! b) * (F1 . f))) by A9, A4, A5, FUNCTOR0:def 23

      .= (G1 . ((F2 . f) * (t ! a))) by A1, A3, FUNCTOR2:def 7

      .= ((G1 . (F2 . f)) * (G1 . (t ! a))) by A6, A8, FUNCTOR0:def 23

      .= (((G1 * F2) . f) * G1ta) by A3, A7, A10, Th6

      .= (((G1 * F2) . f) * ((G1 * t) ! a)) by A2, A9, Th11;

    end;

    theorem :: FUNCTOR3:29



     Th29: G1 is_naturally_transformable_to G2 implies (s * F1) is natural_transformation of (G1 * F1), (G2 * F1)

    proof

      assume

       A1: G1 is_naturally_transformable_to G2;

      thus (G1 * F1) is_naturally_transformable_to (G2 * F1) by A1, Lm2;

      let a,b be Object of A such that

       A2: <^a, b^> <> {} ;



       A3: <^(F1 . a), (F1 . b)^> <> {} by A2, FUNCTOR0:def 18;

      reconsider sF1a = (s ! (F1 . a)) as Morphism of (G1 . (F1 . a)), ((G2 * F1) . a) by FUNCTOR0: 33;

      let f be Morphism of a, b;



       A4: ((G2 * F1) . a) = (G2 . (F1 . a)) by FUNCTOR0: 33;



       A5: ((G2 * F1) . b) = (G2 . (F1 . b)) by FUNCTOR0: 33;

      then

      reconsider sF1b = (s ! (F1 . b)) as Morphism of ((G1 * F1) . b), ((G2 * F1) . b) by FUNCTOR0: 33;



       A6: ((G1 * F1) . b) = (G1 . (F1 . b)) & ((G2 * F1) . b) = (G2 . (F1 . b)) by FUNCTOR0: 33;



       A7: ((G1 * F1) . a) = (G1 . (F1 . a)) by FUNCTOR0: 33;

      then

      reconsider G1F1f = (G1 . (F1 . f)) as Morphism of ((G1 * F1) . a), ((G1 * F1) . b) by FUNCTOR0: 33;



       A8: G1 is_transformable_to G2 by A1;



      hence (((s * F1) ! b) * ((G1 * F1) . f)) = (sF1b * ((G1 * F1) . f)) by Th12

      .= (sF1b * G1F1f) by A2, Th6

      .= ((G2 . (F1 . f)) * (s ! (F1 . a))) by A1, A7, A6, A3, FUNCTOR2:def 7

      .= (((G2 * F1) . f) * sF1a) by A2, A4, A5, Th6

      .= (((G2 * F1) . f) * ((s * F1) ! a)) by A8, A7, Th12;

    end;

    theorem :: FUNCTOR3:30

    F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies (G1 * F1) is_naturally_transformable_to (G2 * F2) & (s (#) t) is natural_transformation of (G1 * F1), (G2 * F2) by Lm2;

    theorem :: FUNCTOR3:31

    for t be transformation of F1, F2, t1 be transformation of F2, F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds ((s1 `*` s) (#) (t1 `*` t)) = ((s1 (#) t1) `*` (s (#) t))

    proof

      let t be transformation of F1, F2, t1 be transformation of F2, F3 such that

       A1: F1 is_naturally_transformable_to F2 and

       A2: F2 is_naturally_transformable_to F3 and

       A3: G1 is_naturally_transformable_to G2 and

       A4: G2 is_naturally_transformable_to G3;



       A5: F1 is_transformable_to F2 by A1;

      then

       A6: (s (#) t) = ((G2 * t) `*` (s * F1)) by A3, Th22;



       A7: (G2 * F1) is_transformable_to (G2 * F2) by A5, Th10;



       A8: (G3 * F1) is_transformable_to (G3 * F2) by A5, Th10;

      (G1 * F1) is_naturally_transformable_to (G2 * F2) by A1, A3, Lm2;

      then

       A9: (G1 * F1) is_transformable_to (G2 * F2);



       A10: G1 is_transformable_to G2 by A3;

      then

       A11: (G1 * F1) is_transformable_to (G2 * F1) by Th10;



       A12: F2 is_transformable_to F3 by A2;

      then

       A13: (s1 (#) t1) = ((G3 * t1) `*` (s1 * F2)) by A4, Th22;



       A14: (G3 * F2) is_transformable_to (G3 * F3) by A12, Th10;



       A15: G2 is_transformable_to G3 by A4;

      then

       A16: (G2 * F1) is_transformable_to (G3 * F1) by Th10;

      G1 is_transformable_to G3 by A10, A15, FUNCTOR2: 2;

      then

       A17: (G1 * F1) is_transformable_to (G3 * F1) by Th10;



       A18: (G2 * F2) is_transformable_to (G3 * F2) by A15, Th10;

      F1 is_transformable_to F3 by A5, A12, FUNCTOR2: 2;



      hence ((s1 `*` s) (#) (t1 `*` t)) = ((G3 * (t1 `*` t)) `*` ((s1 `*` s) * F1)) by A3, A4, Th22, FUNCTOR2: 8

      .= (((G3 * t1) `*` (G3 * t)) `*` ((s1 `*` s) * F1)) by A5, A12, Th13

      .= (((G3 * t1) `*` (G3 * t)) `*` ((s1 qua transformation of G2, G3 `*` s) * F1)) by A3, A4, FUNCTOR2:def 8

      .= (((G3 * t1) `*` (G3 * t)) `*` ((s1 * F1) `*` (s * F1))) by A10, A15, Th14

      .= ((G3 * t1) `*` ((G3 * t) `*` ((s1 * F1) `*` (s * F1)))) by A14, A8, A17, FUNCTOR2: 6

      .= ((G3 * t1) `*` (((G3 * t) `*` (s1 * F1)) `*` (s * F1))) by A8, A11, A16, FUNCTOR2: 6

      .= ((G3 * t1) `*` ((s1 (#) t) `*` (s * F1))) by A4, A5, Th22

      .= ((G3 * t1) `*` ((s1 * F2) `*` ((G2 * t) `*` (s * F1)))) by A11, A18, A7, FUNCTOR2: 6

      .= ((s1 (#) t1) `*` (s (#) t)) by A14, A18, A9, A13, A6, FUNCTOR2: 6;

    end;

    begin

    theorem :: FUNCTOR3:32



     Th32: F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & (for a be Object of A holds (t ! a) is iso) implies F2 is_naturally_transformable_to F1 & ex f be natural_transformation of F2, F1 st for a be Object of A holds (f . a) = ((t ! a) " ) & (f ! a) is iso

    proof

      assume that

       A1: F1 is_naturally_transformable_to F2 and

       A2: F2 is_transformable_to F1 and

       A3: for a be Object of A holds (t ! a) is iso;

      defpred P[ object, object] means ex a be Object of A st a = $1 & $2 = ((t ! a) " );

      set I = the carrier of A;



       A4: for i be object st i in I holds ex j be object st P[i, j]

      proof

        let i be object;

        assume i in I;

        then

        reconsider o = i as Object of A;

        take ((t ! o) " );

        thus thesis;

      end;

      consider f be ManySortedSet of I such that

       A5: for i be object st i in I holds P[i, (f . i)] from PBOOLE:sch 3( A4);

      f is transformation of F2, F1

      proof

        thus F2 is_transformable_to F1 by A2;

        let a be Object of A;

        ex b be Object of A st b = a & (f . a) = ((t ! b) " ) by A5;

        hence thesis;

      end;

      then

      reconsider f as transformation of F2, F1;



       A6: F1 is_transformable_to F2 by A1;

       A7:

      now

        let a,b be Object of A such that

         A8: <^a, b^> <> {} ;



         A9: <^(F1 . a), (F1 . b)^> <> {} by A8, FUNCTOR0:def 18;

        let g be Morphism of a, b;



         A10: ex bb be Object of A st bb = b & (f . b) = ((t ! bb) " ) by A5;



         A11: (t ! b) is iso by A3;



         A12: <^(F2 . a), (F1 . a)^> <> {} by A2;



         A13: <^(F1 . a), (F2 . a)^> <> {} by A6;



         A14: ex aa be Object of A st aa = a & (f . a) = ((t ! aa) " ) by A5;

        then

        reconsider fa = (f . a) as Morphism of (F2 . a), (F1 . a);



         A15: (t ! a) is iso by A3;



         A16: <^(F1 . b), (F2 . b)^> <> {} by A6;



         A17: <^(F2 . b), (F1 . b)^> <> {} by A2;



         A18: <^(F2 . a), (F2 . b)^> <> {} by A8, FUNCTOR0:def 18;

        then

         A19: <^(F2 . a), (F1 . b)^> <> {} by A17, ALTCAT_1:def 2;



        hence ((f ! b) * (F2 . g)) = (((f ! b) * (F2 . g)) * ( idm (F2 . a))) by ALTCAT_1:def 17

        .= (((f ! b) * (F2 . g)) * ((t ! a) * fa)) by A14, A15, ALTCAT_3:def 5

        .= (((f ! b) * (F2 . g)) * ((t ! a) * (f ! a))) by A2, FUNCTOR2:def 4

        .= ((((f ! b) * (F2 . g)) * (t ! a)) * (f ! a)) by A13, A12, A19, ALTCAT_1: 21

        .= (((f ! b) * ((F2 . g) * (t ! a))) * (f ! a)) by A13, A17, A18, ALTCAT_1: 21

        .= (((f ! b) * ((t ! b) * (F1 . g))) * (f ! a)) by A1, A8, FUNCTOR2:def 7

        .= ((((f ! b) * (t ! b)) * (F1 . g)) * (f ! a)) by A17, A16, A9, ALTCAT_1: 21

        .= (((((t ! b) " ) * (t ! b)) * (F1 . g)) * (f ! a)) by A2, A10, FUNCTOR2:def 4

        .= ((( idm (F1 . b)) * (F1 . g)) * (f ! a)) by A11, ALTCAT_3:def 5

        .= ((F1 . g) * (f ! a)) by A9, ALTCAT_1: 20;

      end;

      hence F2 is_naturally_transformable_to F1 by A2;

      F2 is_naturally_transformable_to F1 by A2, A7;

      then

      reconsider f as natural_transformation of F2, F1 by A7, FUNCTOR2:def 7;

      take f;

      let a be Object of A;

      consider b be Object of A such that

       A20: b = a and

       A21: (f . a) = ((t ! b) " ) by A5;

      thus (f . a) = ((t ! a) " ) by A20, A21;



       A22: <^(F1 . a), (F2 . a)^> <> {} by A6;



       A23: <^(F2 . a), (F1 . a)^> <> {} by A2;

      (f ! a) = ((t ! b) " ) by A2, A21, FUNCTOR2:def 4;

      hence thesis by A3, A20, A22, A23, ALTCAT_4: 3;

    end;

    definition

      let A,B be category, F1,F2 be covariant Functor of A, B;

      :: FUNCTOR3:def4

      pred F1,F2 are_naturally_equivalent means

      : Def4: F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ex t be natural_transformation of F1, F2 st for a be Object of A holds (t ! a) is iso;

      reflexivity

      proof

        let F be covariant Functor of A, B;

        thus F is_naturally_transformable_to F & F is_transformable_to F;

        take ( idt F);

        let a be Object of A;

        (( idt F) ! a) = ( idm (F . a)) by FUNCTOR2: 4;

        hence thesis;

      end;

      symmetry

      proof

        let F1,F2 be covariant Functor of A, B such that

         A1: F1 is_naturally_transformable_to F2 and

         A2: F2 is_transformable_to F1;

        given t be natural_transformation of F1, F2 such that

         A3: for a be Object of A holds (t ! a) is iso;

        consider f be natural_transformation of F2, F1 such that

         A4: for a be Object of A holds (f . a) = ((t ! a) " ) & (f ! a) is iso by A1, A2, A3, Th32;

        thus F2 is_naturally_transformable_to F1 by A1, A2, A3, Th32;

        thus F1 is_transformable_to F2 by A1;

        take f;

        thus thesis by A4;

      end;

    end

    definition

      let A,B be category, F1,F2 be covariant Functor of A, B;

      :: FUNCTOR3:def5

      mode natural_equivalence of F1,F2 -> natural_transformation of F1, F2 means

      : Def5: for a be Object of A holds (it ! a) is iso;

      existence by A1;

    end

    reserve e for natural_equivalence of F1, F2,

e1 for natural_equivalence of F2, F3,

f for natural_equivalence of G1, G2;

    theorem :: FUNCTOR3:33



     Th33: (F1,F2) are_naturally_equivalent & (F2,F3) are_naturally_equivalent implies (F1,F3) are_naturally_equivalent

    proof

      assume that

       A1: F1 is_naturally_transformable_to F2 and

       A2: F2 is_transformable_to F1;

      given t be natural_transformation of F1, F2 such that

       A3: for a be Object of A holds (t ! a) is iso;

      assume that

       A4: F2 is_naturally_transformable_to F3 and

       A5: F3 is_transformable_to F2;

      given t1 be natural_transformation of F2, F3 such that

       A6: for a be Object of A holds (t1 ! a) is iso;

      thus F1 is_naturally_transformable_to F3 & F3 is_transformable_to F1 by A1, A2, A4, A5, FUNCTOR2: 2, FUNCTOR2: 8;

      take (t1 `*` t);

      let a be Object of A;



       A7: (t1 ! a) is iso by A6;

      F3 is_transformable_to F1 by A2, A5, FUNCTOR2: 2;

      then

       A8: <^(F3 . a), (F1 . a)^> <> {} ;



       A9: (t ! a) is iso by A3;



       A10: F2 is_transformable_to F3 by A4;

      then

       A11: <^(F2 . a), (F3 . a)^> <> {} ;



       A12: F1 is_transformable_to F2 by A1;

      then

       A13: <^(F1 . a), (F2 . a)^> <> {} ;

      ((t1 `*` t) ! a) = ((t1 qua transformation of F2, F3 `*` t) ! a) by A1, A4, FUNCTOR2:def 8

      .= ((t1 ! a) * (t ! a)) by A12, A10, FUNCTOR2:def 5;

      hence thesis by A13, A11, A8, A7, A9, ALTCAT_3: 7;

    end;

    theorem :: FUNCTOR3:34



     Th34: (F1,F2) are_naturally_equivalent & (F2,F3) are_naturally_equivalent implies (e1 `*` e) is natural_equivalence of F1, F3

    proof

      assume that

       A1: (F1,F2) are_naturally_equivalent and

       A2: (F2,F3) are_naturally_equivalent ;

      thus

       A3: (F1,F3) are_naturally_equivalent by A1, A2, Th33;

      let a be Object of A;



       A4: F1 is_transformable_to F2 by A1, Def4;

      then

       A5: <^(F1 . a), (F2 . a)^> <> {} ;

      F3 is_transformable_to F1 by A3;

      then

       A6: <^(F3 . a), (F1 . a)^> <> {} ;



       A7: F2 is_transformable_to F3 by A2, Def4;

      then

       A8: <^(F2 . a), (F3 . a)^> <> {} ;

      F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 by A1, A2;



      then

       A9: ((e1 `*` e) ! a) = ((e1 qua transformation of F2, F3 `*` e) ! a) by FUNCTOR2:def 8

      .= ((e1 ! a) * (e ! a)) by A4, A7, FUNCTOR2:def 5;

      (e1 ! a) is iso & (e ! a) is iso by A1, A2, Def5;

      hence thesis by A9, A5, A8, A6, ALTCAT_3: 7;

    end;

    theorem :: FUNCTOR3:35



     Th35: (F1,F2) are_naturally_equivalent implies ((G1 * F1),(G1 * F2)) are_naturally_equivalent & (G1 * e) is natural_equivalence of (G1 * F1), (G1 * F2)

    proof

      assume

       A1: (F1,F2) are_naturally_equivalent ;

      then

       A2: F2 is_transformable_to F1;



       A3: F1 is_naturally_transformable_to F2 by A1;

      then

      reconsider k = (G1 * e) as natural_transformation of (G1 * F1), (G1 * F2) by Th28;



       A4: F1 is_transformable_to F2 by A1, Def4;

       A5:

      now

        let a be Object of A;



         A6: ((G1 * F1) . a) = (G1 . (F1 . a)) & ((G1 * F2) . a) = (G1 . (F2 . a)) by FUNCTOR0: 33;



         A7: <^(F2 . a), (F1 . a)^> <> {} by A2;

        (k ! a) = (G1 . (e ! a)) & <^(F1 . a), (F2 . a)^> <> {} by A4, Th11;

        hence (k ! a) is iso by A1, A6, A7, Def5, ALTCAT_4: 20;

      end;

      ((G1 * F1),(G1 * F2)) are_naturally_equivalent by A3, Lm2, A2, Th10, A5;

      hence thesis by A5, Def5;

    end;

    theorem :: FUNCTOR3:36



     Th36: (G1,G2) are_naturally_equivalent implies ((G1 * F1),(G2 * F1)) are_naturally_equivalent & (f * F1) is natural_equivalence of (G1 * F1), (G2 * F1)

    proof

      assume

       A1: (G1,G2) are_naturally_equivalent ;

      then G1 is_naturally_transformable_to G2;

      then

      reconsider k = (f * F1) as natural_transformation of (G1 * F1), (G2 * F1) by Th29;

       A2:

      now

        let a be Object of A;

        G1 is_transformable_to G2 by A1, Def4;

        then

         A3: (k ! a) = (f ! (F1 . a)) by Th12;

        ((G1 * F1) . a) = (G1 . (F1 . a)) & ((G2 * F1) . a) = (G2 . (F1 . a)) by FUNCTOR0: 33;

        hence (k ! a) is iso by A1, A3, Def5;

      end;

      ((G1 * F1),(G2 * F1)) are_naturally_equivalent by Lm2, A1, Th10, A2;

      hence thesis by A2, Def5;

    end;

    theorem :: FUNCTOR3:37

    (F1,F2) are_naturally_equivalent & (G1,G2) are_naturally_equivalent implies ((G1 * F1),(G2 * F2)) are_naturally_equivalent & (f (#) e) is natural_equivalence of (G1 * F1), (G2 * F2)

    proof

      assume that

       A1: (F1,F2) are_naturally_equivalent and

       A2: (G1,G2) are_naturally_equivalent ;



       A3: ((G1 * F1),(G1 * F2)) are_naturally_equivalent by A1, Th35;

      G1 is_naturally_transformable_to G2 by A2;

      then

      reconsider sF2 = (f * F2) as natural_transformation of (G1 * F2), (G2 * F2) by Th29;

      F1 is_naturally_transformable_to F2 by A1;

      then

      reconsider G1t = (G1 * e) as natural_transformation of (G1 * F1), (G1 * F2) by Th28;



       A4: ((G1 * F2),(G2 * F2)) are_naturally_equivalent by A2, Th36;

      (f * F2) is natural_equivalence of (G1 * F2), (G2 * F2) & (G1 * e) is natural_equivalence of (G1 * F1), (G1 * F2) by A1, A2, Th35, Th36;

      then (sF2 `*` G1t) is natural_equivalence of (G1 * F1), (G2 * F2) by A4, A3, Th34;

      hence thesis by A4, A3, Th33, FUNCTOR2:def 8;

    end;

    definition

      let A,B be category, F1,F2 be covariant Functor of A, B, e be natural_equivalence of F1, F2;

      :: FUNCTOR3:def6

      func e " -> natural_equivalence of F2, F1 means

      : Def6: for a be Object of A holds (it . a) = ((e ! a) " );

      existence

      proof



         A2: for a be Object of A holds (e ! a) is iso by A1, Def5;

        F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 by A1;

        then

        consider f be natural_transformation of F2, F1 such that

         A3: for a be Object of A holds (f . a) = ((e ! a) " ) & (f ! a) is iso by A2, Th32;

        f is natural_equivalence of F2, F1

        proof

          thus (F2,F1) are_naturally_equivalent by A1;

          let a be Object of A;

          thus thesis by A3;

        end;

        then

        reconsider f as natural_equivalence of F2, F1;

        take f;

        let a be Object of A;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let P,R be natural_equivalence of F2, F1 such that

         A4: for a be Object of A holds (P . a) = ((e ! a) " ) and

         A5: for a be Object of A holds (R . a) = ((e ! a) " );



         A6: F2 is_transformable_to F1 by A1;

        now

          let a be Object of A;



          thus (P ! a) = (P . a) by A6, FUNCTOR2:def 4

          .= ((e ! a) " ) by A4

          .= (R . a) by A5

          .= (R ! a) by A6, FUNCTOR2:def 4;

        end;

        hence P = R by A6, FUNCTOR2: 3;

      end;

    end

    theorem :: FUNCTOR3:38



     Th38: for o be Object of A st (F1,F2) are_naturally_equivalent holds ((e " ) ! o) = ((e ! o) " )

    proof

      let o be Object of A;

      assume

       A1: (F1,F2) are_naturally_equivalent ;

      then F2 is_transformable_to F1;



      hence ((e " ) ! o) = ((e " ) . o) by FUNCTOR2:def 4

      .= ((e ! o) " ) by A1, Def6;

    end;

    theorem :: FUNCTOR3:39



     Th39: (F1,F2) are_naturally_equivalent implies (e `*` (e " )) = ( idt F2)

    proof

      assume

       A1: (F1,F2) are_naturally_equivalent ;

      then

       A2: F1 is_transformable_to F2 & F2 is_transformable_to F1 by Def4;



       A3: F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F1 by A1, Def4;

      now

        let a be Object of A;



         A4: (e ! a) is iso by A1, Def5;



        thus ((e `*` (e " )) ! a) = ((e qua transformation of F1, F2 `*` (e " )) ! a) by A3, FUNCTOR2:def 8

        .= ((e ! a) * ((e " ) ! a)) by A2, FUNCTOR2:def 5

        .= ((e ! a) * ((e ! a) " )) by A1, Th38

        .= ( idm (F2 . a)) by A4, ALTCAT_3:def 5

        .= (( idt F2) ! a) by FUNCTOR2: 4;

      end;

      hence thesis by FUNCTOR2: 3;

    end;

    theorem :: FUNCTOR3:40

    (F1,F2) are_naturally_equivalent implies ((e " ) `*` e) = ( idt F1)

    proof

      assume

       A1: (F1,F2) are_naturally_equivalent ;

      then

       A2: F1 is_transformable_to F2 & F2 is_transformable_to F1 by Def4;



       A3: F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F1 by A1, Def4;

      now

        let a be Object of A;



         A4: (e ! a) is iso by A1, Def5;



        thus (((e " ) `*` e) ! a) = (((e " ) `*` e qua transformation of F1, F2) ! a) by A3, FUNCTOR2:def 8

        .= (((e " ) ! a) * (e ! a)) by A2, FUNCTOR2:def 5

        .= (((e ! a) " ) * (e ! a)) by A1, Th38

        .= ( idm (F1 . a)) by A4, ALTCAT_3:def 5

        .= (( idt F1) ! a) by FUNCTOR2: 4;

      end;

      hence thesis by FUNCTOR2: 3;

    end;

    definition

      let A,B be category, F be covariant Functor of A, B;

      :: original: idt

      redefine

      func idt F -> natural_equivalence of F, F ;

      coherence

      proof

        set e = the natural_equivalence of F, F;

        (e `*` (e " )) = ( idt F) by Th39;

        hence thesis by Th34;

      end;

    end

    theorem :: FUNCTOR3:41

    (F1,F2) are_naturally_equivalent implies ((e " ) " ) = e

    proof

      assume

       A1: (F1,F2) are_naturally_equivalent ;

      then

       A2: F1 is_transformable_to F2 by Def4;

      now

        let a be Object of A;



         A3: <^(F1 . a), (F2 . a)^> <> {} by A2;

        F2 is_transformable_to F1 by A1;

        then

         A4: <^(F2 . a), (F1 . a)^> <> {} ;

        (e ! a) is iso by A1, Def5;

        then

         A5: (e ! a) is retraction coretraction by ALTCAT_3: 5;



        thus (((e " ) " ) ! a) = (((e " ) ! a) " ) by A1, Th38

        .= (((e ! a) " ) " ) by A1, Th38

        .= (e ! a) by A3, A4, A5, ALTCAT_3: 3;

      end;

      hence thesis by A2, FUNCTOR2: 3;

    end;

    theorem :: FUNCTOR3:42

    for k be natural_equivalence of F1, F3 st k = (e1 `*` e) & (F1,F2) are_naturally_equivalent & (F2,F3) are_naturally_equivalent holds (k " ) = ((e " ) `*` (e1 " ))

    proof

      let k be natural_equivalence of F1, F3 such that

       A1: k = (e1 `*` e) and

       A2: (F1,F2) are_naturally_equivalent and

       A3: (F2,F3) are_naturally_equivalent ;



       A4: F3 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F1 by A2, A3, Def4;



       A5: F1 is_transformable_to F2 & F2 is_transformable_to F3 by A2, A3, Def4;



       A6: F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 by A2, A3;



       A7: F3 is_transformable_to F2 & F2 is_transformable_to F1 by A2, A3;

      then

       A8: F3 is_transformable_to F1 by FUNCTOR2: 2;

      now

        let a be Object of A;



         A9: <^(F1 . a), (F2 . a)^> <> {} & <^(F2 . a), (F3 . a)^> <> {} by A5;



         A10: <^(F3 . a), (F1 . a)^> <> {} by A8;



         A11: (e ! a) is iso & (e1 ! a) is iso by A2, A3, Def5;



        thus ((k " ) ! a) = (((e1 `*` e) ! a) " ) by A1, A2, A3, Th33, Th38

        .= (((e1 qua transformation of F2, F3 `*` e) ! a) " ) by A6, FUNCTOR2:def 8

        .= (((e1 ! a) * (e ! a)) " ) by A5, FUNCTOR2:def 5

        .= (((e ! a) " ) * ((e1 ! a) " )) by A11, A9, A10, ALTCAT_3: 7

        .= (((e ! a) " ) * ((e1 " ) ! a)) by A3, Th38

        .= (((e " ) ! a) * ((e1 " ) ! a)) by A2, Th38

        .= (((e " ) qua transformation of F2, F1 `*` (e1 " )) ! a) by A7, FUNCTOR2:def 5

        .= (((e " ) `*` (e1 " )) ! a) by A4, FUNCTOR2:def 8;

      end;

      hence thesis by A7, FUNCTOR2: 2, FUNCTOR2: 3;

    end;

    theorem :: FUNCTOR3:43

    (( idt F1) " ) = ( idt F1)

    proof

      now

        let a be Object of A;



        thus ((( idt F1) " ) ! a) = ((( idt F1) ! a) " ) by Th38

        .= (( idm (F1 . a)) " ) by FUNCTOR2: 4

        .= ( idm (F1 . a)) by ALTCAT_3: 4

        .= (( idt F1) ! a) by FUNCTOR2: 4;

      end;

      hence thesis by FUNCTOR2: 3;

    end;