cat_1.miz



    begin

    definition

      struct ( MultiGraphStruct) CatStr (# the carrier, carrier' -> set,

the Source, Target -> Function of the carrier', the carrier,

the Comp -> PartFunc of [: the carrier', the carrier':], the carrier' #)

       attr strict strict;

    end

    reserve C for CatStr;

    definition

      let C;

      mode Object of C is Element of C;

      mode Morphism of C is Element of the carrier' of C;

    end

    reserve f,g for Morphism of C;

    registration

      cluster non void non empty for CatStr;

      existence

      proof

        take CatStr (# { 0 }, { { 0 }}, ( { 0 } :-> 0 ), ( { 0 } :-> 0 ), (( { 0 }, { 0 }) :-> { 0 }) #);

        thus thesis;

      end;

    end

    definition

      let C, f, g;

      assume

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

      :: CAT_1:def1

      func g (*) f -> Morphism of C equals

      : Def1: (the Comp of C . (g,f));

      coherence by A1, PARTFUN1: 4;

    end

    definition

      ::$Canceled

      let C be non void non empty CatStr, a,b be Object of C;

      :: CAT_1:def4

      func Hom (a,b) -> Subset of the carrier' of C equals { f where f be Morphism of C : ( dom f) = a & ( cod f) = b };

      correctness

      proof

        set M = { f where f be Morphism of C : ( dom f) = a & ( cod f) = b };

        M c= the carrier' of C

        proof

          let x be object;

          assume x in M;

          then ex f be Morphism of C st x = f & ( dom f) = a & ( cod f) = b;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    reserve C for non void non empty CatStr,

f,g for Morphism of C,

a,b,c,d for Object of C;

    theorem :: CAT_1:1

    

     Th1: f in ( Hom (a,b)) iff ( dom f) = a & ( cod f) = b

    proof

      thus f in ( Hom (a,b)) implies ( dom f) = a & ( cod f) = b

      proof

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

        then ex g st f = g & ( dom g) = a & ( cod g) = b;

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: CAT_1:2

    ( Hom (( dom f),( cod f))) <> {} by Th1;

    definition

      let C, a, b;

      assume

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

      :: CAT_1:def5

      mode Morphism of a,b -> Morphism of C means

      : Def3: it in ( Hom (a,b));

      existence by A1, SUBSET_1: 4;

    end

    ::$Canceled

    theorem :: CAT_1:4

    

     Th3: for f be Morphism of C holds f is Morphism of ( dom f), ( cod f)

    proof

      let f be Morphism of C;

      f in ( Hom (( dom f),( cod f)));

      hence thesis by Def3;

    end;

    theorem :: CAT_1:5

    

     Th4: for f be Morphism of a, b st ( Hom (a,b)) <> {} holds ( dom f) = a & ( cod f) = b

    proof

      let f be Morphism of a, b;

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

      then f in ( Hom (a,b)) by Def3;

      hence thesis by Th1;

    end;

    theorem :: CAT_1:6

    for f be Morphism of a, b holds for h be Morphism of c, d st ( Hom (a,b)) <> {} & ( Hom (c,d)) <> {} & f = h holds a = c & b = d

    proof

      let f be Morphism of a, b;

      let h be Morphism of c, d;

      assume that

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

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

      ( dom f) = a & ( cod f) = b by A1, Th4;

      hence thesis by A2, Th4;

    end;

    theorem :: CAT_1:7

    

     Th6: for f be Morphism of a, b st ( Hom (a,b)) = {f} holds for g be Morphism of a, b holds f = g

    proof

      let f be Morphism of a, b such that

       A1: ( Hom (a,b)) = {f};

      let g be Morphism of a, b;

      g in {f} by A1, Def3;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: CAT_1:8

    

     Th7: for f be Morphism of a, b st ( Hom (a,b)) <> {} & for g be Morphism of a, b holds f = g holds ( Hom (a,b)) = {f}

    proof

      let f be Morphism of a, b such that

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

       A2: for g be Morphism of a, b holds f = g;

      for x be object holds x in ( Hom (a,b)) iff x = f

      proof

        let x be object;

        thus x in ( Hom (a,b)) implies x = f

        proof

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

          then

          consider g be Morphism of C such that

           A3: x = g and

           A4: ( dom g) = a & ( cod g) = b;

          g is Morphism of a, b by A4, Th3;

          hence thesis by A2, A3;

        end;

        thus thesis by A1, Def3;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: CAT_1:9

    for f be Morphism of a, b st (( Hom (a,b)),( Hom (c,d))) are_equipotent & ( Hom (a,b)) = {f} holds ex h be Morphism of c, d st ( Hom (c,d)) = {h}

    proof

      let f be Morphism of a, b;

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

      then

      consider F be Function such that F is one-to-one and

       A1: ( dom F) = ( Hom (a,b)) & ( rng F) = ( Hom (c,d)) by WELLORD2:def 4;

      assume ( Hom (a,b)) = {f};

      then

       A2: ( Hom (c,d)) = {(F . f)} by A1, FUNCT_1: 4;

      then (F . f) in ( Hom (c,d)) by TARSKI:def 1;

      then (F . f) is Morphism of c, d by Def3;

      hence thesis by A2;

    end;

    definition

      let C be non empty non void CatStr;

      :: CAT_1:def6

      attr C is Category-like means

      : Def4: for f,g be Morphism of C holds [g, f] in ( dom the Comp of C) iff ( dom g) = ( cod f);

      :: CAT_1:def7

      attr C is transitive means

      : Def5: for f,g be Morphism of C st ( dom g) = ( cod f) holds ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g);

      :: CAT_1:def8

      attr C is associative means

      : Def6: for f,g,h be Morphism of C st ( dom h) = ( cod g) & ( dom g) = ( cod f) holds (h (*) (g (*) f)) = ((h (*) g) (*) f);

      :: CAT_1:def9

      attr C is reflexive means

      : Def7: for b be Element of C holds ( Hom (b,b)) <> {} ;

      :: CAT_1:def10

      attr C is with_identities means

      : Def8: for a be Element of C holds ex i be Morphism of a, a st for b be Element of C holds (( Hom (a,b)) <> {} implies for g be Morphism of a, b holds (g (*) i) = g) & (( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (i (*) f) = f);

    end

    definition

      let o,m be object;

      :: CAT_1:def11

      func 1Cat (o,m) -> strict CatStr equals CatStr (# {o}, {m}, (m :-> o), (m :-> o), ((m,m) :-> m) #);

      correctness ;

    end

    registration

      let o,m be object;

      cluster ( 1Cat (o,m)) -> non empty trivial non void trivial';

      coherence ;

    end

    registration

      cluster non empty trivial -> transitive reflexive for non empty non void CatStr;

      coherence

      proof

        let C be non empty non void CatStr such that

         A1: C is non empty trivial;

        thus for f,g be Morphism of C st ( dom g) = ( cod f) holds ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g) by A1, ZFMISC_1:def 10;

        let b be Element of C;

        set i = the Morphism of C;

        ( cod i) = b & ( dom i) = b by A1, ZFMISC_1:def 10;

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

      end;

    end

    registration

      cluster non void trivial' -> associative with_identities for non empty non void CatStr;

      coherence

      proof

        let C be non empty non void CatStr such that

         A1: C is non void trivial';

        thus for f,g,h be Morphism of C st ( dom h) = ( cod g) & ( dom g) = ( cod f) holds (h (*) (g (*) f)) = ((h (*) g) (*) f) by A1, ZFMISC_1:def 10;

        let a be Element of C;

        take i = the Morphism of a, a;

        let b be Element of C;

        thus ( Hom (a,b)) <> {} implies for g be Morphism of a, b holds (g (*) i) = g by A1, ZFMISC_1:def 10;

        thus ( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (i (*) f) = f by A1, ZFMISC_1:def 10;

      end;

    end

    registration

      let o,m be object;

      cluster ( 1Cat (o,m)) -> Category-like;

      coherence

      proof

        let f,g be Morphism of ( 1Cat (o,m));

        thus [g, f] in ( dom the Comp of ( 1Cat (o,m))) implies ( dom g) = ( cod f) by ZFMISC_1:def 10;

        assume ( dom g) = ( cod f);

        

         A1: ( dom the Comp of ( 1Cat (o,m))) = { [m, m]} by FUNCOP_1: 13;

        f = m & g = m by TARSKI:def 1;

        hence thesis by A1, TARSKI:def 1;

      end;

    end

    registration

      cluster reflexive transitive associative with_identities Category-like non void non empty strict for non empty non void CatStr;

      existence

      proof

        take ( 1Cat ( 0 , 0 ));

        thus thesis;

      end;

    end

    definition

      mode Category is reflexive transitive associative with_identities Category-like non void non empty CatStr;

    end

    registration

      let C be reflexive non void non empty CatStr, a be Object of C;

      cluster ( Hom (a,a)) -> non empty;

      coherence by Def7;

    end

    ::$Canceled

    reserve o,m for set;

    theorem :: CAT_1:11

    

     Th9: for a,b be Object of ( 1Cat (o,m)) holds for f be Morphism of ( 1Cat (o,m)) holds f in ( Hom (a,b))

    proof

      let a,b be Object of ( 1Cat (o,m));

      let f be Morphism of ( 1Cat (o,m));

      ( dom f) = o by TARSKI:def 1;

      then ( dom f) = a & ( cod f) = b by TARSKI:def 1;

      hence thesis;

    end;

    theorem :: CAT_1:12

    for a,b be Object of ( 1Cat (o,m)) holds for f be Morphism of ( 1Cat (o,m)) holds f is Morphism of a, b

    proof

      let a,b be Object of ( 1Cat (o,m));

      let f be Morphism of ( 1Cat (o,m));

      f in ( Hom (a,b)) by Th9;

      hence thesis by Def3;

    end;

    theorem :: CAT_1:13

    for a,b be Object of ( 1Cat (o,m)) holds ( Hom (a,b)) <> {} by Th9;

    theorem :: CAT_1:14

    for a,b,c,d be Object of ( 1Cat (o,m)) holds for f be Morphism of a, b holds for g be Morphism of c, d holds f = g

    proof

      let a,b,c,d be Object of ( 1Cat (o,m));

      let f be Morphism of a, b;

      let g be Morphism of c, d;

      f = m by TARSKI:def 1;

      hence thesis by TARSKI:def 1;

    end;

    reserve B,C,D for Category;

    reserve a,b,c,d for Object of C;

    reserve f,f1,f2,g,g1,g2 for Morphism of C;

    theorem :: CAT_1:15

    ( dom g) = ( cod f) iff [g, f] in ( dom the Comp of C) by Def4;

    theorem :: CAT_1:16

    

     Th14: ( dom g) = ( cod f) implies (g (*) f) = (the Comp of C . (g,f))

    proof

      assume ( dom g) = ( cod f);

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

      hence thesis by Def1;

    end;

    theorem :: CAT_1:17

    for f,g be Morphism of C st ( dom g) = ( cod f) holds ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g) by Def5;

    theorem :: CAT_1:18

    for f,g,h be Morphism of C st ( dom h) = ( cod g) & ( dom g) = ( cod f) holds (h (*) (g (*) f)) = ((h (*) g) (*) f) by Def6;

    definition

      let C be with_identities reflexive non void non empty CatStr, a be Object of C;

      :: CAT_1:def12

      func id a -> Morphism of a, a means

      : Def10: for b be Object of C holds (( Hom (a,b)) <> {} implies for f be Morphism of a, b holds (f (*) it ) = f) & (( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (it (*) f) = f);

      existence by Def8;

      uniqueness

      proof

        let m1,m2 be Morphism of a, a such that

         A1: for b be Object of C holds (( Hom (a,b)) <> {} implies for f be Morphism of a, b holds (f (*) m1) = f) & (( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (m1 (*) f) = f) and

         A2: for b be Object of C holds (( Hom (a,b)) <> {} implies for f be Morphism of a, b holds (f (*) m2) = f) & (( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (m2 (*) f) = f);

        

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

        

        hence m1 = (m1 (*) m2) by A2

        .= m2 by A3, A1;

      end;

    end

    ::$Canceled

    theorem :: CAT_1:21

    for f be Morphism of C st ( cod f) = b holds (( id b) (*) f) = f

    proof

      let f be Morphism of C;

      assume

       A1: ( cod f) = b;

      then

      reconsider ff = f as Morphism of ( dom f), b by Th3;

      ( Hom (( dom f),b)) <> {} by A1, Th1;

      then (( id b) (*) ff) = ff by Def10;

      hence thesis;

    end;

    theorem :: CAT_1:22

    for g be Morphism of C st ( dom g) = b holds (g (*) ( id b)) = g

    proof

      let f be Morphism of C;

      assume

       A1: ( dom f) = b;

      then

      reconsider ff = f as Morphism of b, ( cod f) by Th3;

      ( Hom (b,( cod f))) <> {} by A1, Th1;

      then (ff (*) ( id b)) = ff by Def10;

      hence thesis;

    end;

    reserve f,f1,f2 for Morphism of a, b;

    reserve f9 for Morphism of b, a;

    reserve g for Morphism of b, c;

    reserve h,h1,h2 for Morphism of c, d;

    theorem :: CAT_1:23

    

     Th19: ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} implies (g (*) f) in ( Hom (a,c))

    proof

      assume that

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

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

      

       A3: f in ( Hom (a,b)) by A1, Def3;

      then

       A4: ( cod f) = b by Th1;

      

       A5: g in ( Hom (b,c)) by A2, Def3;

      then

       A6: ( dom g) = b by Th1;

      ( cod g) = c by A5, Th1;

      then

       A7: ( cod (g (*) f)) = c by A6, A4, Def5;

      ( dom f) = a by A3, Th1;

      then ( dom (g (*) f)) = a by A6, A4, Def5;

      hence thesis by A7;

    end;

    definition

      let C, a, b, c, f, g;

      assume

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

      :: CAT_1:def13

      func g * f -> Morphism of a, c equals

      : Def11: (g (*) f);

      correctness

      proof

        (g (*) f) in ( Hom (a,c)) by A1, Th19;

        hence thesis by Def3;

      end;

    end

    theorem :: CAT_1:24

    ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} implies ( Hom (a,c)) <> {} by Th19;

    theorem :: CAT_1:25

    

     Th21: ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} & ( Hom (c,d)) <> {} implies ((h * g) * f) = (h * (g * f))

    proof

      assume that

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

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

       A3: ( Hom (c,d)) <> {} ;

      

       A4: ( Hom (a,c)) <> {} by A1, A2, Th19;

      h in ( Hom (c,d)) by A3, Def3;

      then

       A5: ( dom h) = c by Th1;

      g in ( Hom (b,c)) by A2, Def3;

      then

       A6: ( cod g) = c & ( dom g) = b by Th1;

      reconsider hh = h as Morphism of C;

      reconsider gg = g as Morphism of C;

      reconsider ff = f as Morphism of C;

      f in ( Hom (a,b)) by A1, Def3;

      then

       A7: ( cod f) = b by Th1;

      ( Hom (b,d)) <> {} by A2, A3, Th19;

      

      hence ((h * g) * f) = ((h * g) (*) ff) by A1, Def11

      .= ((hh (*) gg) (*) ff) by A2, A3, Def11

      .= (hh (*) (gg (*) ff)) by A5, A6, A7, Def6

      .= (hh (*) (g * f)) by A1, A2, Def11

      .= (h * (g * f)) by A3, A4, Def11;

    end;

    ::$Canceled

    theorem :: CAT_1:27

    ( id a) in ( Hom (a,a)) by Def3;

    theorem :: CAT_1:28

    

     Th23: ( Hom (a,b)) <> {} implies (( id b) * f) = f

    proof

      assume

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

      

       A2: (( id b) (*) f) = f by A1, Def10;

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

      hence thesis by A1, A2, Def11;

    end;

    theorem :: CAT_1:29

    

     Th24: ( Hom (b,c)) <> {} implies (g * ( id b)) = g

    proof

      assume

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

      

       A2: (g (*) ( id b)) = g by A1, Def10;

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

      hence thesis by A1, A2, Def11;

    end;

    registration

      let C, a;

      let f be Morphism of a, a;

      

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

      reduce (f * ( id a)) to f;

      reducibility by A1, Th24;

      reduce (( id a) * f) to f;

      reducibility by A1, Th23;

    end

    theorem :: CAT_1:30

    (( id a) * ( id a)) = ( id a);

    definition

      let C be Category, b,c be Object of C, g be Morphism of b, c;

      :: CAT_1:def14

      attr g is monic means ( Hom (b,c)) <> {} & for a be Object of C st ( Hom (a,b)) <> {} holds for f1,f2 be Morphism of a, b st (g * f1) = (g * f2) holds f1 = f2;

    end

    definition

      let C be Category, a,b be Object of C, f be Morphism of a, b;

      :: CAT_1:def15

      attr f is epi means ( Hom (a,b)) <> {} & for c be Object of C st ( Hom (b,c)) <> {} holds for g1,g2 be Morphism of b, c st (g1 * f) = (g2 * f) holds g1 = g2;

    end

    definition

      let C be Category, a,b be Object of C, f be Morphism of a, b;

      :: CAT_1:def16

      attr f is invertible means ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} & ex g be Morphism of b, a st (f * g) = ( id b) & (g * f) = ( id a);

    end

    theorem :: CAT_1:31

    ( Hom (b,c)) <> {} implies (g is monic iff for a holds for f1,f2 be Morphism of a, b st ( Hom (a,b)) <> {} & (g * f1) = (g * f2) holds f1 = f2);

    theorem :: CAT_1:32

    g is monic & h is monic implies (h * g) is monic

    proof

      assume that

       A1: g is monic and

       A2: h is monic;

      

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

      

       A4: ( Hom (c,d)) <> {} by A2;

       A5:

      now

        let a, f1, f2 such that

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

         A7: ((h * g) * f1) = ((h * g) * f2);

        

         A8: ( Hom (a,c)) <> {} by A3, A6, Th19;

        (h * (g * f1)) = ((h * g) * f1) & ((h * g) * f2) = (h * (g * f2)) by A3, A4, A6, Th21;

        then (g * f1) = (g * f2) by A2, A7, A8;

        hence f1 = f2 by A1, A6;

      end;

      ( Hom (b,d)) <> {} by A3, A4, Th19;

      hence thesis by A5;

    end;

    theorem :: CAT_1:33

    ( Hom (b,c)) <> {} & ( Hom (c,d)) <> {} & (h * g) is monic implies g is monic

    proof

      assume that

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

       A2: ( Hom (c,d)) <> {} and

       A3: (h * g) is monic;

      now

        let a, f1, f2;

        assume

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

        then (h * (g * f1)) = ((h * g) * f1) & (h * (g * f2)) = ((h * g) * f2) by A1, A2, Th21;

        hence (g * f1) = (g * f2) implies f1 = f2 by A3, A4;

      end;

      hence thesis by A1;

    end;

    theorem :: CAT_1:34

    for h be Morphism of a, b holds for g be Morphism of b, a st ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} & (h * g) = ( id b) holds g is monic

    proof

      let h be Morphism of a, b;

      let g be Morphism of b, a such that

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

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

       A3: (h * g) = ( id b);

      now

        let c;

        let g1,g2 be Morphism of c, b such that

         A4: ( Hom (c,b)) <> {} and

         A5: (g * g1) = (g * g2);

        

        thus g1 = ((h * g) * g1) by A3, A4, Th23

        .= (h * (g * g2)) by A1, A2, A4, A5, Th21

        .= ((h * g) * g2) by A1, A2, A4, Th21

        .= g2 by A3, A4, Th23;

      end;

      hence thesis by A2;

    end;

    theorem :: CAT_1:35

    ( id b) is monic

    proof

       A1:

      now

        let a;

        let f1,f2 be Morphism of a, b;

        assume

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

        then (( id b) * f1) = f1 by Th23;

        hence (( id b) * f1) = (( id b) * f2) implies f1 = f2 by A2, Th23;

      end;

      thus thesis by A1;

    end;

    theorem :: CAT_1:36

    ( Hom (a,b)) <> {} implies (f is epi iff for c holds for g1,g2 be Morphism of b, c st ( Hom (b,c)) <> {} & (g1 * f) = (g2 * f) holds g1 = g2);

    theorem :: CAT_1:37

    f is epi & g is epi implies (g * f) is epi

    proof

      assume that

       A1: f is epi and

       A2: g is epi;

      

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

      

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

       A5:

      now

        let d, h1, h2 such that

         A6: ( Hom (c,d)) <> {} and

         A7: (h1 * (g * f)) = (h2 * (g * f));

        

         A8: ( Hom (b,d)) <> {} by A4, A6, Th19;

        (h1 * (g * f)) = ((h1 * g) * f) & ((h2 * g) * f) = (h2 * (g * f)) by A3, A4, A6, Th21;

        then (h1 * g) = (h2 * g) by A1, A7, A8;

        hence h1 = h2 by A2, A6;

      end;

      ( Hom (a,c)) <> {} by A3, A4, Th19;

      hence thesis by A5;

    end;

    theorem :: CAT_1:38

    ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} & (g * f) is epi implies g is epi

    proof

      assume that

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

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

       A3: (g * f) is epi;

      now

        let d, h1, h2;

        assume

         A4: ( Hom (c,d)) <> {} ;

        then (h1 * (g * f)) = ((h1 * g) * f) & (h2 * (g * f)) = ((h2 * g) * f) by A1, A2, Th21;

        hence (h1 * g) = (h2 * g) implies h1 = h2 by A3, A4;

      end;

      hence thesis by A2;

    end;

    theorem :: CAT_1:39

    for h be Morphism of a, b holds for g be Morphism of b, a st ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} & (h * g) = ( id b) holds h is epi

    proof

      let h be Morphism of a, b;

      let g be Morphism of b, a;

      assume that

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

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

       A3: (h * g) = ( id b);

      now

        let c;

        let h1,h2 be Morphism of b, c such that

         A4: ( Hom (b,c)) <> {} and

         A5: (h1 * h) = (h2 * h);

        

        thus h1 = (h1 * (h * g)) by A3, A4, Th24

        .= ((h2 * h) * g) by A1, A2, A4, A5, Th21

        .= (h2 * (h * g)) by A1, A2, A4, Th21

        .= h2 by A3, A4, Th24;

      end;

      hence thesis by A1;

    end;

    theorem :: CAT_1:40

    ( id b) is epi

    proof

       A1:

      now

        let c;

        let g1,g2 be Morphism of b, c;

        assume

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

        then (g1 * ( id b)) = g1 by Th24;

        hence (g1 * ( id b)) = (g2 * ( id b)) implies g1 = g2 by A2, Th24;

      end;

      thus thesis by A1;

    end;

    theorem :: CAT_1:41

    ( Hom (a,b)) <> {} implies (f is invertible iff ( Hom (b,a)) <> {} & ex g be Morphism of b, a st (f * g) = ( id b) & (g * f) = ( id a));

    theorem :: CAT_1:42

    

     Th37: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} implies for g1,g2 be Morphism of b, a st (f * g1) = ( id b) & (g2 * f) = ( id a) holds g1 = g2

    proof

      assume that

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

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

      let g1,g2 be Morphism of b, a;

      assume

       A3: (f * g1) = ( id b);

      assume (g2 * f) = ( id a);

      

      hence g1 = ((g2 * f) * g1) by A2, Th23

      .= (g2 * ( id b)) by A1, A2, A3, Th21

      .= g2 by A2, Th24;

    end;

    definition

      let C, a, b, f;

      assume that

       A1: f is invertible;

      :: CAT_1:def17

      func f " -> Morphism of b, a means

      : Def15: (f * it ) = ( id b) & (it * f) = ( id a);

      existence by A1;

      uniqueness by A1, Th37;

    end

    theorem :: CAT_1:43

    f is invertible implies f is monic & f is epi

    proof

      assume that

       A1: f is invertible;

      

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

      consider k be Morphism of b, a such that

       A3: (f * k) = ( id b) and

       A4: (k * f) = ( id a) by A1;

      

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

      now

        let c be Object of C, g,h be Morphism of c, a such that

         A6: ( Hom (c,a)) <> {} and

         A7: (f * g) = (f * h);

        g = ((k * f) * g) by A4, A6, Th23

        .= (k * (f * h)) by A2, A5, A6, A7, Th21

        .= (( id a) * h) by A2, A5, A4, A6, Th21;

        hence g = h by A6, Th23;

      end;

      hence f is monic by A2;

      now

        let c be Object of C, g,h be Morphism of b, c such that

         A8: ( Hom (b,c)) <> {} and

         A9: (g * f) = (h * f);

        g = (g * (f * k)) by A3, A8, Th24

        .= ((h * f) * k) by A2, A5, A8, A9, Th21

        .= (h * ( id b)) by A2, A5, A3, A8, Th21;

        hence g = h by A8, Th24;

      end;

      hence thesis by A2;

    end;

    theorem :: CAT_1:44

    ( id a) is invertible

    proof

      ( Hom (a,a)) <> {} & (( id a) * ( id a)) = ( id a);

      hence thesis;

    end;

    theorem :: CAT_1:45

    

     Th40: f is invertible & g is invertible implies (g * f) is invertible

    proof

      assume

       A1: f is invertible;

      then

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

      consider f1 be Morphism of b, a such that

       A3: (f * f1) = ( id b) and

       A4: (f1 * f) = ( id a) by A1;

      assume

       A5: g is invertible;

      then

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

      consider g1 be Morphism of c, b such that

       A7: (g * g1) = ( id c) and

       A8: (g1 * g) = ( id b) by A5;

       A9:

      now

        thus

         A10: ( Hom (c,a)) <> {} by A2, A6, Th19;

        take f1g1 = (f1 * g1);

        

        thus ((g * f) * f1g1) = (g * (f * (f1 * g1))) by A2, A6, A10, Th21

        .= (g * (( id b) * g1)) by A2, A3, A6, Th21

        .= ( id c) by A6, A7, Th23;

        ( Hom (a,c)) <> {} by A2, A6, Th19;

        

        hence (f1g1 * (g * f)) = (f1 * (g1 * (g * f))) by A2, A6, Th21

        .= (f1 * (( id b) * f)) by A2, A6, A8, Th21

        .= ( id a) by A2, A4, Th23;

      end;

      ( Hom (a,c)) <> {} by A2, A6, Th19;

      hence thesis by A9;

    end;

    theorem :: CAT_1:46

    f is invertible implies (f " ) is invertible

    proof

      assume

       A1: f is invertible;

      then

       A2: (f * (f " )) = ( id b) by Def15;

      

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

      ( Hom (b,a)) <> {} & ((f " ) * f) = ( id a) by A1, Def15;

      hence thesis by A3, A2;

    end;

    theorem :: CAT_1:47

    f is invertible & g is invertible implies ((g * f) " ) = ((f " ) * (g " ))

    proof

      assume that

       A1: f is invertible and

       A2: g is invertible;

      

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

      

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

      

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

      

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

      then

       A7: ( Hom (c,a)) <> {} by A5, Th19;

      

      then

       A8: (((f " ) * (g " )) * (g * f)) = ((((f " ) * (g " )) * g) * f) by A3, A4, Th21

      .= (((f " ) * ((g " ) * g)) * f) by A4, A6, A5, Th21

      .= (((f " ) * ( id b)) * f) by A2, Def15

      .= ((f " ) * f) by A6, Th24

      .= ( id a) by A1, Def15;

      

       A9: ( Hom (a,c)) <> {} & (g * f) is invertible by A1, A2, Th19, Th40;

      ((g * f) * ((f " ) * (g " ))) = (g * (f * ((f " ) * (g " )))) by A3, A4, A7, Th21

      .= (g * ((f * (f " )) * (g " ))) by A3, A6, A5, Th21

      .= (g * (( id b) * (g " ))) by A1, Def15

      .= (g * (g " )) by A5, Th23

      .= ( id c) by A2, Def15;

      hence thesis by A8, A9, Def15;

    end;

    definition

      let C, a;

      :: CAT_1:def18

      attr a is terminal means ( Hom (b,a)) <> {} & ex f be Morphism of b, a st for g be Morphism of b, a holds f = g;

      :: CAT_1:def19

      attr a is initial means ( Hom (a,b)) <> {} & ex f be Morphism of a, b st for g be Morphism of a, b holds f = g;

      let b;

      :: CAT_1:def20

      pred a,b are_isomorphic means ex f st f is invertible;

      reflexivity

      proof

        let a be Object of C;

        take ( id a);

        (( id a) * ( id a)) = ( id a);

        hence thesis;

      end;

      symmetry

      proof

        let a,b be Object of C;

        given f be Morphism of a, b such that

         A1: f is invertible;

        

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

        consider g be Morphism of b, a such that

         A3: (f * g) = ( id b) & (g * f) = ( id a) by A1;

        take g;

        thus g is invertible by A2, A3;

      end;

    end

    theorem :: CAT_1:48

    (a,b) are_isomorphic iff ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} & ex f, f9 st (f * f9) = ( id b) & (f9 * f) = ( id a)

    proof

      thus (a,b) are_isomorphic implies ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} & ex f, f9 st (f * f9) = ( id b) & (f9 * f) = ( id a)

      proof

        given f such that

         A1: f is invertible;

        thus ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} by A1;

        take f;

        thus thesis by A1;

      end;

      assume that

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

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

      given f such that

       A4: ex f9 st (f * f9) = ( id b) & (f9 * f) = ( id a);

      take f;

      thus thesis by A2, A3, A4;

    end;

    theorem :: CAT_1:49

    a is initial iff for b holds ex f be Morphism of a, b st ( Hom (a,b)) = {f}

    proof

      thus a is initial implies for b holds ex f be Morphism of a, b st ( Hom (a,b)) = {f}

      proof

        assume

         A1: a is initial;

        let b;

        consider f be Morphism of a, b such that

         A2: for g be Morphism of a, b holds f = g by A1;

        take f;

        thus thesis by A2, Th7, A1;

      end;

      assume

       A3: for b holds ex f be Morphism of a, b st ( Hom (a,b)) = {f};

      let b;

      consider f be Morphism of a, b such that

       A4: ( Hom (a,b)) = {f} by A3;

      thus ( Hom (a,b)) <> {} by A4;

      take f;

      thus thesis by A4, Th6;

    end;

    theorem :: CAT_1:50

    

     Th45: a is initial implies for h be Morphism of a, a holds ( id a) = h

    proof

      assume a is initial;

      then

      consider f be Morphism of a, a such that

       A1: for g be Morphism of a, a holds f = g;

      let h be Morphism of a, a;

      ( id a) = f by A1;

      hence thesis by A1;

    end;

    theorem :: CAT_1:51

    a is initial & b is initial implies (a,b) are_isomorphic

    proof

      assume that

       A1: a is initial and

       A2: b is initial;

      set g = the Morphism of b, a;

      set f = the Morphism of a, b;

      

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

      take f;

      now

        thus ( Hom (b,a)) <> {} by A2;

        take g;

        thus (f * g) = ( id b) & (g * f) = ( id a) by A1, A2, Th45;

      end;

      hence thesis by A3;

    end;

    theorem :: CAT_1:52

    a is initial & (a,b) are_isomorphic implies b is initial

    proof

      assume that

       A1: a is initial;

      given f such that

       A2: f is invertible;

      

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

      let c;

      consider h be Morphism of a, c such that

       A4: for g be Morphism of a, c holds h = g by A1;

      ( Hom (a,c)) <> {} by A1;

      hence

       A5: ( Hom (b,c)) <> {} by A3, Th19;

      consider f9 such that

       A6: (f * f9) = ( id b) and (f9 * f) = ( id a) by A2;

      

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

      take (h * f9);

      let h9 be Morphism of b, c;

      

      thus h9 = (h9 * (f * f9)) by A6, A5, Th24

      .= ((h9 * f) * f9) by A3, A5, A7, Th21

      .= (h * f9) by A4;

    end;

    theorem :: CAT_1:53

    b is terminal iff for a holds ex f be Morphism of a, b st ( Hom (a,b)) = {f}

    proof

      thus b is terminal implies for a holds ex f be Morphism of a, b st ( Hom (a,b)) = {f}

      proof

        assume

         A1: b is terminal;

        let a;

        consider f be Morphism of a, b such that

         A2: for g be Morphism of a, b holds f = g by A1;

        take f;

        thus thesis by A2, Th7, A1;

      end;

      assume

       A3: for a holds ex f be Morphism of a, b st ( Hom (a,b)) = {f};

      let a;

      consider f be Morphism of a, b such that

       A4: ( Hom (a,b)) = {f} by A3;

      thus ( Hom (a,b)) <> {} by A4;

      take f;

      thus thesis by A4, Th6;

    end;

    theorem :: CAT_1:54

    

     Th49: a is terminal implies for h be Morphism of a, a holds ( id a) = h

    proof

      assume a is terminal;

      then

      consider f be Morphism of a, a such that

       A1: for g be Morphism of a, a holds f = g;

      let h be Morphism of a, a;

      ( id a) = f by A1;

      hence thesis by A1;

    end;

    theorem :: CAT_1:55

    a is terminal & b is terminal implies (a,b) are_isomorphic

    proof

      assume that

       A1: a is terminal and

       A2: b is terminal;

      set g = the Morphism of b, a;

      set f = the Morphism of a, b;

      

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

      take f;

      now

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

        take g;

        thus (f * g) = ( id b) & (g * f) = ( id a) by A1, A2, Th49;

      end;

      hence thesis by A3;

    end;

    theorem :: CAT_1:56

    b is terminal & (a,b) are_isomorphic implies a is terminal

    proof

      assume that

       A1: b is terminal;

      given f such that

       A2: f is invertible;

      

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

      let c;

      consider h be Morphism of c, b such that

       A4: for g be Morphism of c, b holds h = g by A1;

      ( Hom (c,b)) <> {} by A1;

      hence

       A5: ( Hom (c,a)) <> {} by A3, Th19;

      consider f9 such that (f * f9) = ( id b) and

       A6: (f9 * f) = ( id a) by A2;

      

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

      take (f9 * h);

      let h9 be Morphism of c, a;

      

      thus (f9 * h) = (f9 * (f * h9)) by A4

      .= ((f9 * f) * h9) by A3, A5, A7, Th21

      .= h9 by A6, A5, Th23;

    end;

    theorem :: CAT_1:57

    ( Hom (a,b)) <> {} & a is terminal implies f is monic

    proof

      assume that

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

       A2: a is terminal;

      now

        let c be Object of C, g,h be Morphism of c, a such that ( Hom (c,a)) <> {} and (f * g) = (f * h);

        consider ff be Morphism of c, a such that

         A3: for gg be Morphism of c, a holds ff = gg by A2;

        ff = g by A3;

        hence g = h by A3;

      end;

      hence thesis by A1;

    end;

    registration

      let C, a;

      reduce ( dom ( id a)) to a;

      reducibility

      proof

        ( id a) in ( Hom (a,a)) by Def3;

        hence thesis by Th1;

      end;

      reduce ( cod ( id a)) to a;

      reducibility

      proof

        ( id a) in ( Hom (a,a)) by Def3;

        hence thesis by Th1;

      end;

    end

    theorem :: CAT_1:58

    

     Th53: ( dom ( id a)) = a & ( cod ( id a)) = a;

    theorem :: CAT_1:59

    

     Th54: ( id a) = ( id b) implies a = b

    proof

      assume

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

      

      thus a = ( dom ( id a))

      .= b by Th53, A1;

    end;

    theorem :: CAT_1:60

    (a,b) are_isomorphic & (b,c) are_isomorphic implies (a,c) are_isomorphic

    proof

      given f be Morphism of a, b such that

       A1: f is invertible;

      given g be Morphism of b, c such that

       A2: g is invertible;

      take (g * f);

      thus thesis by A1, A2, Th40;

    end;

    definition

      let C, D;

      :: CAT_1:def21

      mode Functor of C,D -> Function of the carrier' of C, the carrier' of D means

      : Def19: (for c be Element of C holds ex d be Element of D st (it . ( id c)) = ( id d)) & (for f be Element of the carrier' of C holds (it . ( id ( dom f))) = ( id ( dom (it . f))) & (it . ( id ( cod f))) = ( id ( cod (it . f)))) & for f,g be Element of the carrier' of C st [g, f] in ( dom the Comp of C) holds (it . (g (*) f)) = ((it . g) (*) (it . f));

      existence

      proof

        set d = the Element of D;

        reconsider F = (the carrier' of C --> ( id d)) as Function of the carrier' of C, the carrier' of D;

        take F;

        thus for c be Element of C holds ex d be Element of D st (F . ( id c)) = ( id d) by FUNCOP_1: 7;

        

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

        thus for f be Element of the carrier' of C holds (F . ( id ( dom f))) = ( id ( dom (F . f))) & (F . ( id ( cod f))) = ( id ( cod (F . f)))

        proof

          let f be Element of the carrier' of C;

          

           A2: (F . f) = ( id d) by FUNCOP_1: 7;

          

          thus (F . ( id ( dom f))) = ( id d) by FUNCOP_1: 7

          .= ( id ( dom (F . f))) by A2;

          

          thus (F . ( id ( cod f))) = ( id d) by FUNCOP_1: 7

          .= ( id ( cod (F . f))) by A2;

        end;

        let f,g be Element of the carrier' of C such that [g, f] in ( dom the Comp of C);

        

        thus (F . (g (*) f)) = (( id d) * ( id d)) by FUNCOP_1: 7

        .= (( id d) (*) ( id d)) by A1, Def11

        .= (( id d) (*) (F . f)) by FUNCOP_1: 7

        .= ((F . g) (*) (F . f)) by FUNCOP_1: 7;

      end;

    end

    theorem :: CAT_1:61

    

     Th56: for T be Function of the carrier' of C, the carrier' of D st (for c be Object of C holds ex d be Object of D st (T . ( id c)) = ( id d)) & (for f be Morphism of C holds (T . ( id ( dom f))) = ( id ( dom (T . f))) & (T . ( id ( cod f))) = ( id ( cod (T . f)))) & (for f,g be Morphism of C st ( dom g) = ( cod f) holds (T . (g (*) f)) = ((T . g) (*) (T . f))) holds T is Functor of C, D

    proof

      let T be Function of the carrier' of C, the carrier' of D such that

       A1: for c be Object of C holds ex d be Object of D st (T . ( id c)) = ( id d) and

       A2: for f be Morphism of C holds (T . ( id ( dom f))) = ( id ( dom (T . f))) & (T . ( id ( cod f))) = ( id ( cod (T . f))) and

       A3: for f,g be Morphism of C st ( dom g) = ( cod f) holds (T . (g (*) f)) = ((T . g) (*) (T . f));

      thus for c be Element of C holds ex d be Element of D st (T . ( id c)) = ( id d) by A1;

      thus for f be Element of the carrier' of C holds (T . ( id ( dom f))) = ( id ( dom (T . f))) & (T . ( id ( cod f))) = ( id ( cod (T . f))) by A2;

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

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

      then

       A4: ( dom g) = ( cod f) by Def4;

      thus thesis by A3, A4;

    end;

    theorem :: CAT_1:62

    for T be Functor of C, D holds for c be Object of C holds ex d be Object of D st (T . ( id c)) = ( id d) by Def19;

    theorem :: CAT_1:63

    for T be Functor of C, D holds for f be Morphism of C holds (T . ( id ( dom f))) = ( id ( dom (T . f))) & (T . ( id ( cod f))) = ( id ( cod (T . f))) by Def19;

    theorem :: CAT_1:64

    

     Th59: for T be Functor of C, D holds for f,g be Morphism of C st ( dom g) = ( cod f) holds ( dom (T . g)) = ( cod (T . f)) & (T . (g (*) f)) = ((T . g) (*) (T . f))

    proof

      let T be Functor of C, D;

      let f,g be Morphism of C;

      assume

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

      then

       A2: (the Comp of C . (g,f)) = (g (*) f) & [g, f] in ( dom the Comp of C) by Def4, Th14;

      ( id ( dom (T . g))) = (T . ( id ( cod f))) by A1, Def19

      .= ( id ( cod (T . f))) by Def19;

      hence ( dom (T . g)) = ( cod (T . f)) by Th54;

      thus thesis by A2, Def19;

    end;

    theorem :: CAT_1:65

    

     Th60: for T be Function of the carrier' of C, the carrier' of D holds for F be Function of the carrier of C, the carrier of D st (for c be Object of C holds (T . ( id c)) = ( id (F . c))) & (for f be Morphism of C holds (F . ( dom f)) = ( dom (T . f)) & (F . ( cod f)) = ( cod (T . f))) & (for f,g be Morphism of C st ( dom g) = ( cod f) holds (T . (g (*) f)) = ((T . g) (*) (T . f))) holds T is Functor of C, D

    proof

      let T be Function of the carrier' of C, the carrier' of D;

      let F be Function of the carrier of C, the carrier of D;

      assume that

       A1: for c be Object of C holds (T . ( id c)) = ( id (F . c)) and

       A2: for f be Morphism of C holds (F . ( dom f)) = ( dom (T . f)) & (F . ( cod f)) = ( cod (T . f)) and

       A3: for f,g be Morphism of C st ( dom g) = ( cod f) holds (T . (g (*) f)) = ((T . g) (*) (T . f));

      

       A4: for c be Object of C holds ex d be Object of D st (T . ( id c)) = ( id d)

      proof

        let c be Object of C;

        take (F . c);

        thus thesis by A1;

      end;

      for f be Morphism of C holds (T . ( id ( dom f))) = ( id ( dom (T . f))) & (T . ( id ( cod f))) = ( id ( cod (T . f)))

      proof

        let f be Morphism of C;

        

        thus (T . ( id ( dom f))) = ( id (F . ( dom f))) by A1

        .= ( id ( dom (T . f))) by A2;

        

        thus (T . ( id ( cod f))) = ( id (F . ( cod f))) by A1

        .= ( id ( cod (T . f))) by A2;

      end;

      hence thesis by A3, A4, Th56;

    end;

    definition

      let C, D;

      let F be Function of the carrier' of C, the carrier' of D;

      assume

       A1: for c be Element of C holds ex d be Element of D st (F . ( id c)) = ( id d);

      :: CAT_1:def22

      func Obj (F) -> Function of the carrier of C, the carrier of D means

      : Def20: for c be Element of C holds for d be Element of D st (F . ( id c)) = ( id d) holds (it . c) = d;

      existence

      proof

        defpred P[ Object of C, Object of D] means for d be Element of D st (F . ( id $1)) = ( id d) holds $2 = d;

        

         A2: for c be Element of C holds ex y be Element of D st P[c, y]

        proof

          let c be Element of C;

          consider y be Element of D such that

           A3: (F . ( id c)) = ( id y) by A1;

          take y;

          let d be Element of D;

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

          hence thesis by A3, Th54;

        end;

        thus ex f be Function of the carrier of C, the carrier of D st for x be Element of C holds P[x, (f . x)] from FUNCT_2:sch 3( A2);

      end;

      uniqueness

      proof

        let F1,F2 be Function of the carrier of C, the carrier of D such that

         A4: for c be Element of C holds for d be Element of D st (F . ( id c)) = ( id d) holds (F1 . c) = d and

         A5: for c be Element of C holds for d be Element of D st (F . ( id c)) = ( id d) holds (F2 . c) = d;

        for c be Element of C holds (F1 . c) = (F2 . c)

        proof

          let c be Element of C;

          consider d1 be Element of D such that

           A6: (F . ( id c)) = ( id d1) by A1;

          (F1 . c) = d1 by A4, A6;

          hence thesis by A5, A6;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: CAT_1:66

    for T be Function of the carrier' of C, the carrier' of D st for c be Object of C holds ex d be Object of D st (T . ( id c)) = ( id d) holds for c be Object of C holds for d be Object of D st (T . ( id c)) = ( id d) holds (( Obj T) . c) = d by Def20;

    theorem :: CAT_1:67

    

     Th62: for T be Functor of C, D holds for c be Object of C holds for d be Object of D st (T . ( id c)) = ( id d) holds (( Obj T) . c) = d

    proof

      let T be Functor of C, D;

      for c be Object of C holds ex d be Object of D st (T . ( id c)) = ( id d) by Def19;

      hence thesis by Def20;

    end;

    theorem :: CAT_1:68

    

     Th63: for T be Functor of C, D, c be Object of C holds (T . ( id c)) = ( id (( Obj T) . c))

    proof

      let T be Functor of C, D, c be Object of C;

      ex d be Object of D st (T . ( id c)) = ( id d) by Def19;

      hence thesis by Th62;

    end;

    theorem :: CAT_1:69

    

     Th64: for T be Functor of C, D, f be Morphism of C holds (( Obj T) . ( dom f)) = ( dom (T . f)) & (( Obj T) . ( cod f)) = ( cod (T . f))

    proof

      let T be Functor of C, D, f be Morphism of C;

      (T . ( id ( dom f))) = ( id ( dom (T . f))) & (T . ( id ( cod f))) = ( id ( cod (T . f))) by Def19;

      hence thesis by Th62;

    end;

    definition

      let C,D be Category;

      let T be Functor of C, D;

      let c be Object of C;

      :: CAT_1:def23

      func T . c -> Object of D equals (( Obj T) . c);

      correctness ;

    end

    theorem :: CAT_1:70

    for T be Functor of C, D holds for c be Object of C holds for d be Object of D st (T . ( id c)) = ( id d) holds (T . c) = d by Th62;

    theorem :: CAT_1:71

    for T be Functor of C, D, c be Object of C holds (T . ( id c)) = ( id (T . c)) by Th63;

    theorem :: CAT_1:72

    for T be Functor of C, D, f be Morphism of C holds (T . ( dom f)) = ( dom (T . f)) & (T . ( cod f)) = ( cod (T . f)) by Th64;

    theorem :: CAT_1:73

    

     Th68: for T be Functor of B, C holds for S be Functor of C, D holds (S * T) is Functor of B, D

    proof

      let T be Functor of B, C;

      let S be Functor of C, D;

      reconsider FF = (( Obj S) * ( Obj T)) as Function of the carrier of B, the carrier of D;

      reconsider TT = (S * T) as Function of the carrier' of B, the carrier' of D;

      now

        thus for b be Object of B holds (TT . ( id b)) = ( id (FF . b))

        proof

          let b be Object of B;

          

          thus (TT . ( id b)) = (S . (T . ( id b))) by FUNCT_2: 15

          .= (S . ( id (T . b))) by Th63

          .= ( id (S . (( Obj T) . b))) by Th63

          .= ( id (FF . b)) by FUNCT_2: 15;

        end;

        thus for f be Morphism of B holds (FF . ( dom f)) = ( dom (TT . f)) & (FF . ( cod f)) = ( cod (TT . f))

        proof

          let f be Morphism of B;

          

          thus (FF . ( dom f)) = (( Obj S) . (( Obj T) . ( dom f))) by FUNCT_2: 15

          .= (( Obj S) . ( dom (T . f))) by Th64

          .= ( dom (S . (T . f))) by Th64

          .= ( dom (TT . f)) by FUNCT_2: 15;

          

          thus (FF . ( cod f)) = (( Obj S) . (( Obj T) . ( cod f))) by FUNCT_2: 15

          .= (( Obj S) . ( cod (T . f))) by Th64

          .= ( cod (S . (T . f))) by Th64

          .= ( cod (TT . f)) by FUNCT_2: 15;

        end;

        let f,g be Morphism of B;

        assume

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

        then

         A2: ( dom (T . g)) = ( cod (T . f)) by Th59;

        

        thus (TT . (g (*) f)) = (S . (T . (g (*) f))) by FUNCT_2: 15

        .= (S . ((T . g) (*) (T . f))) by A1, Th59

        .= ((S . (T . g)) (*) (S . (T . f))) by A2, Th59

        .= ((TT . g) (*) (S . (T . f))) by FUNCT_2: 15

        .= ((TT . g) (*) (TT . f)) by FUNCT_2: 15;

      end;

      hence thesis by Th60;

    end;

    definition

      let B, C, D;

      let T be Functor of B, C;

      let S be Functor of C, D;

      :: original: *

      redefine

      func S * T -> Functor of B, D ;

      coherence by Th68;

    end

    theorem :: CAT_1:74

    

     Th69: ( id the carrier' of C) is Functor of C, C

    proof

      set F = ( id the carrier of C);

      set T = ( id the carrier' of C);

      (for c be Object of C holds (T . ( id c)) = ( id (F . c))) & (for f be Morphism of C holds (F . ( dom f)) = ( dom (T . f)) & (F . ( cod f)) = ( cod (T . f))) & for f,g be Morphism of C st ( dom g) = ( cod f) holds (T . (g (*) f)) = ((T . g) (*) (T . f));

      hence thesis by Th60;

    end;

    theorem :: CAT_1:75

    

     Th70: for T be Functor of B, C, S be Functor of C, D, b be Object of B holds (( Obj (S * T)) . b) = (( Obj S) . (( Obj T) . b))

    proof

      let T be Functor of B, C, S be Functor of C, D, b be Object of B;

      

       A1: ((S * T) . ( id b)) = (S . (T . ( id b))) by FUNCT_2: 15;

      consider d be Object of D such that

       A2: ((S * T) . ( id b)) = ( id d) by Def19;

      consider c be Object of C such that

       A3: (T . ( id b)) = ( id c) by Def19;

      

      thus (( Obj (S * T)) . b) = d by A2, Th62

      .= (( Obj S) . c) by A2, A3, A1, Th62

      .= (( Obj S) . (( Obj T) . b)) by A3, Th62;

    end;

    theorem :: CAT_1:76

    for T be Functor of B, C holds for S be Functor of C, D holds for b be Object of B holds ((S * T) . b) = (S . (T . b)) by Th70;

    definition

      let C;

      :: CAT_1:def24

      func id C -> Functor of C, C equals ( id the carrier' of C);

      coherence by Th69;

    end

    theorem :: CAT_1:77

    

     Th72: for c be Object of C holds (( Obj ( id C)) . c) = c

    proof

      let c be Object of C;

      (( id C) . ( id c)) = ( id c);

      hence thesis by Th62;

    end;

    theorem :: CAT_1:78

    

     Th73: ( Obj ( id C)) = ( id the carrier of C)

    proof

      ( dom ( Obj ( id C))) = the carrier of C & for x be object holds x in the carrier of C implies (( Obj ( id C)) . x) = x by Th72, FUNCT_2:def 1;

      hence thesis by FUNCT_1: 17;

    end;

    theorem :: CAT_1:79

    for c be Object of C holds (( id C) . c) = c by Th72;

    definition

      let C,D be Category;

      let T be Functor of C, D;

      :: CAT_1:def25

      attr T is isomorphic means T is one-to-one & ( rng T) = the carrier' of D & ( rng ( Obj T)) = the carrier of D;

      :: CAT_1:def26

      attr T is full means for c,c9 be Object of C st ( Hom ((T . c),(T . c9))) <> {} holds for g be Morphism of (T . c), (T . c9) holds ( Hom (c,c9)) <> {} & ex f be Morphism of c, c9 st g = (T . f);

      :: CAT_1:def27

      attr T is faithful means for c,c9 be Object of C st ( Hom (c,c9)) <> {} holds for f1,f2 be Morphism of c, c9 holds (T . f1) = (T . f2) implies f1 = f2;

    end

    theorem :: CAT_1:80

    ( id C) is isomorphic

    proof

      ( rng ( id the carrier of C)) = the carrier of C;

      hence ( id C) is one-to-one & ( rng ( id C)) = the carrier' of C & ( rng ( Obj ( id C))) = the carrier of C by Th73;

    end;

    theorem :: CAT_1:81

    

     Th76: for T be Functor of C, D holds for c,c9 be Object of C holds for f be set st f in ( Hom (c,c9)) holds (T . f) in ( Hom ((T . c),(T . c9)))

    proof

      let T be Functor of C, D;

      let c,c9 be Object of C;

      let f be set;

      assume

       A1: f in ( Hom (c,c9));

      then

      reconsider f9 = f as Morphism of c, c9 by Def3;

      ( cod f9) = c9 by A1, Th1;

      then

       A2: (T . c9) = ( cod (T . f9)) by Th64;

      ( dom f9) = c by A1, Th1;

      then (T . c) = ( dom (T . f9)) by Th64;

      hence thesis by A2;

    end;

    theorem :: CAT_1:82

    

     Th77: for T be Functor of C, D holds for c,c9 be Object of C st ( Hom (c,c9)) <> {} holds for f be Morphism of c, c9 holds (T . f) in ( Hom ((T . c),(T . c9)))

    proof

      let T be Functor of C, D;

      let c,c9 be Object of C such that

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

      let f be Morphism of c, c9;

      f in ( Hom (c,c9)) by A1, Def3;

      hence thesis by Th76;

    end;

    theorem :: CAT_1:83

    

     Th78: for T be Functor of C, D holds for c,c9 be Object of C st ( Hom (c,c9)) <> {} holds for f be Morphism of c, c9 holds (T . f) is Morphism of (T . c), (T . c9)

    proof

      let T be Functor of C, D;

      let c,c9 be Object of C such that

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

      let f be Morphism of c, c9;

      (T . f) in ( Hom ((T . c),(T . c9))) by A1, Th77;

      hence thesis by Def3;

    end;

    theorem :: CAT_1:84

    

     Th79: for T be Functor of C, D holds for c,c9 be Object of C st ( Hom (c,c9)) <> {} holds ( Hom ((T . c),(T . c9))) <> {}

    proof

      let T be Functor of C, D;

      let c,c9 be Object of C;

      set f = the Element of ( Hom (c,c9));

      assume ( Hom (c,c9)) <> {} ;

      then f in ( Hom (c,c9));

      hence thesis by Th76;

    end;

    theorem :: CAT_1:85

    for T be Functor of B, C holds for S be Functor of C, D st T is full & S is full holds (S * T) is full

    proof

      let T be Functor of B, C;

      let S be Functor of C, D;

      assume that

       A1: T is full and

       A2: S is full;

      let b,b9 be Object of B such that

       A3: ( Hom (((S * T) . b),((S * T) . b9))) <> {} ;

      let g be Morphism of ((S * T) . b), ((S * T) . b9);

      

       A4: ((S * T) . b) = (S . (T . b)) & ((S * T) . b9) = (S . (T . b9)) by Th70;

      then

      consider f be Morphism of (T . b), (T . b9) such that

       A5: g = (S . f) by A2, A3;

      

       A6: ( Hom ((T . b),(T . b9))) <> {} by A2, A3, A4;

      hence ( Hom (b,b9)) <> {} by A1;

      consider h be Morphism of b, b9 such that

       A7: f = (T . h) by A1, A6;

      take h;

      thus thesis by A5, A7, FUNCT_2: 15;

    end;

    theorem :: CAT_1:86

    for T be Functor of B, C holds for S be Functor of C, D st T is faithful & S is faithful holds (S * T) is faithful

    proof

      let T be Functor of B, C;

      let S be Functor of C, D;

      assume that

       A1: T is faithful and

       A2: S is faithful;

      let b,b9 be Object of B such that

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

      let f1,f2 be Morphism of b, b9;

      

       A4: (T . f2) is Morphism of (T . b), (T . b9) by A3, Th78;

      assume

       A5: ((S * T) . f1) = ((S * T) . f2);

      

       A6: ((S * T) . f1) = (S . (T . f1)) & ((S * T) . f2) = (S . (T . f2)) by FUNCT_2: 15;

      ( Hom ((T . b),(T . b9))) <> {} & (T . f1) is Morphism of (T . b), (T . b9) by A3, Th78, Th79;

      then (T . f1) = (T . f2) by A2, A5, A6, A4;

      hence thesis by A1, A3;

    end;

    theorem :: CAT_1:87

    

     Th82: for T be Functor of C, D holds for c,c9 be Object of C holds (T .: ( Hom (c,c9))) c= ( Hom ((T . c),(T . c9)))

    proof

      let T be Functor of C, D;

      let c,c9 be Object of C;

      let f be object;

      assume f in (T .: ( Hom (c,c9)));

      then ex g be Element of the carrier' of C st g in ( Hom (c,c9)) & f = (T . g) by FUNCT_2: 65;

      hence thesis by Th76;

    end;

    definition

      let C,D be Category;

      let T be Functor of C, D;

      let c,c9 be Object of C;

      :: CAT_1:def28

      func hom (T,c,c9) -> Function of ( Hom (c,c9)), ( Hom ((T . c),(T . c9))) equals (T | ( Hom (c,c9)));

      correctness

      proof

        (T .: ( Hom (c,c9))) c= ( Hom ((T . c),(T . c9))) by Th82;

        hence thesis by FUNCT_2: 101;

      end;

    end

    theorem :: CAT_1:88

    

     Th83: for T be Functor of C, D holds for c,c9 be Object of C st ( Hom (c,c9)) <> {} holds for f be Morphism of c, c9 holds (( hom (T,c,c9)) . f) = (T . f)

    proof

      let T be Functor of C, D;

      let c,c9 be Object of C;

      assume

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

      let f be Morphism of c, c9;

      f in ( Hom (c,c9)) by A1, Def3;

      hence thesis by FUNCT_1: 49;

    end;

    theorem :: CAT_1:89

    for T be Functor of C, D holds T is full iff for c,c9 be Object of C holds ( rng ( hom (T,c,c9))) = ( Hom ((T . c),(T . c9)))

    proof

      let T be Functor of C, D;

      thus T is full implies for c,c9 be Object of C holds ( rng ( hom (T,c,c9))) = ( Hom ((T . c),(T . c9)))

      proof

        assume

         A1: T is full;

        let c,c9 be Object of C;

        now

          assume

           A2: ( Hom ((T . c),(T . c9))) <> {} ;

          for g be object holds g in ( rng ( hom (T,c,c9))) iff g in ( Hom ((T . c),(T . c9)))

          proof

            let g be object;

            thus g in ( rng ( hom (T,c,c9))) implies g in ( Hom ((T . c),(T . c9)))

            proof

              assume g in ( rng ( hom (T,c,c9)));

              then

              consider f be object such that

               A3: f in ( dom ( hom (T,c,c9))) and

               A4: (( hom (T,c,c9)) . f) = g by FUNCT_1:def 3;

              f in ( Hom (c,c9)) by A2, A3, FUNCT_2:def 1;

              hence thesis by A2, A4, FUNCT_2: 5;

            end;

            assume g in ( Hom ((T . c),(T . c9)));

            then g is Morphism of (T . c), (T . c9) by Def3;

            then

            consider f be Morphism of c, c9 such that

             A5: g = (T . f) by A1, A2;

            ( Hom (c,c9)) <> {} by A1, A2;

            then f in ( Hom (c,c9)) by Def3;

            then (( hom (T,c,c9)) . f) in ( rng ( hom (T,c,c9))) by A2, FUNCT_2: 4;

            hence thesis by A5, A1, A2, Th83;

          end;

          hence thesis by TARSKI: 2;

        end;

        hence thesis;

      end;

      assume

       A6: for c,c9 be Object of C holds ( rng ( hom (T,c,c9))) = ( Hom ((T . c),(T . c9)));

      let c,c9 be Object of C such that

       A7: ( Hom ((T . c),(T . c9))) <> {} ;

      let g be Morphism of (T . c), (T . c9);

      g in ( Hom ((T . c),(T . c9))) by A7, Def3;

      then g in ( rng ( hom (T,c,c9))) by A6;

      then

      consider f be object such that

       A8: f in ( dom ( hom (T,c,c9))) and

       A9: (( hom (T,c,c9)) . f) = g by FUNCT_1:def 3;

      thus ( Hom (c,c9)) <> {} by A8;

      

       A10: f in ( Hom (c,c9)) by A7, A8, FUNCT_2:def 1;

      then

      reconsider f as Morphism of c, c9 by Def3;

      take f;

      thus thesis by A9, A10, Th83;

    end;

    theorem :: CAT_1:90

    for T be Functor of C, D holds T is faithful iff for c,c9 be Object of C holds ( hom (T,c,c9)) is one-to-one

    proof

      let T be Functor of C, D;

      thus T is faithful implies for c,c9 be Object of C holds ( hom (T,c,c9)) is one-to-one

      proof

        assume

         A1: T is faithful;

        let c,c9 be Object of C;

        now

           A2:

          now

            let f1,f2 be object;

            assume that

             A3: f1 in ( Hom (c,c9)) and

             A4: f2 in ( Hom (c,c9));

            

             A5: f2 is Morphism of c, c9 by A4, Def3;

            then

             A6: (T . f2) = (( hom (T,c,c9)) . f2) by A3, Th83;

            

             A7: f1 is Morphism of c, c9 by A3, Def3;

            then (T . f1) = (( hom (T,c,c9)) . f1) by A3, Th83;

            hence (( hom (T,c,c9)) . f1) = (( hom (T,c,c9)) . f2) implies f1 = f2 by A1, A3, A7, A5, A6;

          end;

          assume ( Hom ((T . c),(T . c9))) <> {} ;

          hence thesis by A2, FUNCT_2: 19;

        end;

        hence thesis;

      end;

      assume

       A8: for c,c9 be Object of C holds ( hom (T,c,c9)) is one-to-one;

      let c,c9 be Object of C such that

       A9: ( Hom (c,c9)) <> {} ;

      let f1,f2 be Morphism of c, c9;

      

       A10: (T . f2) = (( hom (T,c,c9)) . f2) by A9, Th83;

      

       A11: f2 in ( Hom (c,c9)) & (T . f1) = (( hom (T,c,c9)) . f1) by A9, Def3, Th83;

      

       A12: ( hom (T,c,c9)) is one-to-one by A8;

      ( Hom ((T . c),(T . c9))) <> {} & f1 in ( Hom (c,c9)) by A9, Def3, Th79;

      hence thesis by A12, A11, A10, FUNCT_2: 19;

    end;

    theorem :: CAT_1:91

    for a,b be Element of C st ( Hom (a,b)) <> {} holds ex m be Morphism of a, b st m in ( Hom (a,b))

    proof

      let a,b be Element of C;

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

      then

      consider m be object such that

       A1: m in ( Hom (a,b)) by XBOOLE_0:def 1;

      reconsider m as Morphism of a, b by A1, Def3;

      take m;

      thus thesis by A1;

    end;

    theorem :: CAT_1:92

    the carrier' of C = ( union the set of all ( Hom (a,b)))

    proof

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

      thus the carrier' of C c= M

      proof

        let e be object;

        assume e in the carrier' of C;

        then

        reconsider e as Morphism of C;

        

         A1: e in ( Hom (( dom e),( cod e)));

        ( Hom (( dom e),( cod e))) in A;

        hence thesis by A1, TARSKI:def 4;

      end;

      let e be object;

      assume e in M;

      then

      consider X be set such that

       A2: e in X and

       A3: X in A by TARSKI:def 4;

      ex a, b st X = ( Hom (a,b)) by A3;

      hence thesis by A2;

    end;