nattra_1.miz



    begin

    reserve A,B,C for Category,

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

G for Functor of B, C;

    reserve m,o for set;

    ::$Canceled

    theorem :: NATTRA_1:5

    

     Th1: for a be Object of A holds [ [( id a), ( id a)], ( id a)] in the Comp of A

    proof

      let a be Object of A;

      

       A1: ( dom ( id a)) = a;

      

       A2: ( cod ( id a)) = a;

      then

       A3: [( id a), ( id a)] in ( dom the Comp of A) by A1, CAT_1: 15;

      (( id a) (*) ( id a)) = ( id a) by A1, CAT_1: 22;

      then (the Comp of A . (( id a),( id a))) = ( id a) by A1, A2, CAT_1: 16;

      hence thesis by A3, FUNCT_1:def 2;

    end;

    theorem :: NATTRA_1:6

    

     Th2: the Comp of ( 1Cat (o,m)) = { [ [m, m], m]}

    proof

      set A = ( 1Cat (o,m));

      reconsider f = m as Morphism of A by TARSKI:def 1;

      set a = the Object of A;

      thus the Comp of A c= { [ [m, m], m]}

      proof

        set o9 = the Object of A;

        let x be object;

        

         A1: ( dom ( id o9)) = o9;

        

         A2: ( cod ( id o9)) = o9;

        assume

         A3: x in the Comp of A;

        then

        consider x1,x2 be object such that

         A4: x = [x1, x2] by RELAT_1:def 1;

        

         A5: x1 in ( dom the Comp of A) by A3, A4, XTUPLE_0:def 12;

        ( dom the Comp of A) c= [:the carrier' of A, the carrier' of A:] by RELAT_1:def 18;

        then

        consider x11,x12 be object such that

         A6: x11 in the carrier' of A and

         A7: x12 in the carrier' of A and

         A8: x1 = [x11, x12] by A5, ZFMISC_1:def 2;

        

         A9: x12 = ( id o9) by A7, ZFMISC_1:def 10;

        

         A10: x2 is set by TARSKI: 1;

        x11 = ( id o9) by A6, ZFMISC_1:def 10;

        then x2 = (the Comp of A . (( id o9),( id o9))) by A3, A4, A5, A8, A9, FUNCT_1:def 2, A10;

        then x2 = (( id o9) (*) ( id o9) qua Morphism of A) by A1, A2, CAT_1: 16;

        then

         A11: x2 = m by TARSKI:def 1;

        

         A12: x12 = m by A7, TARSKI:def 1;

        x11 = m by A6, TARSKI:def 1;

        hence thesis by A4, A8, A12, A11, TARSKI:def 1;

      end;

      let x be object;

      assume x in { [ [m, m], m]};

      then

       A13: x = [ [m, m], m] by TARSKI:def 1;

      f = ( id a) by TARSKI:def 1;

      hence thesis by A13, Th1;

    end;

    theorem :: NATTRA_1:7

    

     Th3: for a be Object of A holds ( 1Cat (a,( id a))) is Subcategory of A

    proof

      let d be Object of A;

      thus the carrier of ( 1Cat (d,( id d))) c= the carrier of A

      proof

        let b be object;

        assume b in the carrier of ( 1Cat (d,( id d)));

        then b = d by TARSKI:def 1;

        hence thesis;

      end;

      thus for a,b be Object of ( 1Cat (d,( id d))), a9,b9 be Object of A st a = a9 & b = b9 holds ( Hom (a,b)) c= ( Hom (a9,b9))

      proof

        let a,b be Object of ( 1Cat (d,( id d))), a9,b9 be Object of A;

        assume that

         A1: a = a9 and

         A2: b = b9;

        

         A3: b9 = d by A2, TARSKI:def 1;

        let x be object;

        assume x in ( Hom (a,b));

        then

         A4: x = ( id d) by TARSKI:def 1;

        a9 = d by A1, TARSKI:def 1;

        hence thesis by A3, A4, CAT_1: 27;

      end;

      thus the Comp of ( 1Cat (d,( id d))) c= the Comp of A

      proof

        let x be object;

        assume x in the Comp of ( 1Cat (d,( id d)));

        then x in { [ [( id d), ( id d)], ( id d)]} by Th2;

        then x = [ [( id d), ( id d)], ( id d)] by TARSKI:def 1;

        hence thesis by Th1;

      end;

      let a be Object of ( 1Cat (d,( id d))), a9 be Object of A;

      assume a = a9;

      then a9 = d by TARSKI:def 1;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: NATTRA_1:8

    

     Th4: for C be Subcategory of A holds the Source of C = (the Source of A | the carrier' of C) & the Target of C = (the Target of A | the carrier' of C) & the Comp of C = (the Comp of A || the carrier' of C)

    proof

      let C be Subcategory of A;

      

       A1: ( dom the Source of A) = the carrier' of A by FUNCT_2:def 1;

       A2:

      now

        let x be object;

        assume x in ( dom the Source of C);

        then

        reconsider m = x as Morphism of C by FUNCT_2:def 1;

        reconsider m9 = m as Morphism of A by CAT_2: 8;

        

        thus (the Source of C . x) = ( dom m)

        .= ( dom m9) by CAT_2: 9

        .= (the Source of A . x);

      end;

       A3:

      now

        let x be object;

        assume x in ( dom the Target of C);

        then

        reconsider m = x as Morphism of C by FUNCT_2:def 1;

        reconsider m9 = m as Morphism of A by CAT_2: 8;

        

        thus (the Target of C . x) = ( cod m)

        .= ( cod m9) by CAT_2: 9

        .= (the Target of A . x);

      end;

      ( dom the Source of C) = the carrier' of C by FUNCT_2:def 1;

      then ( dom the Source of C) = (( dom the Source of A) /\ the carrier' of C) by A1, CAT_2: 7, XBOOLE_1: 28;

      hence the Source of C = (the Source of A | the carrier' of C) by A2, FUNCT_1: 46;

      

       A4: ( dom the Target of A) = the carrier' of A by FUNCT_2:def 1;

      ( dom the Target of C) = the carrier' of C by FUNCT_2:def 1;

      then ( dom the Target of C) = (( dom the Target of A) /\ the carrier' of C) by A4, CAT_2: 7, XBOOLE_1: 28;

      hence the Target of C = (the Target of A | the carrier' of C) by A3, FUNCT_1: 46;

      

       A5: ( dom the Comp of C) = (( dom the Comp of A) /\ [:the carrier' of C, the carrier' of C:])

      proof

        the Comp of C c= the Comp of A by CAT_2:def 4;

        then

         A6: ( dom the Comp of C) c= ( dom the Comp of A) by RELAT_1: 11;

        ( dom the Comp of C) c= [:the carrier' of C, the carrier' of C:] by RELAT_1:def 18;

        hence ( dom the Comp of C) c= (( dom the Comp of A) /\ [:the carrier' of C, the carrier' of C:]) by A6, XBOOLE_1: 19;

        let x be object;

        assume

         A7: x in (( dom the Comp of A) /\ [:the carrier' of C, the carrier' of C:]);

        then x in [:the carrier' of C, the carrier' of C:] by XBOOLE_0:def 4;

        then

        reconsider f = (x `1 ), g = (x `2 ) as Morphism of C by MCART_1: 10;

        reconsider f9 = f, g9 = g as Morphism of A by CAT_2: 8;

        x in ( dom the Comp of A) by A7, XBOOLE_0:def 4;

        then

         A8: [f9, g9] in ( dom the Comp of A) by MCART_1: 21;

        ( dom f) = ( dom f9) by CAT_2: 9

        .= ( cod g9) by A8, CAT_1: 15

        .= ( cod g) by CAT_2: 9;

        then [f, g] in ( dom the Comp of C) by CAT_1: 15;

        hence thesis by A7, MCART_1: 21;

      end;

      the Comp of C c= the Comp of A by CAT_2:def 4;

      

      hence the Comp of C = (the Comp of A | (( dom the Comp of A) /\ [:the carrier' of C, the carrier' of C:]) qua set) by A5, GRFUNC_1: 23

      .= ((the Comp of A qua Relation | ( dom the Comp of A) qua set) | [:the carrier' of C, the carrier' of C:] qua set) by RELAT_1: 71

      .= (the Comp of A || the carrier' of C);

    end;

    theorem :: NATTRA_1:9

    

     Th5: for O be non empty Subset of the carrier of A, M be non empty Subset of the carrier' of A st for o be Element of A st o in O holds ( id o) in M holds for DOM,COD be Function of M, O st DOM = (the Source of A | M) & COD = (the Target of A | M) holds for COMP be PartFunc of [:M, M qua non empty set:], M st COMP = (the Comp of A || M) holds CatStr (# O, M, DOM, COD, COMP #) is Subcategory of A

    proof

      let O be non empty Subset of the carrier of A, M be non empty Subset of the carrier' of A such that

       A1: for o be Element of A st o in O holds ( id o) in M;

      let DOM,COD be Function of M, O such that

       A2: DOM = (the Source of A | M) and

       A3: COD = (the Target of A | M);

      let COMP be PartFunc of [:M, M qua non empty set:], M such that

       A4: COMP = (the Comp of A || M);

      set C = CatStr (# O, M, DOM, COD, COMP #);

       A5:

      now

        let f be Morphism of A, g be Morphism of C such that

         A6: f = g;

        ( dom the Source of C) = the carrier' of C by FUNCT_2:def 1;

        hence ( dom f) = ( dom g) by A2, A6, FUNCT_1: 47;

        ( dom the Target of C) = the carrier' of C by FUNCT_2:def 1;

        hence ( cod f) = ( cod g) by A3, A6, FUNCT_1: 47;

      end;

      

       A7: ( dom the Comp of C) = (( dom the Comp of A) /\ [:the carrier' of C, the carrier' of C:]) by A4, RELAT_1: 61;

       A8:

      now

        let f,g be Morphism of C;

        reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def 3;

        assume ( dom g) = ( cod f);

        

        then ( dom g9) = ( cod f) by A5

        .= ( cod f9) by A5;

        then

         A9: [g9, f9] in ( dom the Comp of A) by CAT_1:def 6;

         [g, f] in [:the carrier' of C, the carrier' of C:] by ZFMISC_1: 87;

        hence [g, f] in ( dom the Comp of C) by A7, A9, XBOOLE_0:def 4;

      end;

      

       A10: ( dom the Comp of C) c= ( dom the Comp of A) by A4, RELAT_1: 60;

      

       A11: C is Category-like

      proof

        let f,g be Morphism of C;

        reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def 3;

        thus [g, f] in ( dom the Comp of C) implies ( dom g) = ( cod f)

        proof

          assume

           A12: [g, f] in ( dom the Comp of C);

          

          thus ( dom g) = ( dom g9) by A5

          .= ( cod f9) by A10, A12, CAT_1:def 6

          .= ( cod f) by A5;

        end;

        thus thesis by A8;

      end;

      

       A13: C is transitive

      proof

        let f,g be Morphism of C;

        reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def 3;

        assume

         A14: ( dom g) = ( cod f);

         [g, f] in ( dom the Comp of C) by A14, A11;

        then

         A15: (the Comp of C . (g,f)) = (g (*) f) by CAT_1:def 1;

        

         A16: ( dom g9) = ( cod f) by A5, A14

        .= ( cod f9) by A5;

        then [g9, f9] in ( dom the Comp of A) by CAT_1:def 6;

        then

         A17: (the Comp of A . (g9,f9)) = (g9 (*) f9) by CAT_1:def 1;

        

         A18: (the Comp of C . (g,f)) = (the Comp of A . (g9,f9)) by A4, A8, A14, FUNCT_1: 47;

        

        thus ( dom (g (*) f)) = ( dom (g9 (*) f9)) by A5, A18, A15, A17

        .= ( dom f9) by A16, CAT_1:def 7

        .= ( dom f) by A5;

        

        thus ( cod (g (*) f)) = ( cod (g9 (*) f9)) by A5, A18, A15, A17

        .= ( cod g9) by A16, CAT_1:def 7

        .= ( cod g) by A5;

      end;

      

       A19: for f,g be Morphism of C st ( cod g) = ( dom f) holds for ff,gg be Morphism of A st ff = f & gg = g holds (f (*) g) = (ff (*) gg)

      proof

        let f,g be Morphism of C such that

         A20: ( cod g) = ( dom f);

        let ff,gg be Morphism of A such that

         A21: ff = f & gg = g;

        

         A22: ( cod gg) = ( dom f) by A20, A5, A21

        .= ( dom ff) by A5, A21;

         [f, g] in ( dom the Comp of C) by A20, A11;

        

        hence (f (*) g) = (the Comp of C . (f,g)) by CAT_1:def 1

        .= (the Comp of A . (ff,gg)) by A21, A4, A8, A20, FUNCT_1: 47

        .= (ff (*) gg) by A22, CAT_1: 16;

      end;

      

       A23: C is associative

      proof

        let f,g,h be Morphism of C;

        reconsider g9 = g, f9 = f, h9 = h as Morphism of A by TARSKI:def 3;

        assume that

         A24: ( dom h) = ( cod g) and

         A25: ( dom g) = ( cod f);

        reconsider gf = (the Comp of C . (g,f)), hg = (the Comp of C . [h, g]) as Morphism of C by A8, A24, A25, PARTFUN1: 4;

        

         A26: ( dom h9) = ( cod g) by A5, A24

        .= ( cod g9) by A5;

        then

         A27: [h9, g9] in ( dom the Comp of A) by CAT_1:def 6;

        

         A28: ( dom g9) = ( cod f) by A5, A25

        .= ( cod f9) by A5;

        then

         A29: [g9, f9] in ( dom the Comp of A) by CAT_1:def 6;

        reconsider gf9 = (g9 (*) f9), hg9 = (h9 (*) g9) as Morphism of A;

        (the Comp of C . (h,g)) = (the Comp of A . (h9,g9)) by A4, A8, A24, FUNCT_1: 47;

        then

         A30: hg = (h9 (*) g9) by A27, CAT_1:def 1;

        

        then

         A31: ( dom hg) = ( dom hg9) by A5

        .= ( dom g9) by A26, CAT_1:def 7

        .= ( cod f) by A5, A25;

        (the Comp of C . (g,f)) = (the Comp of A . (g9,f9)) by A4, A8, A25, FUNCT_1: 47;

        then

         A32: gf = gf9 by A29, CAT_1:def 1;

        

         A33: ( dom h) = ( cod g9) by A5, A24

        .= ( cod gf9) by A28, CAT_1:def 7

        .= ( cod gf) by A5, A32;

        

         A34: (h (*) g) = (h9 (*) g9) by A19, A24;

        (g (*) f) = (g9 (*) f9) by A19, A25;

        

        hence (h (*) (g (*) f)) = (h9 (*) (g9 (*) f9)) by A19, A33, A32

        .= ((h9 (*) g9) (*) f9) by A26, A28, CAT_1:def 8

        .= ((h (*) g) (*) f) by A19, A34, A30, A31;

      end;

      

       A35: C is reflexive

      proof

        let b be Object of C;

        reconsider b9 = b as Object of A by TARSKI:def 3;

        reconsider ii = ( id b9) as Morphism of C by A1;

        

         A36: ( cod ii) = ( cod ( id b9)) by A5

        .= b;

        ( dom ii) = ( dom ( id b9)) by A5

        .= b;

        then ii in ( Hom (b,b)) by A36;

        hence ( Hom (b,b)) <> {} ;

      end;

      

       A37: for a be Object of C, aa be Element of A st a = aa holds for m be Morphism of C st m = ( id aa) holds for b be Object of C holds (( Hom (a,b)) <> {} implies for f be Morphism of a, b holds (f (*) m) = f) & (( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (m (*) f) = f)

      proof

        let a be Object of C, aa be Element of A such that

         A38: a = aa;

        let m be Morphism of C such that

         A39: m = ( id aa);

        let b be Object of C;

        reconsider bb = b as Object of A by TARSKI:def 3;

        thus ( Hom (a,b)) <> {} implies for f be Morphism of a, b holds (f (*) m) = f

        proof

          assume

           A40: ( Hom (a,b)) <> {} ;

          let f be Morphism of a, b;

          reconsider ff = f as Morphism of A by TARSKI:def 3;

          ( dom f) = a by A40, CAT_1: 5;

          then

           A41: ( dom ff) = aa by A38, A5;

          ( dom f) = ( cod ( id aa)) by A38, A40, CAT_1: 5

          .= ( cod m) by A39, A5;

          

          hence (f (*) m) = (ff (*) ( id aa)) by A19, A39

          .= f by A41, CAT_1: 22;

        end;

        thus ( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (m (*) f) = f

        proof

          assume

           A42: ( Hom (b,a)) <> {} ;

          let f be Morphism of b, a;

          reconsider ff = f as Morphism of A by TARSKI:def 3;

          ( cod f) = a by A42, CAT_1: 5;

          then

           A43: ( cod ff) = aa by A38, A5;

          ( dom f) = b by A42, CAT_1: 5;

          then ( dom ff) = bb by A5;

          then

           A44: ff in ( Hom (bb,aa)) by A43;

          then

          reconsider ff as Morphism of bb, aa by CAT_1:def 5;

          

           A45: ( Hom (aa,aa)) <> {} ;

          ( cod f) = ( dom ( id aa)) by A38, A42, CAT_1: 5

          .= ( dom m) by A39, A5;

          

          hence (m (*) f) = (( id aa) (*) ff) by A19, A39

          .= (( id aa) * ff) by A44, A45, CAT_1:def 13

          .= f by A44, CAT_1: 28;

        end;

      end;

      C is with_identities

      proof

        let a be Element of C;

        reconsider aa = a as Element of A by TARSKI:def 3;

        reconsider m = ( id aa) as Morphism of C by A1;

        

         A46: ( cod m) = ( cod ( id aa)) by A5

        .= a;

        ( dom m) = ( dom ( id aa)) by A5

        .= a;

        then m in ( Hom (a,a)) by A46;

        then

        reconsider m as Morphism of a, a by CAT_1:def 5;

        take m;

        thus thesis by A37;

      end;

      then

      reconsider C as Category by A11, A13, A23, A35;

      C is Subcategory of A

      proof

        thus the carrier of C c= the carrier of A;

        thus for a,b be Object of C, a9,b9 be Object of A st a = a9 & b = b9 holds ( Hom (a,b)) c= ( Hom (a9,b9))

        proof

          let a,b be Object of C, a9,b9 be Object of A such that

           A47: a = a9 and

           A48: b = b9;

          let x be object;

          assume x in ( Hom (a,b));

          then

          consider f be Morphism of C such that

           A49: x = f and

           A50: ( dom f) = a and

           A51: ( cod f) = b;

          reconsider f9 = f as Morphism of A by TARSKI:def 3;

          

           A52: ( cod f9) = b9 by A5, A48, A51;

          ( dom f9) = a9 by A5, A47, A50;

          hence thesis by A49, A52;

        end;

        thus the Comp of C c= the Comp of A by A4, RELAT_1: 59;

        let a be Object of C, a9 be Object of A;

        assume

         A53: a = a9;

        reconsider m = ( id a9) as Morphism of C by A1, A53;

        

         A54: ( cod m) = ( cod ( id a9)) by A5

        .= a by A53;

        ( dom m) = ( dom ( id a9)) by A5

        .= a by A53;

        then m in ( Hom (a,a)) by A54;

        then

        reconsider m as Morphism of a, a by CAT_1:def 5;

        for b be Object of C holds (( Hom (a,b)) <> {} implies for f be Morphism of a, b holds (f (*) m) = f) & (( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (m (*) f) = f) by A53, A37;

        hence ( id a) = ( id a9) by CAT_1:def 12;

      end;

      hence thesis;

    end;

    theorem :: NATTRA_1:10

    

     Th6: for C be strict Category, A be strict Subcategory of C st the carrier of A = the carrier of C & the carrier' of A = the carrier' of C holds A = C

    proof

      let C be strict Category, A be strict Subcategory of C such that

       A1: the carrier of A = the carrier of C and

       A2: the carrier' of A = the carrier' of C;

      

       A3: the Target of A = (the Target of C | the carrier' of A) by Th4

      .= the Target of C by A2;

      

       A4: the Comp of A = (the Comp of C || the carrier' of A) by Th4

      .= the Comp of C by A2;

      the Source of A = (the Source of C | the carrier' of A) by Th4

      .= the Source of C by A2;

      hence thesis by A1, A3, A4;

    end;

    begin

    definition

      ::$Canceled

    end

    theorem :: NATTRA_1:11

    for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((G * F) /. f) = (G /. (F /. f))

    proof

      let a,b be Object of A;

      assume

       A1: ( Hom (a,b)) <> {} ;

      then

       A2: ( Hom ((F . a),(F . b))) <> {} by CAT_1: 84;

      let f be Morphism of a, b;

      

      thus ((G * F) /. f) = ((G * F) . f qua Morphism of A) by A1, CAT_3:def 10

      .= (G . (F . f qua Morphism of A)) by FUNCT_2: 15

      .= (G . (F /. f) qua Morphism of B) by A1, CAT_3:def 10

      .= (G /. (F /. f)) by A2, CAT_3:def 10;

    end;

    theorem :: NATTRA_1:12

    for F1,F2 be Functor of A, B st for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds (F1 . f) = (F2 . f) holds F1 = F2

    proof

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

       A1: for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds (F1 . f) = (F2 . f);

      now

        let f be Morphism of A;

        reconsider f9 = f as Morphism of ( dom f), ( cod f) by CAT_1: 4;

        set a = ( dom f), b = ( cod f);

        ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

        

        hence (F1 . f) = (F2 . f9) by A1

        .= (F2 . f);

      end;

      hence thesis;

    end;

    theorem :: NATTRA_1:13

    

     Th9: for a,b,c be Object of A st ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} holds for f be Morphism of a, b, g be Morphism of b, c holds (F /. (g * f)) = ((F /. g) * (F /. f))

    proof

      let a,b,c be Object of A;

      assume that

       A1: ( Hom (a,b)) <> {} and

       A2: ( Hom (b,c)) <> {} ;

      let f be Morphism of a, b, g be Morphism of b, c;

      

       A3: ( dom g) = b by A2, CAT_1: 5;

      

       A4: ( cod f) = b by A1, CAT_1: 5;

      

       A5: (F /. g) = (F . g qua Morphism of A) by A2, CAT_3:def 10;

      

       A6: ( Hom ((F . a),(F . b))) <> {} by A1, CAT_1: 84;

      

       A7: (F /. f) = (F . f qua Morphism of A) by A1, CAT_3:def 10;

      

       A8: ( Hom ((F . b),(F . c))) <> {} by A2, CAT_1: 84;

      ( Hom (a,c)) <> {} by A1, A2, CAT_1: 24;

      

      hence (F /. (g * f)) = (F . (g * f) qua Morphism of A) by CAT_3:def 10

      .= (F . (g qua Morphism of A (*) f qua Morphism of A)) by A1, A2, CAT_1:def 13

      .= ((F . g qua Morphism of A) (*) (F . f qua Morphism of A)) by A3, A4, CAT_1: 64

      .= ((F /. g) * (F /. f)) by A6, A8, A5, A7, CAT_1:def 13;

    end;

    theorem :: NATTRA_1:14

    for c be Object of A, d be Object of B st (F /. ( id c)) = ( id d) holds (F . c) = d

    proof

      let c be Object of A, d be Object of B;

      

       A1: ( Hom (c,c)) <> {} ;

      assume (F /. ( id c)) = ( id d);

      then (F . ( id c) qua Morphism of A) = ( id d) by A1, CAT_3:def 10;

      hence thesis by CAT_1: 70;

    end;

    theorem :: NATTRA_1:15

    

     Th11: for a be Object of A holds (F /. ( id a)) = ( id (F . a))

    proof

      let a be Object of A;

      ( Hom (a,a)) <> {} ;

      

      hence (F /. ( id a)) = (F . ( id a) qua Morphism of A) by CAT_3:def 10

      .= ( id (F . a)) by CAT_1: 71;

    end;

    theorem :: NATTRA_1:16

    for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds (( id A) /. f) = f

    proof

      let a,b be Object of A such that

       A1: ( Hom (a,b)) <> {} ;

      let f be Morphism of a, b;

      

      thus (( id A) /. f) = (( id A) . f qua Morphism of A) by A1, CAT_3:def 10

      .= f by FUNCT_1: 18;

    end;

    theorem :: NATTRA_1:17

    for a,b,c,d be Object of A st ( Hom (a,b)) meets ( Hom (c,d)) holds a = c & b = d

    proof

      let a,b,c,d be Object of A;

      assume ( Hom (a,b)) meets ( Hom (c,d));

      then

      consider x be object such that

       A1: x in ( Hom (a,b)) and

       A2: x in ( Hom (c,d)) by XBOOLE_0: 3;

      reconsider x as Morphism of A by A1;

      

       A3: ( cod x) = b by A1, CAT_1: 1;

      ( dom x) = a by A1, CAT_1: 1;

      hence thesis by A2, A3, CAT_1: 1;

    end;

    begin

    definition

      let A, B, F1, F2;

      :: NATTRA_1:def2

      pred F1 is_transformable_to F2 means

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

      reflexivity ;

    end

    theorem :: NATTRA_1:18

    

     Th14: F is_transformable_to F1 & F1 is_transformable_to F2 implies F is_transformable_to F2

    proof

      assume that

       A1: F is_transformable_to F1 and

       A2: F1 is_transformable_to F2;

      let a be Object of A;

      

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

      ( Hom ((F . a),(F1 . a))) <> {} by A1;

      hence thesis by A3, CAT_1: 24;

    end;

    definition

      let A, B, F1, F2;

      assume

       A1: F1 is_transformable_to F2;

      :: NATTRA_1:def3

      mode transformation of F1,F2 -> Function of the carrier of A, the carrier' of B means

      : Def2: for a be Object of A holds (it . a) is Morphism of (F1 . a), (F2 . a);

      existence

      proof

        deffunc F( Object of A) = ( Hom ((F1 . $1),(F2 . $1)));

        

         A2: for a be Object of A holds the carrier' of B meets F(a)

        proof

          let a be Object of A;

          set x = the Element of ( Hom ((F1 . a),(F2 . a)));

          

           A3: ( Hom ((F1 . a),(F2 . a))) <> {} by A1;

          now

            take x;

            thus x in the carrier' of B & x in ( Hom ((F1 . a),(F2 . a))) by A3, TARSKI:def 3;

          end;

          hence thesis by XBOOLE_0: 3;

        end;

        consider t be Function of the carrier of A, the carrier' of B such that

         A4: for a be Object of A holds (t . a) in F(a) from FUNCT_2:sch 10( A2);

        take t;

        let a be Object of A;

        (t . a) in ( Hom ((F1 . a),(F2 . a))) by A4;

        hence thesis by CAT_1:def 5;

      end;

    end

    definition

      let A, B;

      let F be Functor of A, B;

      :: NATTRA_1:def4

      func id F -> transformation of F, F means

      : Def3: for a be Object of A holds (it . a) = ( id (F . a));

      existence

      proof

        deffunc F( Object of A) = ( id (F . $1));

        consider t be Function of the carrier of A, the carrier' of B such that

         A1: for a be Object of A holds (t . a) = F(a) from FUNCT_2:sch 4;

        for a be Object of A holds (t . a) is Morphism of (F . a), (F . a)

        proof

          let a be Object of A;

          (t . a) = ( id (F . a)) by A1;

          hence thesis;

        end;

        then

        reconsider t as transformation of F, F by Def2;

        take t;

        let a be Object of A;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be transformation of F, F such that

         A2: for a be Object of A holds (it1 . a) = ( id (F . a)) and

         A3: for a be Object of A holds (it2 . a) = ( id (F . a));

        now

          let a be Object of A;

          

          thus (it1 . a) = ( id (F . a)) by A2

          .= (it2 . a) by A3;

        end;

        hence it1 = it2;

      end;

    end

    definition

      let A, B, F1, F2;

      assume

       A1: F1 is_transformable_to F2;

      let t be transformation of F1, F2;

      let a be Object of A;

      :: NATTRA_1:def5

      func t . a -> Morphism of (F1 . a), (F2 . a) equals

      : Def4: (t . a);

      coherence by A1, Def2;

    end

    definition

      let A, B, F, F1, F2;

      assume that

       A1: F is_transformable_to F1 and

       A2: F1 is_transformable_to F2;

      let t1 be transformation of F, F1;

      let t2 be transformation of F1, F2;

      :: NATTRA_1:def6

      func t2 `*` t1 -> transformation of F, F2 means

      : Def5: for a be Object of A holds (it . a) = ((t2 . a) * (t1 . a));

      existence

      proof

        deffunc F( Object of A) = ((t2 . $1) * (t1 . $1));

        consider t be Function of the carrier of A, the carrier' of B such that

         A3: for a be Object of A holds (t . a) = F(a) from FUNCT_2:sch 4;

        

         A4: for a be Object of A holds (t . a) is Morphism of (F . a), (F2 . a)

        proof

          let a be Object of A;

          (t . a) = ((t2 . a) * (t1 . a)) by A3;

          hence thesis;

        end;

        F is_transformable_to F2 by A1, A2, Th14;

        then

        reconsider t9 = t as transformation of F, F2 by A4, Def2;

        take t9;

        let a be Object of A;

        

        thus (t9 . a) = (t . a) by A1, A2, Def4, Th14

        .= ((t2 . a) * (t1 . a)) by A3;

      end;

      uniqueness

      proof

        let it1,it2 be transformation of F, F2 such that

         A5: for a be Object of A holds (it1 . a) = ((t2 . a) * (t1 . a)) and

         A6: for a be Object of A holds (it2 . a) = ((t2 . a) * (t1 . a));

        now

          let a be Object of A;

          

          thus (it1 qua Function of the carrier of A, the carrier' of B . a) = (it1 . a) by A1, A2, Def4, Th14

          .= ((t2 . a) * (t1 . a)) by A5

          .= (it2 . a) by A6

          .= (it2 qua Function of the carrier of A, the carrier' of B . a) by A1, A2, Def4, Th14;

        end;

        hence it1 = it2;

      end;

    end

    theorem :: NATTRA_1:19

    

     Th15: F1 is_transformable_to F2 implies for t1,t2 be transformation of F1, F2 st for a be Object of A holds (t1 . a) = (t2 . a) holds t1 = t2

    proof

      assume

       A1: F1 is_transformable_to F2;

      let t1,t2 be transformation of F1, F2;

      assume

       A2: for a be Object of A holds (t1 . a) = (t2 . a);

      now

        let a be Object of A;

        

        thus (t1 qua Function of the carrier of A, the carrier' of B . a) = (t1 . a) by A1, Def4

        .= (t2 . a) by A2

        .= (t2 qua Function of the carrier of A, the carrier' of B . a) by A1, Def4;

      end;

      hence thesis;

    end;

    theorem :: NATTRA_1:20

    

     Th16: for a be Object of A holds (( id F) . a) = ( id (F . a))

    proof

      let a be Object of A;

      

      thus (( id F) . a) = (( id F) qua Function of the carrier of A, the carrier' of B . a) by Def4

      .= ( id (F . a)) by Def3;

    end;

    theorem :: NATTRA_1:21

    

     Th17: F1 is_transformable_to F2 implies for t be transformation of F1, F2 holds (( id F2) `*` t) = t & (t `*` ( id F1)) = t

    proof

      assume

       A1: F1 is_transformable_to F2;

      let t be transformation of F1, F2;

      now

        let a be Object of A;

        

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

        

        thus ((( id F2) `*` t) . a) = ((( id F2) . a) * (t . a)) by A1, Def5

        .= (( id (F2 . a)) * (t . a)) by Th16

        .= (t . a) by A2, CAT_1: 28;

      end;

      hence (( id F2) `*` t) = t by A1, Th15;

      now

        let a be Object of A;

        

         A3: ( Hom ((F1 . a),(F2 . a))) <> {} by A1;

        

        thus ((t `*` ( id F1)) . a) = ((t . a) * (( id F1) . a)) by A1, Def5

        .= ((t . a) * ( id (F1 . a))) by Th16

        .= (t . a) by A3, CAT_1: 29;

      end;

      hence thesis by A1, Th15;

    end;

    theorem :: NATTRA_1:22

    

     Th18: F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 implies for t1 be transformation of F, F1, t2 be transformation of F1, F2, t3 be transformation of F2, F3 holds ((t3 `*` t2) `*` t1) = (t3 `*` (t2 `*` t1))

    proof

      assume that

       A1: F is_transformable_to F1 and

       A2: F1 is_transformable_to F2 and

       A3: F2 is_transformable_to F3;

      let t1 be transformation of F, F1, t2 be transformation of F1, F2, t3 be transformation of F2, F3;

      

       A4: F1 is_transformable_to F3 by A2, A3, Th14;

      

       A5: F is_transformable_to F2 by A1, A2, Th14;

      now

        let a be Object of A;

        

         A6: ( Hom ((F . a),(F1 . a))) <> {} by A1;

        

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

        

         A8: ( Hom ((F2 . a),(F3 . a))) <> {} by A3;

        

        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 A6, A7, A8, CAT_1: 25

        .= ((t3 . a) * ((t2 `*` t1) . a)) by A1, A2, Def5

        .= ((t3 `*` (t2 `*` t1)) . a) by A3, A5, Def5;

      end;

      hence thesis by A1, A4, Th14, Th15;

    end;

    begin

    

     Lm1: for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((( id F) . b) * (F /. f)) = ((F /. f) * (( id F) . a))

    proof

      let a,b be Object of A such that

       A1: ( Hom (a,b)) <> {} ;

      let f be Morphism of a, b;

      

       A2: ( Hom (a,a)) <> {} ;

      

       A3: ( Hom (b,b)) <> {} ;

      

      thus ((( id F) . b) * (F /. f)) = (( id (F . b)) * (F /. f)) by Th16

      .= ((F /. ( id b)) * (F /. f)) by Th11

      .= (F /. (( id b) * f)) by A1, A3, Th9

      .= (F /. f) by A1, CAT_1: 28

      .= (F /. (f * ( id a))) by A1, CAT_1: 29

      .= ((F /. f) * (F /. ( id a))) by A1, A2, Th9

      .= ((F /. f) * ( id (F . a))) by Th11

      .= ((F /. f) * (( id F) . a)) by Th16;

    end;

    definition

      let A, B, F1, F2;

      :: NATTRA_1:def7

      pred F1 is_naturally_transformable_to F2 means F1 is_transformable_to F2 & ex t be transformation of F1, F2 st for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((t . b) * (F1 /. f)) = ((F2 /. f) * (t . a));

      reflexivity

      proof

        let F;

        ex t be transformation of F, F st for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((t . b) * (F /. f)) = ((F /. f) * (t . a))

        proof

          take ( id F);

          thus thesis by Lm1;

        end;

        hence thesis;

      end;

    end

    

     Lm2: F is_transformable_to F1 & F1 is_transformable_to F2 implies for t1 be transformation of F, F1 st for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((t1 . b) * (F /. f)) = ((F1 /. f) * (t1 . a)) holds for t2 be transformation of F1, F2 st for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((t2 . b) * (F1 /. f)) = ((F2 /. f) * (t2 . a)) holds for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds (((t2 `*` t1) . b) * (F /. f)) = ((F2 /. f) * ((t2 `*` t1) . a))

    proof

      assume that

       A1: F is_transformable_to F1 and

       A2: F1 is_transformable_to F2;

      let t1 be transformation of F, F1 such that

       A3: for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((t1 . b) * (F /. f)) = ((F1 /. f) * (t1 . a));

      let t2 be transformation of F1, F2 such that

       A4: for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((t2 . b) * (F1 /. f)) = ((F2 /. f) * (t2 . a));

      let a,b be Object of A;

      

       A5: ( Hom ((F . b),(F1 . b))) <> {} by A1;

      

       A6: ( Hom ((F . a),(F1 . a))) <> {} by A1;

      

       A7: ( Hom ((F1 . b),(F2 . b))) <> {} by A2;

      

       A8: ( Hom ((F1 . a),(F2 . a))) <> {} by A2;

      assume

       A9: ( Hom (a,b)) <> {} ;

      then

       A10: ( Hom ((F . a),(F . b))) <> {} by CAT_1: 84;

      let f be Morphism of a, b;

      

       A11: ( Hom ((F2 . a),(F2 . b))) <> {} by A9, CAT_1: 84;

      

       A12: ( Hom ((F1 . a),(F1 . b))) <> {} by A9, CAT_1: 84;

      

      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, CAT_1: 25

      .= ((t2 . b) * ((F1 /. f) * (t1 . a))) by A3, A9

      .= (((t2 . b) * (F1 /. f)) * (t1 . a)) by A6, A7, A12, CAT_1: 25

      .= (((F2 /. f) * (t2 . a)) * (t1 . a)) by A4, A9

      .= ((F2 /. f) * ((t2 . a) * (t1 . a))) by A6, A8, A11, CAT_1: 25

      .= ((F2 /. f) * ((t2 `*` t1) . a)) by A1, A2, Def5;

    end;

    theorem :: NATTRA_1:23

    

     Th19: F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies F is_naturally_transformable_to F2

    proof

      assume

       A1: F is_transformable_to F1;

      given t1 be transformation of F, F1 such that

       A2: for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((t1 . b) * (F /. f)) = ((F1 /. f) * (t1 . a));

      assume

       A3: F1 is_transformable_to F2;

      given t2 be transformation of F1, F2 such that

       A4: for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((t2 . b) * (F1 /. f)) = ((F2 /. f) * (t2 . a));

      thus F is_transformable_to F2 by A1, A3, Th14;

      take (t2 `*` t1);

      thus thesis by A1, A2, A3, A4, Lm2;

    end;

    definition

      let A, B, F1, F2;

      assume

       A1: F1 is_naturally_transformable_to F2;

      :: NATTRA_1:def8

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

      : Def7: for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((it . b) * (F1 /. f)) = ((F2 /. f) * (it . a));

      existence by A1;

    end

    definition

      let A, B, F;

      :: original: id

      redefine

      func id F -> natural_transformation of F, F ;

      coherence

      proof

        thus F is_naturally_transformable_to F;

        thus thesis by Lm1;

      end;

    end

    definition

      let A, B, F, F1, F2;

      let t1 be natural_transformation of F, F1;

      let t2 be natural_transformation of F1, F2;

      :: NATTRA_1:def9

      func t2 `*` t1 -> natural_transformation of F, F2 equals

      : Def8: (t2 `*` t1);

      coherence

      proof

        

         A3: F is_naturally_transformable_to F2 by A1, A2, Th19;

        

         A4: F1 is_transformable_to F2 by A2;

        

         A5: for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((t2 . b) * (F1 /. f)) = ((F2 /. f) * (t2 . a)) by A2, Def7;

        

         A6: for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((t1 . b) * (F /. f)) = ((F1 /. f) * (t1 . a)) by A1, Def7;

        F is_transformable_to F1 by A1;

        then for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds (((t2 `*` t1) . b) * (F /. f)) = ((F2 /. f) * ((t2 `*` t1) . a)) by A4, A6, A5, Lm2;

        hence thesis by A3, Def7;

      end;

    end

    theorem :: NATTRA_1:24

    

     Th20: F1 is_naturally_transformable_to F2 implies for t be natural_transformation of F1, F2 holds (( id F2) `*` t) = t & (t `*` ( id F1)) = t

    proof

      assume

       A1: F1 is_naturally_transformable_to F2;

      then

       A2: F1 is_transformable_to F2;

      let t be natural_transformation of F1, F2;

      

      thus (( id F2) `*` t) = (( id F2) `*` t qua transformation of F1, F2) by A1, Def8

      .= t by A2, Th17;

      

      thus (t `*` ( id F1)) = (t qua transformation of F1, F2 `*` ( id F1)) by A1, Def8

      .= t by A2, Th17;

    end;

    reserve t for natural_transformation of F, F1,

t1 for natural_transformation of F1, F2;

    theorem :: NATTRA_1:25

    

     Th21: F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies for t1 be natural_transformation of F, F1 holds for t2 be natural_transformation of F1, F2 holds for a be Object of A holds ((t2 `*` t1) . a) = ((t2 . a) * (t1 . a))

    proof

      assume that

       A1: F is_naturally_transformable_to F1 and

       A2: F1 is_naturally_transformable_to F2;

      

       A3: F1 is_transformable_to F2 by A2;

      let t1 be natural_transformation of F, F1;

      let t2 be natural_transformation of F1, F2;

      let a be Object of A;

      reconsider t19 = t1 as transformation of F, F1;

      reconsider t29 = t2 as transformation of F1, F2;

      

       A4: F is_transformable_to F1 by A1;

      

      thus ((t2 `*` t1) . a) = ((t29 `*` t19) . a) by A1, A2, Def8

      .= ((t2 . a) * (t1 . a)) by A4, A3, Def5;

    end;

    theorem :: NATTRA_1:26

    

     Th22: F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t3 be natural_transformation of F2, F3 holds ((t3 `*` t1) `*` t) = (t3 `*` (t1 `*` t))

    proof

      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;

      

       A4: F is_naturally_transformable_to F2 by A1, A2, Th19;

      

       A5: F2 is_transformable_to F3 by A3;

      

       A6: F1 is_transformable_to F2 by A2;

      let t3 be natural_transformation of F2, F3;

      

       A7: F is_transformable_to F1 by A1;

      F1 is_naturally_transformable_to F3 by A2, A3, Th19;

      

      hence ((t3 `*` t1) `*` t) = ((t3 `*` t1) `*` t qua transformation of F, F1) by A1, Def8

      .= ((t3 qua transformation of F2, F3 `*` t1) `*` t) by A2, A3, Def8

      .= (t3 `*` (t1 `*` t qua transformation of F, F1)) by A7, A6, A5, Th18

      .= (t3 qua transformation of F2, F3 `*` (t1 `*` t)) by A1, A2, Def8

      .= (t3 `*` (t1 `*` t)) by A3, A4, Def8;

    end;

    definition

      let A, B, F1, F2;

      let IT be transformation of F1, F2;

      :: NATTRA_1:def10

      attr IT is invertible means for a be Object of A holds (IT . a) is invertible;

    end

    definition

      let A, B, F1, F2;

      :: NATTRA_1:def11

      pred F1,F2 are_naturally_equivalent means F1 is_naturally_transformable_to F2 & ex t be natural_transformation of F1, F2 st t is invertible;

      reflexivity

      proof

        let F;

        thus F is_naturally_transformable_to F;

        take ( id F);

        let a be Object of A;

        (( id F) . a) = ( id (F . a)) by Th16;

        hence thesis by CAT_1: 44;

      end;

    end

    notation

      let A, B, F1, F2;

      synonym F1 ~= F2 for F1,F2 are_naturally_equivalent ;

    end

    

     Lm3: for t be transformation of F1, F2 st F1 is_transformable_to F2 & t is invertible holds F2 is_transformable_to F1

    proof

      let t be transformation of F1, F2 such that F1 is_transformable_to F2 and

       A1: for a be Object of A holds (t . a) is invertible;

      let a be Object of A;

      

       A2: (t . a) is invertible by A1;

      thus thesis by A2;

    end;

    definition

      let A, B, F1, F2;

      let t1 be transformation of F1, F2;

      :: NATTRA_1:def12

      func t1 " -> transformation of F2, F1 means

      : Def11: for a be Object of A holds (it . a) = ((t1 . a) " );

      existence

      proof

        deffunc F( Object of A) = ((t1 . $1) " );

        consider t be Function of the carrier of A, the carrier' of B such that

         A3: for a be Object of A holds (t . a) = F(a) from FUNCT_2:sch 4;

         A4:

        now

          let a be Object of A;

          (t . a) = ((t1 . a) " ) by A3;

          hence (t . a) is Morphism of (F2 . a), (F1 . a);

        end;

        F2 is_transformable_to F1 by A1, A2, Lm3;

        then

        reconsider t as transformation of F2, F1 by A4, Def2;

        take t;

        let a be Object of A;

        

        thus (t . a) = (t qua Function of the carrier of A, the carrier' of B . a) by A1, A2, Def4, Lm3

        .= ((t1 . a) " ) by A3;

      end;

      uniqueness

      proof

        let t,t9 be transformation of F2, F1 such that

         A5: for a be Object of A holds (t . a) = ((t1 . a) " ) and

         A6: for a be Object of A holds (t9 . a) = ((t1 . a) " );

        now

          let a be Object of A;

          

          thus (t . a) = ((t1 . a) " ) by A5

          .= (t9 . a) by A6;

        end;

        hence thesis by A1, A2, Lm3, Th15;

      end;

    end

     Lm4:

    now

      let A, B, F1, F2, t1 such that

       A1: F1 is_naturally_transformable_to F2 and

       A2: t1 is invertible;

      let a,b be Object of A such that

       A3: ( Hom (a,b)) <> {} ;

      

       A4: ( Hom ((F1 . a),(F1 . b))) <> {} by A3, CAT_1: 84;

      let f be Morphism of a, b;

      

       A5: ( Hom ((F2 . a),(F2 . b))) <> {} by A3, CAT_1: 84;

      

       A6: F1 is_transformable_to F2 by A1;

      

       A7: ( Hom ((F1 . b),(F2 . b))) <> {} by Def1, A1;

      

       A8: (t1 . b) is invertible by A2;

      then

       A9: ( Hom ((F2 . b),(F1 . b))) <> {} ;

      

       A10: ( Hom ((F1 . a),(F2 . a))) <> {} by A1, Def1;

      ((F2 /. f) * (t1 . a)) = ((t1 . b) * (F1 /. f)) by A1, A3, Def7;

      

      then

       A11: ((((t1 . b) " ) * (F2 /. f)) * (t1 . a)) = (((t1 . b) " ) * ((t1 . b) * (F1 /. f))) by A10, A9, A5, CAT_1: 25

      .= ((((t1 . b) " ) * (t1 . b)) * (F1 /. f)) by A4, A7, A9, CAT_1: 25

      .= (( id (F1 . b)) * (F1 /. f)) by A8, CAT_1:def 17

      .= (F1 /. f) by A4, CAT_1: 28;

      

       A12: (t1 . a) is invertible by A2;

      then

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

      then

       A14: ( Hom ((F2 . a),(F1 . b))) <> {} by A4, CAT_1: 24;

      

      then (((t1 . b) " ) * (F2 /. f)) = ((((t1 . b) " ) * (F2 /. f)) * ( id (F2 . a))) by CAT_1: 29

      .= ((((t1 . b) " ) * (F2 /. f)) * ((t1 . a) * ((t1 . a) " ))) by A12, CAT_1:def 17

      .= ((F1 /. f) * ((t1 . a) " )) by A10, A13, A14, A11, CAT_1: 25;

      

      hence (((t1 " ) . b) * (F2 /. f)) = ((F1 /. f) * ((t1 . a) " )) by A2, A6, Def11

      .= ((F1 /. f) * ((t1 " ) . a)) by A2, A6, Def11;

    end;

    

     Lm5: F1 is_naturally_transformable_to F2 & t1 is invertible implies F2 is_naturally_transformable_to F1

    proof

      assume

       A1: F1 is_naturally_transformable_to F2;

      assume

       A2: t1 is invertible;

      hence F2 is_transformable_to F1 by A1, Lm3;

      take (t1 " );

      thus thesis by A1, A2, Lm4;

    end;

    definition

      let A, B, F1, F2, t1;

      :: NATTRA_1:def13

      func t1 " -> natural_transformation of F2, F1 equals

      : Def12: (t1 qua transformation of F1, F2 " );

      coherence

      proof

        

         A3: for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds (((t1 " ) . b) * (F2 /. f)) = ((F1 /. f) * ((t1 " ) . a)) by A1, A2, Lm4;

        F2 is_naturally_transformable_to F1 by A1, A2, Lm5;

        hence thesis by A3, Def7;

      end;

    end

    theorem :: NATTRA_1:27

    

     Th23: for A, B, F1, F2, t1 st F1 is_naturally_transformable_to F2 & t1 is invertible holds for a be Object of A holds ((t1 " ) . a) = ((t1 . a) " )

    proof

      let A, B, F1, F2, t1 such that

       A1: F1 is_naturally_transformable_to F2 and

       A2: t1 is invertible;

      let a be Object of A;

      

       A3: F1 is_transformable_to F2 by A1;

      

      thus ((t1 " ) . a) = ((t1 qua transformation of F1, F2 " ) . a) by A1, A2, Def12

      .= ((t1 qua transformation of F1, F2 . a) " ) by A2, A3, Def11;

    end;

    theorem :: NATTRA_1:28

    F1 ~= F2 implies F2 ~= F1

    proof

      assume

       A1: F1 is_naturally_transformable_to F2;

      given t be natural_transformation of F1, F2 such that

       A2: t is invertible;

      thus F2 is_naturally_transformable_to F1 by A1, A2, Lm5;

      take (t " );

      let a be Object of A;

      ((t " ) . a) = ((t . a) " ) by A1, A2, Th23;

      hence thesis by A2, CAT_1: 46;

    end;

    theorem :: NATTRA_1:29

    

     Th25: F1 ~= F2 & F2 ~= F3 implies F1 ~= F3

    proof

      assume

       A1: F1 is_naturally_transformable_to F2;

      given t be natural_transformation of F1, F2 such that

       A2: t is invertible;

      assume

       A3: F2 is_naturally_transformable_to F3;

      given t9 be natural_transformation of F2, F3 such that

       A4: t9 is invertible;

      thus F1 is_naturally_transformable_to F3 by A1, A3, Th19;

      take (t9 `*` t);

      let a be Object of A;

      

       A5: (t9 . a) is invertible by A4;

      

       A6: (t . a) is invertible by A2;

      ((t9 `*` t) . a) = ((t9 . a) * (t . a)) by A1, A3, Th21;

      hence thesis by A5, A6, CAT_1: 45;

    end;

    definition

      let A, B, F1, F2;

      assume

       A1: (F1,F2) are_naturally_equivalent ;

      :: NATTRA_1:def14

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

      : Def13: it is invertible;

      existence by A1;

    end

    theorem :: NATTRA_1:30

    ( id F) is natural_equivalence of F, F

    proof

      thus F ~= F;

      let a be Object of A;

      (( id F) . a) = ( id (F . a)) by Th16;

      hence thesis by CAT_1: 44;

    end;

    theorem :: NATTRA_1:31

    F1 ~= F2 & F2 ~= F3 implies for t be natural_equivalence of F1, F2, t9 be natural_equivalence of F2, F3 holds (t9 `*` t) is natural_equivalence of F1, F3

    proof

      assume that

       A1: (F1,F2) are_naturally_equivalent and

       A2: (F2,F3) are_naturally_equivalent ;

      let t be natural_equivalence of F1, F2, t9 be natural_equivalence of F2, F3;

      thus (F1,F3) are_naturally_equivalent by A1, A2, Th25;

      let a be Object of A;

      t9 is invertible by A2, Def13;

      then

       A3: (t9 . a) is invertible;

      t is invertible by A1, Def13;

      then

       A4: (t . a) is invertible;

      

       A5: F1 is_naturally_transformable_to F2 by A1;

      

       A6: F2 is_naturally_transformable_to F3 by A2;

      ((t9 `*` t) . a) = ((t9 . a) * (t . a)) by A5, A6, Th21;

      hence thesis by A3, A4, CAT_1: 45;

    end;

    begin

    definition

      let A, B;

      :: NATTRA_1:def15

      mode NatTrans-DOMAIN of A,B -> non empty set means

      : Def14: for x be set holds x in it implies ex F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 st x = [ [F1, F2], t] & F1 is_naturally_transformable_to F2;

      existence

      proof

        set F = the Functor of A, B;

        take { [ [F, F], ( id F)]};

        let x be set such that

         A1: x in { [ [F, F], ( id F)]};

        take F, F, ( id F);

        thus thesis by A1, TARSKI:def 1;

      end;

    end

    definition

      let A, B;

      :: NATTRA_1:def16

      func NatTrans (A,B) -> NatTrans-DOMAIN of A, B means

      : Def15: for x be set holds x in it iff ex F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 st x = [ [F1, F2], t] & F1 is_naturally_transformable_to F2;

      existence

      proof

        set F = the Functor of A, B;

        defpred P[ object] means ex F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 st $1 = [ [F1, F2], t] & F1 is_naturally_transformable_to F2;

        consider T be set such that

         A1: for x be object holds x in T iff x in [: [:( Funct (A,B)), ( Funct (A,B)):], ( Funcs (the carrier of A,the carrier' of B)):] & P[x] from XBOOLE_0:sch 1;

        F in ( Funct (A,B)) by CAT_2:def 2;

        then

         A2: [F, F] in [:( Funct (A,B)), ( Funct (A,B)):] by ZFMISC_1: 87;

        ( id F) in ( Funcs (the carrier of A,the carrier' of B)) by FUNCT_2: 8;

        then [ [F, F], ( id F)] in [: [:( Funct (A,B)), ( Funct (A,B)):], ( Funcs (the carrier of A,the carrier' of B)):] by A2, ZFMISC_1: 87;

        then

        reconsider T as non empty set by A1;

        for x be set st x in T holds ex F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 st x = [ [F1, F2], t] & F1 is_naturally_transformable_to F2 by A1;

        then

        reconsider T as NatTrans-DOMAIN of A, B by Def14;

        take T;

        let x be set;

        thus x in T implies ex F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 st x = [ [F1, F2], t] & F1 is_naturally_transformable_to F2 by A1;

        given F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 such that

         A3: x = [ [F1, F2], t] and

         A4: F1 is_naturally_transformable_to F2;

        

         A5: F2 in ( Funct (A,B)) by CAT_2:def 2;

        

         A6: t in ( Funcs (the carrier of A,the carrier' of B)) by FUNCT_2: 8;

        F1 in ( Funct (A,B)) by CAT_2:def 2;

        then [F1, F2] in [:( Funct (A,B)), ( Funct (A,B)):] by A5, ZFMISC_1: 87;

        then x in [: [:( Funct (A,B)), ( Funct (A,B)):], ( Funcs (the carrier of A,the carrier' of B)):] by A3, A6, ZFMISC_1: 87;

        hence thesis by A1, A3, A4;

      end;

      uniqueness

      proof

        let S,T be NatTrans-DOMAIN of A, B such that

         A7: for x be set holds x in S iff ex F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 st x = [ [F1, F2], t] & F1 is_naturally_transformable_to F2 and

         A8: for x be set holds x in T iff ex F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 st x = [ [F1, F2], t] & F1 is_naturally_transformable_to F2;

        now

          let x be object;

          x in S iff ex F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 st x = [ [F1, F2], t] & F1 is_naturally_transformable_to F2 by A7;

          hence x in S iff x in T by A8;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: NATTRA_1:32

    

     Th28: F1 is_naturally_transformable_to F2 iff [ [F1, F2], t1] in ( NatTrans (A,B))

    proof

      thus F1 is_naturally_transformable_to F2 implies [ [F1, F2], t1] in ( NatTrans (A,B)) by Def15;

      assume [ [F1, F2], t1] in ( NatTrans (A,B));

      then

      consider F19,F29 be Functor of A, B, t be natural_transformation of F19, F29 such that

       A1: [ [F1, F2], t1] = [ [F19, F29], t] and

       A2: F19 is_naturally_transformable_to F29 by Def15;

      

       A3: [F1, F2] = [F19, F29] by A1, XTUPLE_0: 1;

      then F1 = F19 by XTUPLE_0: 1;

      hence thesis by A2, A3, XTUPLE_0: 1;

    end;

    definition

      let A, B;

      :: NATTRA_1:def17

      func Functors (A,B) -> strict Category means

      : Def16: the carrier of it = ( Funct (A,B)) & the carrier' of it = ( NatTrans (A,B)) & (for f be Morphism of it holds ( dom f) = ((f `1 ) `1 ) & ( cod f) = ((f `1 ) `2 )) & (for f,g be Morphism of it st ( dom g) = ( cod f) holds [g, f] in ( dom the Comp of it )) & (for f,g be Morphism of it st [g, f] in ( dom the Comp of it ) holds ex F, F1, F2, t, t1 st f = [ [F, F1], t] & g = [ [F1, F2], t1] & (the Comp of it . [g, f]) = [ [F, F2], (t1 `*` t)]) & for a be Object of it , F st F = a holds ( id a) = [ [F, F], ( id F)];

      existence

      proof

        defpred P[ object, object, object] means ex F, F1, F2, t, t1 st $2 = [ [F, F1], t] & $1 = [ [F1, F2], t1] & $3 = [ [F, F2], (t1 `*` t)];

        deffunc F( object) = (($1 `1 ) `1 );

         A1:

        now

          let x,y,z1,z2 be object;

          assume that x in ( NatTrans (A,B)) and y in ( NatTrans (A,B));

          assume P[x, y, z1];

          then

          consider F, F1, F2, t, t1 such that

           A2: y = [ [F, F1], t] and

           A3: x = [ [F1, F2], t1] and

           A4: z1 = [ [F, F2], (t1 `*` t)];

          assume P[x, y, z2];

          then

          consider F9,F19,F29 be Functor of A, B, t9 be natural_transformation of F9, F19, t19 be natural_transformation of F19, F29 such that

           A5: y = [ [F9, F19], t9] and

           A6: x = [ [F19, F29], t19] and

           A7: z2 = [ [F9, F29], (t19 `*` t9)];

          

           A8: t = t9 by A2, A5, XTUPLE_0: 1;

           [F1, F2] = [F19, F29] by A3, A6, XTUPLE_0: 1;

          then

           A9: F2 = F29 by XTUPLE_0: 1;

          

           A10: t1 = t19 by A3, A6, XTUPLE_0: 1;

          

           A11: [F, F1] = [F9, F19] by A2, A5, XTUPLE_0: 1;

          then F = F9 by XTUPLE_0: 1;

          hence z1 = z2 by A4, A7, A11, A8, A10, A9, XTUPLE_0: 1;

        end;

         A12:

        now

          let x,y,z be object;

          assume that

           A13: x in ( NatTrans (A,B)) and

           A14: y in ( NatTrans (A,B));

          assume P[x, y, z];

          then

          consider F, F1, F2, t, t1 such that

           A15: y = [ [F, F1], t] and

           A16: x = [ [F1, F2], t1] and

           A17: z = [ [F, F2], (t1 `*` t)];

          

           A18: F1 is_naturally_transformable_to F2 by A13, A16, Th28;

          F is_naturally_transformable_to F1 by A14, A15, Th28;

          hence z in ( NatTrans (A,B)) by A17, Th28, A18, Th19;

        end;

        consider m be PartFunc of [:( NatTrans (A,B)), ( NatTrans (A,B)):], ( NatTrans (A,B)) such that

         A19: for x,y be object holds [x, y] in ( dom m) iff x in ( NatTrans (A,B)) & y in ( NatTrans (A,B)) & ex z be object st P[x, y, z] and

         A20: for x,y be object st [x, y] in ( dom m) holds P[x, y, (m . (x,y))] from BINOP_1:sch 5( A12, A1);

         A21:

        now

          let t be Element of ( NatTrans (A,B));

          consider F1,F2 be Functor of A, B, s be natural_transformation of F1, F2 such that

           A22: t = [ [F1, F2], s] and F1 is_naturally_transformable_to F2 by Def15;

          ((t `1 ) `1 ) = ( [F1, F2] `1 ) by A22

          .= F1;

          hence F(t) in ( Funct (A,B)) by CAT_2:def 2;

        end;

        consider d be Function of ( NatTrans (A,B)), ( Funct (A,B)) such that

         A23: for t be Element of ( NatTrans (A,B)) holds (d . t) = F(t) from FUNCT_2:sch 8( A21);

        deffunc F( set) = (($1 `1 ) `2 );

         A24:

        now

          let t be Element of ( NatTrans (A,B));

          consider F1,F2 be Functor of A, B, s be natural_transformation of F1, F2 such that

           A25: t = [ [F1, F2], s] and F1 is_naturally_transformable_to F2 by Def15;

          ((t `1 ) `2 ) = ( [F1, F2] `2 ) by A25

          .= F2;

          hence F(t) in ( Funct (A,B)) by CAT_2:def 2;

        end;

        consider c be Function of ( NatTrans (A,B)), ( Funct (A,B)) such that

         A26: for t be Element of ( NatTrans (A,B)) holds (c . t) = F(t) from FUNCT_2:sch 8( A24);

        deffunc F( Element of ( Funct (A,B))) = [ [$1, $1], ( id $1)];

        

         A27: for F be Element of ( Funct (A,B)) holds F(F) in ( NatTrans (A,B)) by Def15;

        consider i be Function of ( Funct (A,B)), ( NatTrans (A,B)) such that

         A28: for F be Element of ( Funct (A,B)) holds (i . F) = F(F) from FUNCT_2:sch 8( A27);

        set C = CatStr (# ( Funct (A,B)), ( NatTrans (A,B)), d, c, m #);

         A29:

        now

          let F, F1, F2, t, t1;

          assume that

           A30: F1 is_naturally_transformable_to F2 and

           A31: F is_naturally_transformable_to F1;

          

           A32: [ [F, F1], t] in ( NatTrans (A,B)) by A31, Th28;

          

           A33: P[ [ [F1, F2], t1], [ [F, F1], t], [ [F, F2], (t1 `*` t)]];

           [ [F1, F2], t1] in ( NatTrans (A,B)) by A30, Th28;

          then

          consider F9,F19,F29 be Functor of A, B, t9 be natural_transformation of F9, F19, t19 be natural_transformation of F19, F29 such that

           A34: [ [F, F1], t] = [ [F9, F19], t9] and

           A35: [ [F1, F2], t1] = [ [F19, F29], t19] and

           A36: (m . ( [ [F1, F2], t1], [ [F, F1], t])) = [ [F9, F29], (t19 `*` t9)] by A20, A19, A32, A33;

          

           A37: t = t9 by A34, XTUPLE_0: 1;

           [F1, F2] = [F19, F29] by A35, XTUPLE_0: 1;

          then

           A38: F2 = F29 by XTUPLE_0: 1;

          

           A39: t1 = t19 by A35, XTUPLE_0: 1;

          

           A40: [F, F1] = [F9, F19] by A34, XTUPLE_0: 1;

          then F = F9 by XTUPLE_0: 1;

          hence (m . [ [ [F1, F2], t1], [ [F, F1], t]]) = [ [F, F2], (t1 `*` t)] by A36, A40, A37, A39, A38, XTUPLE_0: 1;

        end;

        

         A41: C is Category-like

        proof

          let f,g be Element of the carrier' of C;

          consider F19,F29 be Functor of A, B, t9 be natural_transformation of F19, F29 such that

           A42: f = [ [F19, F29], t9] and

           A43: F19 is_naturally_transformable_to F29 by Def15;

          thus [g, f] in ( dom the Comp of C) implies ( dom g) = ( cod f)

          proof

            assume [g, f] in ( dom the Comp of C);

            then

            consider F, F1, F2, t, t1 such that

             A44: f = [ [F, F1], t] and

             A45: g = [ [F1, F2], t1] and (m . (g,f)) = [ [F, F2], (t1 `*` t)] by A20;

            

            thus ( dom g) = ((g `1 ) `1 ) by A23

            .= ( [F1, F2] `1 ) by A45

            .= ( [F, F1] `2 )

            .= ((f `1 ) `2 ) by A44

            .= ( cod f) by A26;

          end;

          assume

           A46: ( dom g) = ( cod f);

          consider F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 such that

           A47: g = [ [F1, F2], t] and

           A48: F1 is_naturally_transformable_to F2 by Def15;

          

           A49: F1 = ( [F1, F2] `1 )

          .= ((g `1 ) `1 ) by A47

          .= (c . f) by A23, A46

          .= ((f `1 ) `2 ) by A26

          .= ( [F19, F29] `2 ) by A42

          .= F29;

          then

          reconsider t as natural_transformation of F29, F2;

          (m . [g, f]) = [ [F19, F2], (t `*` t9)] by A29, A47, A48, A42, A43, A49;

          hence thesis by A19, A47, A42, A49;

        end;

        

         A50: C is transitive

        proof

          let f,g be Element of the carrier' of C;

          consider F19,F29 be Functor of A, B, t9 be natural_transformation of F19, F29 such that

           A51: f = [ [F19, F29], t9] and

           A52: F19 is_naturally_transformable_to F29 by Def15;

          assume ( dom g) = ( cod f);

          then

           A53: [g, f] in ( dom m) by A41;

          then

          consider F, F1, F2, t, t1 such that

           A54: f = [ [F, F1], t] and

           A55: g = [ [F1, F2], t1] and

           A56: (m . (g,f)) = [ [F, F2], (t1 `*` t)] by A20;

          

           A57: (m . (g,f)) = (g (*) f) by A53, CAT_1:def 1;

          

           A58: [F, F1] = [F19, F29] by A54, A51, XTUPLE_0: 1;

          then

           A59: F = F19 by XTUPLE_0: 1;

          

           A60: F1 = F29 by A58, XTUPLE_0: 1;

          consider F19,F29 be Functor of A, B, t9 be natural_transformation of F19, F29 such that

           A61: g = [ [F19, F29], t9] and

           A62: F19 is_naturally_transformable_to F29 by Def15;

          

           A63: [F1, F2] = [F19, F29] by A55, A61, XTUPLE_0: 1;

          then

           A64: F2 = F29 by XTUPLE_0: 1;

          F1 = F19 by A63, XTUPLE_0: 1;

          then

          reconsider x = [ [F, F2], (t1 `*` t)] as Element of ( NatTrans (A,B)) by Th28, A52, A59, A60, A62, A64, Th19;

          

          thus ( dom (g (*) f)) = ((x `1 ) `1 ) by A23, A56, A57

          .= ( [F, F2] `1 )

          .= (( [ [F, F1], t] `1 ) `1 )

          .= ( dom f) by A23, A54;

          

          thus ( cod (g (*) f)) = ((x `1 ) `2 ) by A26, A56, A57

          .= ( [F, F2] `2 )

          .= (( [ [F1, F2], t1] `1 ) `2 )

          .= ( cod g) by A26, A55;

        end;

        

         A65: C is associative

        proof

          

           A66: for f,g be Element of the carrier' of C holds [g, f] in ( dom the Comp of C) iff ( dom g) = ( cod f) by A41;

          let f,g,h be Element of the carrier' of C;

          reconsider f9 = f, g9 = g, h9 = h as Element of ( NatTrans (A,B));

          assume that

           A67: ( dom h) = ( cod g) and

           A68: ( dom g) = ( cod f);

           [g9, f9] in ( dom m) by A41, A68;

          then

          consider F1,F19,F2 be Functor of A, B, t1 be natural_transformation of F1, F19, t2 be natural_transformation of F19, F2 such that

           A69: f9 = [ [F1, F19], t1] and

           A70: g9 = [ [F19, F2], t2] and

           A71: (m . (g9,f9)) = [ [F1, F2], (t2 `*` t1)] by A20;

           [h9, g9] in ( dom m) by A41, A67;

          then

          consider F29,F3,F39 be Functor of A, B, t29 be natural_transformation of F29, F3, t3 be natural_transformation of F3, F39 such that

           A72: g9 = [ [F29, F3], t29] and

           A73: h9 = [ [F3, F39], t3] and (m . (h9,g9)) = [ [F29, F39], (t3 `*` t29)] by A20;

          

           A74: [F29, F3] = [F19, F2] by A70, A72, XTUPLE_0: 1;

          then

           A75: g9 = [ [F19, F3], t2] by A70, XTUPLE_0: 1;

          reconsider t2 as natural_transformation of F19, F3 by A74, XTUPLE_0: 1;

          

           A76: F2 = F3 by A74, XTUPLE_0: 1;

          then

           A77: F19 is_naturally_transformable_to F3 by A70, Th28;

          

           A78: F3 is_naturally_transformable_to F39 by A73, Th28;

          then

           A79: F19 is_naturally_transformable_to F39 by A77, Th19;

          

           A80: F1 is_naturally_transformable_to F19 by A69, Th28;

          then

           A81: F1 is_naturally_transformable_to F3 by A77, Th19;

          

           A82: (h (*) g) = (the Comp of C . (h,g)) by A66, A67, CAT_1:def 1;

          

           A83: ( dom (h (*) g)) = ( dom g) by A50, A67;

          

           A84: (g (*) f) = (the Comp of C . (g,f)) by A66, A68, CAT_1:def 1;

          ( cod (g (*) f)) = ( cod g) by A50, A68;

          

          hence (h (*) (g (*) f)) = (the Comp of C . (h,(the Comp of C . (g,f)))) by A84, A66, A67, CAT_1:def 1

          .= [ [F1, F39], (t3 `*` (t2 `*` t1))] by A29, A71, A73, A76, A78, A81

          .= [ [F1, F39], ((t3 `*` t2) `*` t1)] by A80, A77, A78, Th22

          .= (m . [ [ [F19, F39], (t3 `*` t2)], f9]) by A29, A69, A80, A79

          .= (the Comp of C . ((the Comp of C . (h,g)),f)) by A29, A73, A75, A77, A78

          .= ((h (*) g) (*) f) by A83, A82, A66, A68, CAT_1:def 1;

        end;

        

         A85: C is reflexive

        proof

          let b be Element of C;

          reconsider F = b as Functor of A, B by CAT_2:def 2;

          reconsider s = [ [F, F], ( id F)] as Element of ( NatTrans (A,B)) by Def15;

          reconsider s as Morphism of C;

          

           A86: ( dom s) = (( [ [F, F], ( id F)] `1 ) `1 ) by A23

          .= F;

          ( cod s) = (( [ [F, F], ( id F)] `1 ) `2 ) by A26

          .= F;

          then s in ( Hom (b,b)) by A86;

          hence ( Hom (b,b)) <> {} ;

        end;

        

         A87: for a be Object of C, F be Functor of A, B st a = F holds for m be Morphism of C st m = [ [F, F], ( id F)] holds for b be Object of C holds (( Hom (a,b)) <> {} implies for f be Morphism of a, b holds (f (*) m) = f) & (( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (m (*) f) = f)

        proof

          let a be Object of C, F be Functor of A, B such that

           A88: a = F;

          let ii be Morphism of C such that

           A89: ii = [ [F, F], ( id F)];

          let b be Object of C;

          reconsider s = [ [F, F], ( id F)] as Element of ( NatTrans (A,B)) by Def15;

          

           A90: F in ( Funct (A,B)) by CAT_2:def 2;

          then

           A91: (i . F) = [ [F, F], ( id F)] by A28;

          thus ( Hom (a,b)) <> {} implies for f be Morphism of a, b holds (f (*) ii) = f

          proof

            assume

             A92: ( Hom (a,b)) <> {} ;

            let f be Morphism of a, b;

            reconsider f9 = f as Element of ( NatTrans (A,B));

            

             A93: ( dom f) = a by A92, CAT_1: 5;

            consider F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 such that

             A94: f9 = [ [F1, F2], t] and F1 is_naturally_transformable_to F2 by Def15;

            

             A95: F1 = ( [F1, F2] `1 )

            .= ((f9 `1 ) `1 ) by A94

            .= ( dom f) by A23

            .= F by A92, A88, CAT_1: 5;

            then

            reconsider t as natural_transformation of F, F2;

             P[f9, s, [ [F, F2], (t `*` ( id F))]] by A94, A95;

            then

            consider F9,F19,F29 be Functor of A, B, t9 be natural_transformation of F9, F19, t19 be natural_transformation of F19, F29 such that

             A96: (i . F) = [ [F9, F19], t9] and

             A97: f9 = [ [F19, F29], t19] and

             A98: (m . (f9,(i . F))) = [ [F9, F29], (t19 `*` t9)] by A20, A91, A19;

            

             A99: [F9, F19] = [F, F] by A96, A91, XTUPLE_0: 1;

            then

             A100: F9 = F by XTUPLE_0: 1;

            

             A101: F19 = F by A99, XTUPLE_0: 1;

            

             A102: F19 is_naturally_transformable_to F29 by A97, Th28;

            

             A103: F29 = (( [ [F19, F29], t19] `1 ) `2 )

            .= (( [ [F1, F2], t] `1 ) `2 ) by A97, A94

            .= F2;

            

             A104: t19 = ( [ [F19, F29], t19] `2 )

            .= ( [ [F1, F2], t] `2 ) by A97, A94

            .= t;

            

             A105: (t19 `*` ( id F19)) = t19 by Th20, A102;

            ( cod ii) = (( [ [F, F], ( id F)] `1 ) `2 ) by A89, A26

            .= a by A88;

            then [f, ii] in ( dom the Comp of C) by A41, A93;

            

            hence (f (*) ii) = (m . (f,ii)) by CAT_1:def 1

            .= f by A104, A105, A95, A103, A96, A91, A100, A101, A98, A89, A94, XTUPLE_0: 1;

          end;

          assume

           A106: ( Hom (b,a)) <> {} ;

          let f be Morphism of b, a;

          reconsider f9 = f as Element of ( NatTrans (A,B));

          

           A107: ( cod f) = a by A106, CAT_1: 5;

          consider F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 such that

           A108: f9 = [ [F1, F2], t] and F1 is_naturally_transformable_to F2 by Def15;

          

           A109: F2 = ( [F1, F2] `2 )

          .= ((f9 `1 ) `2 ) by A108

          .= ( cod f) by A26

          .= F by A106, A88, CAT_1: 5;

          then

          reconsider t as natural_transformation of F1, F;

           P[s, f9, [ [F1, F], (( id F) `*` t)]] by A108, A109;

          then

          consider F9,F19,F29 be Functor of A, B, t9 be natural_transformation of F9, F19, t19 be natural_transformation of F19, F29 such that

           A110: f9 = [ [F9, F19], t9] and

           A111: (i . F) = [ [F19, F29], t19] and

           A112: (m . ((i . F),f9)) = [ [F9, F29], (t19 `*` t9)] by A20, A91, A19;

          

           A113: t19 = ( id F) by A111, A91, XTUPLE_0: 1;

          

           A114: [F19, F29] = [F, F] by A111, A91, XTUPLE_0: 1;

          then

           A115: F19 = F by XTUPLE_0: 1;

          

           A116: F9 is_naturally_transformable_to F19 by A110, Th28;

          

           A117: F9 = (( [ [F9, F19], t9] `1 ) `1 )

          .= (( [ [F1, F2], t] `1 ) `1 ) by A110, A108

          .= F1;

          

           A118: t9 = ( [ [F9, F19], t9] `2 )

          .= ( [ [F1, F2], t] `2 ) by A110, A108

          .= t;

          

           A119: (( id F19) `*` t9) = t9 by Th20, A116;

          ( dom ii) = (( [ [F, F], ( id F)] `1 ) `1 ) by A89, A23

          .= a by A88;

          then [ii, f] in ( dom the Comp of C) by A41, A107;

          

          hence (ii (*) f) = (m . (ii,f)) by CAT_1:def 1

          .= (m . ((i . F),f9)) by A89, A90, A28

          .= [ [F9, F29], (( id F19) `*` t9)] by A113, A115, A114, A112, XTUPLE_0: 1

          .= f by A108, A118, A119, A114, A109, A117, XTUPLE_0: 1;

        end;

        C is with_identities

        proof

          let a be Element of C;

          reconsider F = a as Functor of A, B by CAT_2:def 2;

          reconsider s = [ [F, F], ( id F)] as Element of ( NatTrans (A,B)) by Def15;

          reconsider s as Morphism of C;

          

           A120: ( dom s) = (( [ [F, F], ( id F)] `1 ) `1 ) by A23

          .= F;

          ( cod s) = (( [ [F, F], ( id F)] `1 ) `2 ) by A26

          .= F;

          then s in ( Hom (a,a)) by A120;

          then

          reconsider s as Morphism of a, a by CAT_1:def 5;

          take s;

          thus thesis by A87;

        end;

        then

        reconsider C as strict Category by A41, A50, A65, A85;

        take C;

        thus the carrier of C = ( Funct (A,B)) & the carrier' of C = ( NatTrans (A,B));

        thus for f be Morphism of C holds ( dom f) = ((f `1 ) `1 ) & ( cod f) = ((f `1 ) `2 ) by A23, A26;

        thus for f,g be Morphism of C st ( dom g) = ( cod f) holds [g, f] in ( dom the Comp of C)

        proof

          let f,g be Morphism of C;

          assume

           A121: ( dom g) = ( cod f);

          consider F19,F29 be Functor of A, B, t9 be natural_transformation of F19, F29 such that

           A122: g = [ [F19, F29], t9] and F19 is_naturally_transformable_to F29 by Def15;

          consider F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 such that

           A123: f = [ [F1, F2], t] and F1 is_naturally_transformable_to F2 by Def15;

          

           A124: F2 = (( [ [F1, F2], t] `1 ) `2 )

          .= ( cod f) by A26, A123

          .= (( [ [F19, F29], t9] `1 ) `1 ) by A23, A122, A121

          .= F19;

          then

          reconsider t9 as natural_transformation of F2, F29;

           P[g, f, [ [F1, F29], (t9 `*` t)]] by A123, A122, A124;

          hence thesis by A19;

        end;

        thus for f,g be Morphism of C st [g, f] in ( dom the Comp of C) holds ex F, F1, F2, t, t1 st f = [ [F, F1], t] & g = [ [F1, F2], t1] & (the Comp of C . [g, f]) = [ [F, F2], (t1 `*` t)]

        proof

          let f,g be Morphism of C;

          assume [g, f] in ( dom the Comp of C);

          then ex F, F1, F2, t, t1 st f = [ [F, F1], t] & g = [ [F1, F2], t1] & (the Comp of C . (g,f)) = [ [F, F2], (t1 `*` t)] by A20;

          hence thesis;

        end;

        let a be Object of C, F such that

         A125: a = F;

        reconsider m = [ [F, F], ( id F)] as Element of ( NatTrans (A,B)) by Def15;

        reconsider m as Morphism of C;

        

         A126: ( dom m) = (( [ [F, F], ( id F)] `1 ) `1 ) by A23

        .= F;

        ( cod m) = (( [ [F, F], ( id F)] `1 ) `2 ) by A26

        .= F;

        then m in ( Hom (a,a)) by A125, A126;

        then

        reconsider m as Morphism of a, a by CAT_1:def 5;

        for b be Object of C holds (( Hom (a,b)) <> {} implies for f be Morphism of a, b holds (f (*) m) = f) & (( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (m (*) f) = f) by A125, A87;

        hence ( id a) = [ [F, F], ( id F)] by CAT_1:def 12;

      end;

      uniqueness

      proof

        let C1,C2 be strict Category such that

         A127: the carrier of C1 = ( Funct (A,B)) and

         A128: the carrier' of C1 = ( NatTrans (A,B)) and

         A129: for f be Morphism of C1 holds ( dom f) = ((f `1 ) `1 ) & ( cod f) = ((f `1 ) `2 ) and

         A130: for f,g be Morphism of C1 st ( dom g) = ( cod f) holds [g, f] in ( dom the Comp of C1) and

         A131: for f,g be Morphism of C1 st [g, f] in ( dom the Comp of C1) holds ex F, F1, F2, t, t1 st f = [ [F, F1], t] & g = [ [F1, F2], t1] & (the Comp of C1 . [g, f]) = [ [F, F2], (t1 `*` t)] and for a be Object of C1, F st F = a holds ( id a) = [ [F, F], ( id F)] and

         A132: the carrier of C2 = ( Funct (A,B)) and

         A133: the carrier' of C2 = ( NatTrans (A,B)) and

         A134: for f be Morphism of C2 holds ( dom f) = ((f `1 ) `1 ) & ( cod f) = ((f `1 ) `2 ) and

         A135: for f,g be Morphism of C2 st ( dom g) = ( cod f) holds [g, f] in ( dom the Comp of C2) and

         A136: for f,g be Morphism of C2 st [g, f] in ( dom the Comp of C2) holds ex F, F1, F2, t, t1 st f = [ [F, F1], t] & g = [ [F1, F2], t1] & (the Comp of C2 . [g, f]) = [ [F, F2], (t1 `*` t)] and for a be Object of C2, F st F = a holds ( id a) = [ [F, F], ( id F)];

        

         A137: the Target of C1 = the Target of C2

        proof

          thus the carrier' of C1 = the carrier' of C2 by A128, A133;

          let a be Morphism of C1;

          reconsider b = a as Morphism of C2 by A128, A133;

          

          thus (the Target of C1 . a) = ( cod a)

          .= ((a `1 ) `2 ) by A129

          .= ( cod b) by A134

          .= (the Target of C2 . a);

        end;

         A138:

        now

          reconsider S1 = ( dom the Comp of C1), S2 = ( dom the Comp of C2) as Subset of [:the carrier' of C1, the carrier' of C1:] by A128, A133, RELAT_1:def 18;

           A139:

          now

            let x be Element of [:the carrier' of C1, the carrier' of C1:];

            

             A140: x = [(x `1 ), (x `2 )] by MCART_1: 21;

            then

            reconsider f1 = (x `2 ), g1 = (x `1 ) as Morphism of C1 by ZFMISC_1: 87;

            reconsider f2 = (x `2 ), g2 = (x `1 ) as Morphism of C2 by A128, A133, A140, ZFMISC_1: 87;

             A141:

            now

              assume [g2, f2] in S2;

              then

              consider F, F1, F2, t, t1 such that

               A142: f2 = [ [F, F1], t] and

               A143: g2 = [ [F1, F2], t1] and (the Comp of C2 . [g2, f2]) = [ [F, F2], (t1 `*` t)] by A136;

              ( dom g1) = ((g1 `1 ) `1 ) by A129

              .= ( [F1, F2] `1 ) by A143

              .= ( [F, F1] `2 )

              .= ((f2 `1 ) `2 ) by A142

              .= ( cod f1) by A129;

              hence [g1, f1] in S1 by A130;

            end;

            now

              assume [g1, f1] in S1;

              then

              consider F, F1, F2, t, t1 such that

               A144: f1 = [ [F, F1], t] and

               A145: g1 = [ [F1, F2], t1] and (the Comp of C1 . [g1, f1]) = [ [F, F2], (t1 `*` t)] by A131;

              ( dom g2) = ((g2 `1 ) `1 ) by A134

              .= ( [F1, F2] `1 ) by A145

              .= ( [F, F1] `2 )

              .= ((f1 `1 ) `2 ) by A144

              .= ( cod f2) by A134;

              hence [g2, f2] in S2 by A135;

            end;

            hence x in S1 iff x in S2 by A141, MCART_1: 21;

          end;

          hence ( dom the Comp of C1) = ( dom the Comp of C2) by SUBSET_1: 3;

          let x be object;

          assume

           A146: x in ( dom the Comp of C1);

          ( dom the Comp of C1) c= [:the carrier' of C1, the carrier' of C1:] by RELAT_1:def 18;

          then

          reconsider f = (x `2 ), g = (x `1 ) as Morphism of C1 by A146, MCART_1: 10;

          

           A147: [g, f] = x by A146, MCART_1: 21;

          then

          consider F9,F19,F29 be Functor of A, B, t9 be natural_transformation of F9, F19, t19 be natural_transformation of F19, F29 such that

           A148: f = [ [F9, F19], t9] and

           A149: g = [ [F19, F29], t19] and

           A150: (the Comp of C2 . [g, f]) = [ [F9, F29], (t19 `*` t9)] by A128, A133, A136, A139, A146;

          consider F, F1, F2, t, t1 such that

           A151: f = [ [F, F1], t] and

           A152: g = [ [F1, F2], t1] and

           A153: (the Comp of C1 . [g, f]) = [ [F, F2], (t1 `*` t)] by A131, A146, A147;

          

           A154: [F, F1] = [F9, F19] by A151, A148, XTUPLE_0: 1;

          then

           A155: F = F9 by XTUPLE_0: 1;

           [F1, F2] = [F19, F29] by A152, A149, XTUPLE_0: 1;

          then

           A156: F2 = F29 by XTUPLE_0: 1;

          

           A157: F1 = F19 by A154, XTUPLE_0: 1;

          t = t9 by A151, A148, XTUPLE_0: 1;

          hence (the Comp of C1 . x) = (the Comp of C2 . x) by A147, A152, A153, A149, A150, A155, A157, A156, XTUPLE_0: 1;

        end;

        the Source of C1 = the Source of C2

        proof

          thus the carrier' of C1 = the carrier' of C2 by A128, A133;

          let a be Morphism of C1;

          reconsider b = a as Morphism of C2 by A128, A133;

          

          thus (the Source of C1 . a) = ( dom a)

          .= ((a `1 ) `1 ) by A129

          .= ( dom b) by A134

          .= (the Source of C2 . a);

        end;

        hence thesis by A127, A132, A137, A138, FUNCT_1: 2;

      end;

    end

    theorem :: NATTRA_1:33

    

     Th29: for f be Morphism of ( Functors (A,B)) st f = [ [F, F1], t] holds ( dom f) = F & ( cod f) = F1

    proof

      let f be Morphism of ( Functors (A,B)) such that

       A1: f = [ [F, F1], t];

      

      thus ( dom f) = ((f `1 ) `1 ) by Def16

      .= ( [F, F1] `1 ) by A1

      .= F;

      

      thus ( cod f) = ((f `1 ) `2 ) by Def16

      .= ( [F, F1] `2 ) by A1

      .= F1;

    end;

    theorem :: NATTRA_1:34

    for a,b be Object of ( Functors (A,B)), f be Morphism of a, b st ( Hom (a,b)) <> {} holds ex F, F1, t st a = F & b = F1 & f = [ [F, F1], t]

    proof

      let a,b be Object of ( Functors (A,B)), f be Morphism of a, b such that

       A1: ( Hom (a,b)) <> {} ;

      the carrier' of ( Functors (A,B)) = ( NatTrans (A,B)) by Def16;

      then

      consider F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 such that

       A2: f = [ [F1, F2], t] and F1 is_naturally_transformable_to F2 by Def14;

      take F1, F2, t;

      

      thus a = ( dom f) by A1, CAT_1: 5

      .= F1 by A2, Th29;

      

      thus b = ( cod f) by A1, CAT_1: 5

      .= F2 by A2, Th29;

      thus thesis by A2;

    end;

    theorem :: NATTRA_1:35

    

     Th31: for t9 be natural_transformation of F2, F3 holds for f,g be Morphism of ( Functors (A,B)) st f = [ [F, F1], t] & g = [ [F2, F3], t9] holds [g, f] in ( dom the Comp of ( Functors (A,B))) iff F1 = F2

    proof

      let t9 be natural_transformation of F2, F3;

      let f,g be Morphism of ( Functors (A,B));

      assume that

       A1: f = [ [F, F1], t] and

       A2: g = [ [F2, F3], t9];

      thus [g, f] in ( dom the Comp of ( Functors (A,B))) implies F1 = F2

      proof

        assume [g, f] in ( dom the Comp of ( Functors (A,B)));

        then

        consider F9,F19,F29 be Functor of A, B, t9 be natural_transformation of F9, F19, t19 be natural_transformation of F19, F29 such that

         A3: f = [ [F9, F19], t9] and

         A4: g = [ [F19, F29], t19] and (the Comp of ( Functors (A,B)) . [g, f]) = [ [F9, F29], (t19 `*` t9)] by Def16;

        

        thus F1 = (( [ [F, F1], t] `1 ) `2 )

        .= (( [ [F9, F19], t9] `1 ) `2 ) by A1, A3

        .= ( [F9, F19] `2 )

        .= (( [ [F19, F29], t19] `1 ) `1 )

        .= ( [F2, F3] `1 ) by A2, A4

        .= F2;

      end;

      

       A5: ( cod f) = F1 by A1, Th29;

      ( dom g) = F2 by A2, Th29;

      hence thesis by A5, Def16;

    end;

    theorem :: NATTRA_1:36

    for f,g be Morphism of ( Functors (A,B)) st f = [ [F, F1], t] & g = [ [F1, F2], t1] holds (g (*) f) = [ [F, F2], (t1 `*` t)]

    proof

      let f,g be Morphism of ( Functors (A,B));

      assume that

       A1: f = [ [F, F1], t] and

       A2: g = [ [F1, F2], t1];

      

       A3: [g, f] in ( dom the Comp of ( Functors (A,B))) by A1, A2, Th31;

      then

      consider F9,F19,F29 be Functor of A, B, t9 be natural_transformation of F9, F19, t19 be natural_transformation of F19, F29 such that

       A4: f = [ [F9, F19], t9] and

       A5: g = [ [F19, F29], t19] and

       A6: (the Comp of ( Functors (A,B)) . (g,f)) = [ [F9, F29], (t19 `*` t9)] by Def16;

      

       A7: t1 = t19 by A2, A5, XTUPLE_0: 1;

      

       A8: [F9, F19] = [F, F1] by A1, A4, XTUPLE_0: 1;

      then

       A9: F = F9 by XTUPLE_0: 1;

       [F19, F29] = [F1, F2] by A2, A5, XTUPLE_0: 1;

      then

       A10: F2 = F29 by XTUPLE_0: 1;

      

       A11: F1 = F19 by A8, XTUPLE_0: 1;

      t = t9 by A1, A4, XTUPLE_0: 1;

      hence thesis by A3, A6, A7, A9, A11, A10, CAT_1:def 1;

    end;

    begin

    definition

      let C be Category;

      :: NATTRA_1:def18

      attr C is quasi-discrete means

      : Def17: for a,b be Element of C st ( Hom (a,b)) <> {} holds a = b;

      :: NATTRA_1:def19

      attr C is pseudo-discrete means

      : Def18: for a be Element of C holds ( Hom (a,a)) is trivial;

    end

    reserve a,b for Element of C;

    

     Lm6: C is quasi-discrete implies the carrier' of C = ( union the set of all ( Hom (a,a)))

    proof

      assume

       A1: C is quasi-discrete;

      set A = the set of all ( Hom (a,b)), N = ( union A), B = the set of all ( Hom (a,a)), M = ( union B);

      

       A2: the carrier' of C = N by CAT_1: 92;

      thus the carrier' of C c= M

      proof

        let e be object;

        assume e in the carrier' of C;

        then

        consider X be set such that

         A3: e in X and

         A4: X in A by A2, TARSKI:def 4;

        consider a, b such that

         A5: X = ( Hom (a,b)) by A4;

        a = b by A1, A3, A5;

        then X in B by A5;

        hence e in M by A3, TARSKI:def 4;

      end;

      let e be object;

      assume e in M;

      then

      consider X be set such that

       A6: e in X and

       A7: X in B by TARSKI:def 4;

      ex a st X = ( Hom (a,a)) by A7;

      hence e in the carrier' of C by A6;

    end;

    

     Lm7: C is pseudo-discrete implies ( Hom (a,a)) = {( id a)}

    proof

      assume C is pseudo-discrete;

      then ( Hom (a,a)) is trivial non empty;

      then

      consider m be object such that

       A1: ( Hom (a,a)) = {m} by ZFMISC_1: 131;

      ( id a) in ( Hom (a,a)) by CAT_1: 27;

      hence ( Hom (a,a)) = {( id a)} by A1, TARSKI:def 1;

    end;

    definition

      let C be Category;

      :: NATTRA_1:def20

      attr C is discrete means C is quasi-discrete pseudo-discrete;

    end

    registration

      cluster discrete -> quasi-discrete pseudo-discrete for Category;

      coherence ;

      cluster quasi-discrete pseudo-discrete -> discrete for Category;

      coherence ;

    end

    

     Lm8: C is discrete implies the carrier' of C c= the set of all ( id a)

    proof

      assume

       A1: C is discrete;

      let e be object;

      assume e in the carrier' of C;

      then e in ( union the set of all ( Hom (a,a))) by A1, Lm6;

      then

      consider X be set such that

       A2: e in X and

       A3: X in the set of all ( Hom (a,a)) by TARSKI:def 4;

      consider a such that

       A4: X = ( Hom (a,a)) by A3;

      X = {( id a)} by A4, A1, Lm7;

      then e = ( id a) by A2, TARSKI:def 1;

      hence e in the set of all ( id b);

    end;

    registration

      let o,m be set;

      cluster ( 1Cat (o,m)) -> discrete;

      coherence

      proof

        thus ( 1Cat (o,m)) is quasi-discrete by ZFMISC_1:def 10;

        let a be Object of ( 1Cat (o,m));

        thus ( Hom (a,a)) is trivial;

      end;

    end

    registration

      cluster discrete for Category;

      existence

      proof

        take ( 1Cat ( {} , {} ));

        thus thesis;

      end;

    end

    registration

      let C be discrete Category;

      let a be Element of C;

      cluster ( Hom (a,a)) -> trivial;

      coherence by Def18;

    end

    theorem :: NATTRA_1:37

    

     Th33: for A be discrete Category, a be Object of A holds ( Hom (a,a)) = {( id a)}

    proof

      let A be discrete Category, a be Object of A;

      now

        let g be Morphism of a, a;

        ( id a) in ( Hom (a,a)) & g in ( Hom (a,a)) by CAT_1:def 5;

        hence g = ( id a) by ZFMISC_1:def 10;

      end;

      hence thesis by CAT_1: 8;

    end;

    registration

      let A be discrete Category;

      cluster -> discrete for Subcategory of A;

      coherence

      proof

        let C be Subcategory of A;

        

         A1: the carrier of C c= the carrier of A by CAT_2:def 4;

        thus C is quasi-discrete

        proof

          let a,b be Element of C;

          reconsider aa = a, bb = b as Element of A by A1;

          assume

           A2: ( Hom (a,b)) <> {} ;

          ( Hom (a,b)) c= ( Hom (aa,bb)) by CAT_2:def 4;

          then ( Hom (aa,bb)) <> {} by A2;

          hence thesis by Def17;

        end;

        let a be Element of C;

        reconsider aa = a as Element of A by A1;

        ( Hom (a,a)) c= ( Hom (aa,aa)) by CAT_2:def 4;

        hence thesis;

      end;

    end

    registration

      let A,B be discrete Category;

      cluster [:A, B:] -> discrete;

      coherence

      proof

        thus [:A, B:] is quasi-discrete

        proof

          let a,b be Element of [:A, B:] such that

           A1: ( Hom (a,b)) <> {} ;

          consider a1 be Element of A, b1 be Element of B such that

           A2: a = [a1, b1] by DOMAIN_1: 1;

          consider a2 be Element of A, b2 be Element of B such that

           A3: b = [a2, b2] by DOMAIN_1: 1;

          ( Hom (a,b)) = [:( Hom (a1,a2)), ( Hom (b1,b2)):] by A2, A3, CAT_2: 32;

          then ( Hom (a1,a2)) <> {} & ( Hom (b1,b2)) <> {} by A1;

          then a1 = a2 & b1 = b2 by Def17;

          hence a = b by A2, A3;

        end;

        let a be Element of [:A, B:];

        consider a1 be Element of A, b1 be Element of B such that

         A4: a = [a1, b1] by DOMAIN_1: 1;

        ( Hom (a,a)) = [:( Hom (a1,a1)), ( Hom (b1,b1)):] by A4, CAT_2: 32;

        hence ( Hom (a,a)) is trivial;

      end;

    end

    ::$Canceled

    theorem :: NATTRA_1:41

    

     Th34: for A be discrete Category, B be Category, F1,F2 be Functor of B, A st F1 is_transformable_to F2 holds F1 = F2

    proof

      let A be discrete Category, B be Category, F1,F2 be Functor of B, A;

      assume

       A1: F1 is_transformable_to F2;

      now

        let m be Morphism of B;

        ( Hom ((F1 . ( dom m)),(F2 . ( dom m)))) <> {} by A1;

        then

         A2: (F1 . ( dom m)) = (F2 . ( dom m)) by Def17;

        

         A3: m in ( Hom (( dom m),( cod m)));

        then ( Hom ((F1 . ( dom m)),(F1 . ( cod m)))) <> {} by CAT_1: 81;

        then (F1 . ( dom m)) = (F1 . ( cod m)) by Def17;

        then

         A4: ( Hom ((F1 . ( dom m)),(F1 . ( cod m)))) = {( id (F1 . ( dom m)))} by Th33;

        ( Hom ((F2 . ( dom m)),(F2 . ( cod m)))) <> {} by A3, CAT_1: 81;

        then (F2 . ( dom m)) = (F2 . ( cod m)) by Def17;

        then

         A5: ( Hom ((F2 . ( dom m)),(F2 . ( cod m)))) = {( id (F2 . ( dom m)))} by Th33;

        (F1 . m) in ( Hom ((F1 . ( dom m)),(F1 . ( cod m)))) by A3, CAT_1: 81;

        then

         A6: (F1 . m) = ( id (F1 . ( dom m))) by A4, TARSKI:def 1;

        (F2 . m) in ( Hom ((F2 . ( dom m)),(F2 . ( cod m)))) by A3, CAT_1: 81;

        hence (F1 . m) = (F2 . m) by A2, A6, A5, TARSKI:def 1;

      end;

      hence thesis;

    end;

    theorem :: NATTRA_1:42

    

     Th35: for A be discrete Category, B be Category, F be Functor of B, A, t be transformation of F, F holds t = ( id F)

    proof

      let A be discrete Category, B be Category, F be Functor of B, A, t be transformation of F, F;

      now

        let a be Object of B;

        

         A1: ( Hom ((F . a),(F . a))) = {( id (F . a))} by Th33;

        (t . a) in ( Hom ((F . a),(F . a))) by CAT_1:def 5;

        

        hence (t . a) = ( id (F . a)) by A1, TARSKI:def 1

        .= (( id F) . a) by Th16;

      end;

      hence thesis by Th15;

    end;

    registration

      let B be Category, A be discrete Category;

      cluster ( Functors (B,A)) -> discrete;

      coherence

      proof

        thus ( Functors (B,A)) is quasi-discrete

        proof

          let a,b be Element of ( Functors (B,A));

          assume ( Hom (a,b)) <> {} ;

          then

          consider f be Morphism of a, b such that

           A1: f in ( Hom (a,b)) by CAT_1: 91;

          f in the carrier' of ( Functors (B,A));

          then f in ( NatTrans (B,A)) by Def16;

          then

          consider F1,F2 be Functor of B, A, t be natural_transformation of F1, F2 such that

           A2: f = [ [F1, F2], t] and

           A3: F1 is_naturally_transformable_to F2 by Def15;

          

           A4: F1 = ( dom f) by A2, Th29

          .= a by A1, CAT_1: 1;

          F2 = ( cod f) by A2, Th29

          .= b by A1, CAT_1: 1;

          hence a = b by A4, Th34, A3;

        end;

        let a be Element of ( Functors (B,A));

         A5:

        now

          let f be set such that

           A6: f in ( Hom (a,a));

          f in the carrier' of ( Functors (B,A)) by A6;

          then f in ( NatTrans (B,A)) by Def16;

          then

          consider F1,F2 be Functor of B, A, t be natural_transformation of F1, F2 such that

           A7: f = [ [F1, F2], t] and

           A8: F1 is_naturally_transformable_to F2 by Def15;

          reconsider ff = f as Morphism of ( Functors (B,A)) by A6;

          

           A9: F1 = ( dom ff) by A7, Th29

          .= a by A6, CAT_1: 1;

          

           A10: F1 = F2 by Th34, A8;

          then t = ( id F1) by Th35;

          hence f = ( id a) by A9, Def16, A7, A10;

        end;

        let x,y be object;

        assume x in ( Hom (a,a)) & y in ( Hom (a,a));

        then x = ( id a) & y = ( id a) by A5;

        hence thesis;

      end;

    end

    registration

      let C be Category;

      cluster strict discrete for Subcategory of C;

      existence

      proof

        set c = the Object of C;

        reconsider A = ( 1Cat (c,( id c))) as Subcategory of C by Th3;

        take A;

        thus thesis;

      end;

    end

    definition

      let C;

      :: NATTRA_1:def21

      func IdCat (C) -> strict Subcategory of C means

      : Def20: the carrier of it = the carrier of C & the carrier' of it = the set of all ( id a) where a be Object of C;

      existence

      proof

        defpred P[ Object of C] means not contradiction;

        deffunc F( Object of C) = ( id $1);

        defpred Q[ Object of C] means F($1) in the carrier' of C;

        set M = { F(a) where a be Object of C : P[a] };

        set N = { F(a) where a be Object of C : Q[a] };

        set N9 = { F(a) where a be Object of C : F(a) in the carrier' of C & P[a] };

        defpred R[ Object of C] means F($1) in the carrier' of C & P[$1];

        set N99 = { F(a) where a be Object of C : R[a] };

        set a = the Object of C;

        

         A1: ( id a) in M;

        

         A2: for a be Object of C holds Q[a] iff P[a];

        

         A3: N = M from FRAENKEL:sch 3( A2);

        

         A4: for a be Object of C holds Q[a] iff R[a];

        

         A5: N = N99 from FRAENKEL:sch 3( A4);

        N9 c= the carrier' of C from FRAENKEL:sch 17;

        then

        reconsider M as non empty Subset of the carrier' of C by A3, A5, A1;

        

         A6: ( rng (the Comp of C || M)) c= M

        proof

          let x be object;

          assume x in ( rng (the Comp of C || M));

          then

          consider y be object such that

           A7: y in ( dom (the Comp of C || M)) and

           A8: x = ((the Comp of C || M) . y) by FUNCT_1:def 3;

          

           A9: y in (( dom the Comp of C) /\ [:M, M:]) by A7, RELAT_1: 61;

          then

           A10: y in ( dom the Comp of C) by XBOOLE_0:def 4;

          y in [:M, M:] by A9, XBOOLE_0:def 4;

          then

          consider y1,y2 be object such that

           A11: y1 in M and

           A12: y2 in M and

           A13: y = [y1, y2] by ZFMISC_1: 84;

          consider a1 be Object of C such that

           A14: y1 = ( id a1) by A11;

          

           A15: ( Hom (a1,a1)) <> {} ;

          consider a2 be Object of C such that

           A16: y2 = ( id a2) by A12;

          

           A17: a1 = ( dom ( id a1))

          .= ( cod ( id a2)) by A13, A14, A16, A10, CAT_1: 15

          .= a2;

          ( id a1) = (( id a1) * ( id a1))

          .= (( id a1) (*) ( id a2)) by A15, A17, CAT_1:def 13

          .= (the Comp of C . (( id a1),( id a2))) by A13, A14, A16, A10, CAT_1:def 1

          .= x by A8, A9, A13, A14, A16, FUNCT_1: 48;

          hence thesis;

        end;

        (the Comp of C || M) is PartFunc of [:M, M qua non empty set:], the carrier' of C by PARTFUN1: 10;

        then

        reconsider COMP = (the Comp of C || M) as PartFunc of [:M, M qua non empty set:], M by A6, RELSET_1: 6;

        

         A18: the carrier of C c= the carrier of C;

        for o be Element of C st o in the carrier of C holds ( id o) in M;

        then

        reconsider A = CatStr (# the carrier of C, M, (the Source of C | M), (the Target of C | M), COMP #) as Subcategory of C by Th5, A18;

        reconsider A as strict Subcategory of C;

        take A;

        thus thesis;

      end;

      uniqueness

      proof

        let It1,It2 be strict Subcategory of C such that

         A19: the carrier of It1 = the carrier of C and

         A20: the carrier' of It1 = the set of all ( id a) where a be Object of C and

         A21: the carrier of It2 = the carrier of C and

         A22: the carrier' of It2 = the set of all ( id a) where a be Object of C;

        set M = the carrier' of It1;

        

         A23: the Target of It2 = (the Target of C | M) by A20, A22, Th4;

        

         A24: the Comp of It2 = (the Comp of C || M) by A20, A22, Th4;

        

         A25: the Source of It1 = (the Source of C | M) by Th4;

        

         A26: the Comp of It1 = (the Comp of C || M) by Th4;

        the Target of It1 = (the Target of C | M) by Th4;

        hence thesis by A19, A20, A21, A22, A25, A23, A26, A24, Th4;

      end;

    end

    registration

      let C;

      cluster ( IdCat C) -> discrete;

      coherence

      proof

        

         A1: the carrier' of ( IdCat C) = the set of all ( id a) where a be Object of C by Def20;

        thus ( IdCat C) is quasi-discrete

        proof

          let a,b be Element of ( IdCat C);

          assume ( Hom (a,b)) <> {} ;

          then

          consider m be object such that

           A2: m in ( Hom (a,b)) by XBOOLE_0:def 1;

          reconsider m as Morphism of ( IdCat C) by A2;

          m in the carrier' of ( IdCat C);

          then

          consider cc be Element of C such that

           A3: m = ( id cc) by A1;

          reconsider c = cc as Element of ( IdCat C) by Def20;

          

           A4: ( id c) in ( Hom (a,b)) by A3, A2, CAT_2:def 4;

          

          hence a = ( dom ( id c)) by CAT_1: 1

          .= ( cod ( id c))

          .= b by A4, CAT_1: 1;

        end;

        let c be Element of ( IdCat C);

        let x,y be object;

        assume

         A5: x in ( Hom (c,c)) & y in ( Hom (c,c));

        then

        reconsider a = x, b = y as Morphism of ( IdCat C);

        set M = the set of all ( id o) where o be Object of C;

        a in the carrier' of ( IdCat C);

        then a in M by Def20;

        then

        consider ox be Element of C such that

         A6: a = ( id ox);

        b in the carrier' of ( IdCat C);

        then b in M by Def20;

        then

        consider oy be Element of C such that

         A7: b = ( id oy);

        reconsider cc = c as Element of C by Def20;

        

         A8: ( Hom (c,c)) c= ( Hom (cc,cc)) by CAT_2:def 4;

        ox = ( dom ( id ox))

        .= cc by A8, A5, A6, CAT_1: 1

        .= ( dom ( id oy)) by A8, A5, A7, CAT_1: 1

        .= oy;

        hence x = y by A6, A7;

      end;

    end

    registration

      cluster strict discrete for Category;

      existence

      proof

        take ( IdCat the Category);

        thus thesis;

      end;

    end

    registration

      let C be strict discrete Category;

      reduce ( IdCat C) to C;

      reducibility

      proof

        the carrier' of C c= the set of all ( id a) where a be Object of C by Lm8;

        then

         A1: the carrier' of C c= the carrier' of ( IdCat C) by Def20;

        the carrier' of ( IdCat C) c= the carrier' of C by CAT_2: 7;

        then the carrier' of ( IdCat C) = the carrier' of C by A1;

        hence thesis by Def20, Th6;

      end;

    end

    ::$Canceled

    theorem :: NATTRA_1:47

    ( IdCat [:A, B:]) = [:( IdCat A), ( IdCat B):]

    proof

      now

        reconsider OA = the carrier of ( IdCat A) as non empty Subset of the carrier of A by CAT_2:def 4;

        set AB = the set of all ( id c) where c be Object of [:A, B:];

        set MA = the set of all ( id a) where a be Object of A;

        set MB = the set of all ( id b) where b be Object of B;

        

         A1: AB = [:MA, MB:]

        proof

          thus AB c= [:MA, MB:]

          proof

            let x be object;

            assume x in AB;

            then

            consider c be Object of [:A, B:] such that

             A2: x = ( id c);

            consider c1 be Object of A, c2 be Object of B such that

             A3: c = [c1, c2] by DOMAIN_1: 1;

            

             A4: ( id c2) in MB;

            

             A5: ( id c1) in MA;

            ( id c) = [( id c1), ( id c2)] by A3, CAT_2: 31;

            hence thesis by A2, A5, A4, ZFMISC_1: 87;

          end;

          let x be object;

          assume x in [:MA, MB:];

          then

          consider x1,x2 be object such that

           A6: x1 in MA and

           A7: x2 in MB and

           A8: x = [x1, x2] by ZFMISC_1: 84;

          consider a be Object of A such that

           A9: x1 = ( id a) by A6;

          consider b be Object of B such that

           A10: x2 = ( id b) by A7;

          ( id [a, b]) = [( id a), ( id b)] by CAT_2: 31;

          hence thesis by A8, A9, A10;

        end;

        reconsider OB = the carrier of ( IdCat B) as non empty Subset of the carrier of B by CAT_2:def 4;

        reconsider MB = the carrier' of ( IdCat B) as non empty Subset of the carrier' of B by CAT_2: 7;

        reconsider MA = the carrier' of ( IdCat A) as non empty Subset of the carrier' of A by CAT_2: 7;

        

         A11: the carrier of ( IdCat B) = the carrier of B by Def20;

        the carrier of ( IdCat A) = the carrier of A by Def20;

        hence [:the carrier of ( IdCat A), the carrier of ( IdCat B):] = the carrier of ( IdCat [:A, B:]) by A11, Def20;

        

         A12: the Target of ( IdCat B) = (the Target of B | the carrier' of ( IdCat B)) by Th4;

        

         A13: the Source of ( IdCat B) = (the Source of B | the carrier' of ( IdCat B)) by Th4;

        

         A14: the carrier' of ( IdCat B) = the set of all ( id b) where b be Object of B by Def20;

        the carrier' of ( IdCat A) = the set of all ( id a) where a be Object of A by Def20;

        hence

         A15: the carrier' of ( IdCat [:A, B:]) = [:the carrier' of ( IdCat A), the carrier' of ( IdCat B):] by A1, A14, Def20;

        the Source of ( IdCat A) = (the Source of A | the carrier' of ( IdCat A)) by Th4;

        

        hence [:the Source of ( IdCat A), the Source of ( IdCat B):] = ( [:the Source of A, the Source of B:] | [:MA, MB:]) by A13, FUNCT_3: 81

        .= the Source of ( IdCat [:A, B:]) by A15, Th4;

        the Target of ( IdCat A) = (the Target of A | the carrier' of ( IdCat A)) by Th4;

        

        hence [:the Target of ( IdCat A), the Target of ( IdCat B):] = ( [:the Target of A, the Target of B:] | [:MA, MB:]) by A12, FUNCT_3: 81

        .= the Target of ( IdCat [:A, B:]) by A15, Th4;

        

         A16: the Comp of ( IdCat A) = (the Comp of A || MA) by Th4;

        the Comp of ( IdCat B) = (the Comp of B || MB) by Th4;

        

        hence |:the Comp of ( IdCat A), the Comp of ( IdCat B):| = ( |:the Comp of A, the Comp of B:| || [:MA, MB:]) by A16, FUNCT_4: 126

        .= the Comp of ( IdCat [:A, B:]) by A15, Th4;

      end;

      hence thesis;

    end;