commacat.miz



    begin

    deffunc obj( CatStr) = the carrier of $1;

    deffunc morph( CatStr) = the carrier' of $1;

    reserve y for set;

    reserve C,D,E for Category,

c,c1,c2 for Object of C,

d,d1 for Object of D,

x for set,

f,f1 for Morphism of E,

g,g1 for Morphism of C,

h,h1 for Morphism of D,

F for Functor of C, E,

G for Functor of D, E;

    definition

      let C, D, E;

      let F be Functor of C, E, G be Functor of D, E;

      given c1, d1, f1 such that

       A1: f1 in ( Hom ((F . c1),(G . d1)));

      :: COMMACAT:def1

      func commaObjs (F,G) -> non empty Subset of [: [:the carrier of C, the carrier of D:], the carrier' of E:] equals

      : Def1: { [ [c, d], f] : f in ( Hom ((F . c),(G . d))) };

      coherence

      proof

        

         A2: { [ [c, d], f] : f in ( Hom ((F . c),(G . d))) } c= [: [:the carrier of C, the carrier of D:], the carrier' of E:]

        proof

          let x be object;

          assume x in { [ [c, d], f] : f in ( Hom ((F . c),(G . d))) };

          then ex c, d, f st x = [ [c, d], f] & f in ( Hom ((F . c),(G . d)));

          hence thesis;

        end;

         [ [c1, d1], f1] in { [ [c, d], f] : f in ( Hom ((F . c),(G . d))) } by A1;

        hence thesis by A2;

      end;

    end

    reserve o,o1,o2 for Element of ( commaObjs (F,G));

    theorem :: COMMACAT:1

    

     Th1: (ex c, d, f st f in ( Hom ((F . c),(G . d)))) implies o = [ [(o `11 ), (o `12 )], (o `2 )] & (o `2 ) in ( Hom ((F . (o `11 )),(G . (o `12 )))) & ( dom (o `2 )) = (F . (o `11 )) & ( cod (o `2 )) = (G . (o `12 ))

    proof

      assume ex c, d, f st f in ( Hom ((F . c),(G . d)));

      then

       A1: ( commaObjs (F,G)) = { [ [c, d], f] : f in ( Hom ((F . c),(G . d))) } by Def1;

      o in ( commaObjs (F,G));

      then

      consider c, d, f such that

       A2: o = [ [c, d], f] and

       A3: f in ( Hom ((F . c),(G . d))) by A1;

      (o `11 ) = c & (o `12 ) = d by A2, MCART_1: 85;

      hence thesis by A2, A3, CAT_1: 1;

    end;

    definition

      let C, D, E, F, G;

      given c1, d1, f1 such that

       A1: f1 in ( Hom ((F . c1),(G . d1)));

      :: COMMACAT:def2

      func commaMorphs (F,G) -> non empty Subset of [: [:( commaObjs (F,G)), ( commaObjs (F,G)):], [:the carrier' of C, the carrier' of D:]:] equals

      : Def2: { [ [o1, o2], [g, h]] : ( dom g) = (o1 `11 ) & ( cod g) = (o2 `11 ) & ( dom h) = (o1 `12 ) & ( cod h) = (o2 `12 ) & ((o2 `2 ) (*) (F . g)) = ((G . h) (*) (o1 `2 )) };

      coherence

      proof

        ( commaObjs (F,G)) = { [ [c, d], f] : f in ( Hom ((F . c),(G . d))) } by A1, Def1;

        then [ [c1, d1], f1] in ( commaObjs (F,G)) by A1;

        then

        reconsider o = [ [c1, d1], f1] as Element of ( commaObjs (F,G));

        set X = { [ [o1, o2], [g, h]] : ( dom g) = (o1 `11 ) & ( cod g) = (o2 `11 ) & ( dom h) = (o1 `12 ) & ( cod h) = (o2 `12 ) & ((o2 `2 ) (*) (F . g)) = ((G . h) (*) (o1 `2 )) };

        

         A2: ( dom ( id d1)) = d1 & ( cod ( id d1)) = d1;

        

         A3: ((o `1 ) `1 ) = (o `11 ) & ((o `1 ) `2 ) = (o `12 ) by MCART_1:def 14, MCART_1:def 15;

        

         A4: X c= [: [:( commaObjs (F,G)), ( commaObjs (F,G)):], [:the carrier' of C, the carrier' of D:]:]

        proof

          let x be object;

          assume x in X;

          then ex g, h, o1, o2 st x = [ [o1, o2], [g, h]] & ( dom g) = (o1 `11 ) & ( cod g) = (o2 `11 ) & ( dom h) = (o1 `12 ) & ( cod h) = (o2 `12 ) & ((o2 `2 ) (*) (F . g)) = ((G . h) (*) (o1 `2 ));

          hence thesis;

        end;

        

         A5: ( [c1, d1] `2 ) = d1 & (o `2 ) = f1;

        ( cod f1) = (G . d1) by A1, CAT_1: 1;

        then

         A6: (( id (G . d1)) (*) f1) = f1 by CAT_1: 21;

        ( dom f1) = (F . c1) by A1, CAT_1: 1;

        then

         A7: (f1 (*) ( id (F . c1))) = f1 by CAT_1: 22;

        

         A8: (F . ( id c1)) = ( id (F . c1)) & (G . ( id d1)) = ( id (G . d1)) by CAT_1: 71;

        ( dom ( id c1)) = c1 & ( cod ( id c1)) = c1;

        then [ [o, o], [( id c1), ( id d1)]] in X by A2, A3, A5, A7, A6, A8;

        hence thesis by A4;

      end;

    end

    reserve k,k1,k2,k9 for Element of ( commaMorphs (F,G));

    definition

      let C, D, E, F, G, k;

      :: original: `11

      redefine

      func k `11 -> Element of ( commaObjs (F,G)) ;

      coherence

      proof

        thus (k `11 ) is Element of ( commaObjs (F,G));

      end;

      :: original: `12

      redefine

      func k `12 -> Element of ( commaObjs (F,G)) ;

      coherence

      proof

        thus (k `12 ) is Element of ( commaObjs (F,G));

      end;

    end

    theorem :: COMMACAT:2

    

     Th2: (ex c, d, f st f in ( Hom ((F . c),(G . d)))) implies k = [ [(k `11 ), (k `12 )], [(k `21 ), (k `22 )]] & ( dom (k `21 )) = ((k `11 ) `11 ) & ( cod (k `21 )) = ((k `12 ) `11 ) & ( dom (k `22 )) = ((k `11 ) `12 ) & ( cod (k `22 )) = ((k `12 ) `12 ) & (((k `12 ) `2 ) (*) (F . (k `21 ))) = ((G . (k `22 )) (*) ((k `11 ) `2 ))

    proof

      assume ex c, d, f st f in ( Hom ((F . c),(G . d)));

      then

       A1: ( commaMorphs (F,G)) = { [ [o1, o2], [g, h]] : ( dom g) = (o1 `11 ) & ( cod g) = (o2 `11 ) & ( dom h) = (o1 `12 ) & ( cod h) = (o2 `12 ) & ((o2 `2 ) (*) (F . g)) = ((G . h) (*) (o1 `2 )) } by Def2;

      k in ( commaMorphs (F,G));

      then

      consider g, h, o1, o2 such that

       A2: k = [ [o1, o2], [g, h]] and

       A3: ( dom g) = (o1 `11 ) & ( cod g) = (o2 `11 ) & ( dom h) = (o1 `12 ) & ( cod h) = (o2 `12 ) & ((o2 `2 ) (*) (F . g)) = ((G . h) (*) (o1 `2 )) by A1;

      

       A4: (k `21 ) = g by A2, MCART_1: 85;

      (k `11 ) = o1 & (k `12 ) = o2 by A2, MCART_1: 85;

      hence thesis by A2, A3, A4, MCART_1: 85;

    end;

    definition

      let C, D, E, F, G, k1, k2;

      given c1, d1, f1 such that

       A1: f1 in ( Hom ((F . c1),(G . d1)));

      assume

       A2: (k1 `12 ) = (k2 `11 );

      :: COMMACAT:def3

      func k2 * k1 -> Element of ( commaMorphs (F,G)) equals

      : Def3: [ [(k1 `11 ), (k2 `12 )], [((k2 `21 ) (*) (k1 `21 )), ((k2 `22 ) (*) (k1 `22 ))]];

      coherence

      proof

        set k22 = ((k2 `22 ) (*) (k1 `22 ));

        set k21 = ((k2 `21 ) (*) (k1 `21 ));

        

         A3: (F . ( cod (k2 `21 ))) = ( cod (F . (k2 `21 ))) & ( dom (F . (k2 `21 ))) = (F . ( dom (k2 `21 ))) by CAT_1: 72;

        

         A4: ( cod (F . (k1 `21 ))) = (F . ( cod (k1 `21 ))) by CAT_1: 72;

        

         A5: ( cod ((k1 `12 ) `2 )) = (G . ((k1 `12 ) `12 )) by A1, Th1;

        

         A6: ( dom (k1 `22 )) = ((k1 `11 ) `12 ) by A1, Th2;

        

         A7: (((k2 `12 ) `2 ) (*) (F . (k2 `21 ))) = ((G . (k2 `22 )) (*) ((k2 `11 ) `2 )) & ( dom ((k2 `12 ) `2 )) = (F . ((k2 `12 ) `11 )) by A1, Th1, Th2;

        

         A8: ( cod (G . (k1 `22 ))) = (G . ( cod (k1 `22 ))) by CAT_1: 72;

        

         A9: (((k1 `12 ) `2 ) (*) (F . (k1 `21 ))) = ((G . (k1 `22 )) (*) ((k1 `11 ) `2 )) & ( dom ((k1 `12 ) `2 )) = (F . ((k1 `12 ) `11 )) by A1, Th1, Th2;

        

         A10: ( dom (G . (k2 `22 ))) = (G . ( dom (k2 `22 ))) by CAT_1: 72;

        

         A11: ( cod ((k1 `11 ) `2 )) = (G . ((k1 `11 ) `12 )) & ( dom (G . (k1 `22 ))) = (G . ( dom (k1 `22 ))) by A1, Th1, CAT_1: 72;

        

         A12: ( cod (k2 `21 )) = ((k2 `12 ) `11 ) by A1, Th2;

        

         A13: ( commaMorphs (F,G)) = { [ [o1, o2], [g, h]] : ( dom g) = (o1 `11 ) & ( cod g) = (o2 `11 ) & ( dom h) = (o1 `12 ) & ( cod h) = (o2 `12 ) & ((o2 `2 ) (*) (F . g)) = ((G . h) (*) (o1 `2 )) } by A1, Def2;

        

         A14: ( dom (k2 `22 )) = ((k2 `11 ) `12 ) by A1, Th2;

        

         A15: ( cod (k1 `22 )) = ((k1 `12 ) `12 ) by A1, Th2;

        then

         A16: ( dom k22) = ( dom (k1 `22 )) & ( cod k22) = ( cod (k2 `22 )) by A2, A14, CAT_1: 17;

        

         A17: ( dom (k1 `21 )) = ((k1 `11 ) `11 ) & ( cod (k2 `22 )) = ((k2 `12 ) `12 ) by A1, Th2;

        

         A18: ( cod (k1 `21 )) = ((k1 `12 ) `11 ) by A1, Th2;

        

         A19: ( dom (k2 `21 )) = ((k2 `11 ) `11 ) by A1, Th2;

        then

         A20: ( dom k21) = ( dom (k1 `21 )) & ( cod k21) = ( cod (k2 `21 )) by A2, A18, CAT_1: 17;

        (((k2 `12 ) `2 ) (*) (F . k21)) = (((k2 `12 ) `2 ) (*) ((F . (k2 `21 )) (*) (F . (k1 `21 )))) by A2, A18, A19, CAT_1: 64

        .= (((G . (k2 `22 )) (*) ((k2 `11 ) `2 )) (*) (F . (k1 `21 ))) by A2, A18, A19, A12, A7, A3, A4, CAT_1: 18

        .= ((G . (k2 `22 )) (*) ((G . (k1 `22 )) (*) ((k1 `11 ) `2 ))) by A2, A18, A14, A9, A5, A4, A10, CAT_1: 18

        .= (((G . (k2 `22 )) (*) (G . (k1 `22 ))) (*) ((k1 `11 ) `2 )) by A2, A6, A15, A14, A10, A11, A8, CAT_1: 18

        .= ((G . k22) (*) ((k1 `11 ) `2 )) by A2, A15, A14, CAT_1: 64;

        then [ [(k1 `11 ), (k2 `12 )], [((k2 `21 ) (*) (k1 `21 )), ((k2 `22 ) (*) (k1 `22 ))]] in ( commaMorphs (F,G)) by A6, A12, A17, A13, A20, A16;

        hence thesis;

      end;

    end

    definition

      let C, D, E, F, G;

      :: COMMACAT:def4

      func commaComp (F,G) -> PartFunc of [:( commaMorphs (F,G)), ( commaMorphs (F,G)):], ( commaMorphs (F,G)) means

      : Def4: ( dom it ) = { [k1, k2] : (k1 `11 ) = (k2 `12 ) } & for k, k9 st [k, k9] in ( dom it ) holds (it . [k, k9]) = (k * k9);

      existence

      proof

        defpred P[ object, object] means ex k1, k2 st $1 = [k1, k2] & $2 = (k1 * k2);

        set X = { [k1, k2] : (k1 `11 ) = (k2 `12 ) };

        

         A1: for x be object st x in X holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in X;

          then

          consider k1, k2 such that

           A2: x = [k1, k2] and (k1 `11 ) = (k2 `12 );

          reconsider y = (k1 * k2) as set;

          take y, k1, k2;

          thus thesis by A2;

        end;

        consider f be Function such that

         A3: ( dom f) = X & for x be object st x in X holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        

         A4: ( rng f) c= ( commaMorphs (F,G))

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A5: y in ( dom f) and

           A6: x = (f . y) by FUNCT_1:def 3;

          ex k1, k2 st y = [k1, k2] & (f . y) = (k1 * k2) by A3, A5;

          hence thesis by A6;

        end;

        ( dom f) c= [:( commaMorphs (F,G)), ( commaMorphs (F,G)):]

        proof

          let x be object;

          assume x in ( dom f);

          then ex k1, k2 st x = [k1, k2] & (k1 `11 ) = (k2 `12 ) by A3;

          hence thesis;

        end;

        then

        reconsider f as PartFunc of [:( commaMorphs (F,G)), ( commaMorphs (F,G)):], ( commaMorphs (F,G)) by A4, RELSET_1: 4;

        take f;

        thus ( dom f) = X by A3;

        let k1, k2;

        assume [k1, k2] in ( dom f);

        then

        consider k, k9 such that

         A7: [k1, k2] = [k, k9] and

         A8: (f . [k1, k2]) = (k * k9) by A3;

        k1 = k by A7, XTUPLE_0: 1;

        hence thesis by A7, A8, XTUPLE_0: 1;

      end;

      uniqueness

      proof

        let f1,f2 be PartFunc of [:( commaMorphs (F,G)), ( commaMorphs (F,G)):], ( commaMorphs (F,G)) such that

         A9: ( dom f1) = { [k1, k2] : (k1 `11 ) = (k2 `12 ) } & for k, k9 st [k, k9] in ( dom f1) holds (f1 . [k, k9]) = (k * k9) and

         A10: ( dom f2) = { [k1, k2] : (k1 `11 ) = (k2 `12 ) } & for k, k9 st [k, k9] in ( dom f2) holds (f2 . [k, k9]) = (k * k9);

        now

          let x be object;

          assume

           A11: x in { [k1, k2] : (k1 `11 ) = (k2 `12 ) };

          then

          consider k1, k2 such that

           A12: x = [k1, k2] and (k1 `11 ) = (k2 `12 );

          

          thus (f1 . x) = (k1 * k2) by A9, A11, A12

          .= (f2 . x) by A10, A11, A12;

        end;

        hence thesis by A9, A10, FUNCT_1: 2;

      end;

    end

    definition

      let C, D, E, F, G;

      given c1, d1, f1 such that

       A1: f1 in ( Hom ((F . c1),(G . d1)));

      :: COMMACAT:def5

      func F comma G -> strict Category means the carrier of it = ( commaObjs (F,G)) & the carrier' of it = ( commaMorphs (F,G)) & (for k holds (the Source of it . k) = (k `11 )) & (for k holds (the Target of it . k) = (k `12 )) & the Comp of it = ( commaComp (F,G));

      existence

      proof

        reconsider O = ( commaObjs (F,G)), M = ( commaMorphs (F,G)) as non empty set;

        defpred P[ Element of ( commaObjs (F,G)), set] means $2 = [ [$1, $1], [( id ($1 `11 )), ( id ($1 `12 ))]];

        deffunc G( Element of ( commaMorphs (F,G))) = ($1 `12 );

        deffunc F( Element of ( commaMorphs (F,G))) = ($1 `11 );

        consider D9 be Function of ( commaMorphs (F,G)), ( commaObjs (F,G)) such that

         A2: (D9 . k) = F(k) from FUNCT_2:sch 4;

        set I = the Function of ( commaObjs (F,G)), ( commaMorphs (F,G));

        reconsider I as Function of O, M;

        reconsider a9 = ( commaComp (F,G)) as PartFunc of [:M, M:], M;

        consider C9 be Function of ( commaMorphs (F,G)), ( commaObjs (F,G)) such that

         A3: (C9 . k) = G(k) from FUNCT_2:sch 4;

        reconsider D9, C9 as Function of M, O;

        set FG = CatStr (# O, M, D9, C9, a9 #);

        

         A4: ( dom the Comp of FG) = { [k1, k2] : (k1 `11 ) = (k2 `12 ) } by Def4;

        

         A5: for f,g be Morphism of FG holds for k1, k2 st f = k1 & g = k2 & ( dom g) = ( cod f) holds (g (*) f) = [ [(k1 `11 ), (k2 `12 )], [((k2 `21 ) (*) (k1 `21 )), ((k2 `22 ) (*) (k1 `22 ))]]

        proof

          let f,g be Morphism of FG;

          let k1, k2;

          assume that

           A6: f = k1 & g = k2 and

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

          

           A8: ( dom g) = (k2 `11 ) & ( cod f) = (k1 `12 ) by A2, A3, A6;

          then

           A9: [k2, k1] in ( dom a9) by A4, A7;

          then

           A10: (a9 . (k2,k1)) = (k2 * k1) by Def4;

          (g (*) f) = (a9 . (g,f)) by A6, A9, CAT_1:def 1;

          hence thesis by A1, A6, A7, A8, A10, Def3;

        end;

        

         A11: for b be Element of FG holds ( Hom (b,b)) <> {}

        proof

          let b be Element of FG;

          reconsider o = b as Element of ( commaObjs (F,G));

          set i = [ [o, o], [( id (o `11 )), ( id (o `12 ))]];

          reconsider g = ( id (o `11 )) as Morphism of C;

          reconsider h = ( id (o `12 )) as Morphism of D;

          

           A12: ( dom g) = (o `11 );

          

           A13: ( cod g) = (o `11 );

          

           A14: ( dom h) = (o `12 );

          

           A15: ( cod h) = (o `12 );

          o in ( commaObjs (F,G));

          then o in { [ [c, d], f] : f in ( Hom ((F . c),(G . d))) } by A1, Def1;

          then

          consider c, d, f such that

           A16: o = [ [c, d], f] and

           A17: f in ( Hom ((F . c),(G . d)));

          

           A18: (F . g) = ( id (F . (o `11 ))) by CAT_1: 71;

          

           A19: (G . h) = ( id (G . (o `12 ))) by CAT_1: 71;

          

           A20: c = (o `11 ) by A16, MCART_1: 85;

          

           A21: d = (o `12 ) by A16, MCART_1: 85;

          

           A22: ( cod (o `2 )) = ( cod f) by A16

          .= (G . d) by A17, CAT_1: 1

          .= (G . (o `12 )) by A21;

          ( dom (o `2 )) = (F . c) by A16, A17, CAT_1: 1

          .= (F . (o `11 )) by A20;

          

          then

           A23: ((o `2 ) (*) (F . g)) = (o `2 ) by A18, CAT_1: 22

          .= ((G . h) (*) (o `2 )) by A19, A22, CAT_1: 21;

          i in { [ [o1, o2], [gg, hh]] where gg be Morphism of C, hh be Morphism of D, o1 be Element of ( commaObjs (F,G)), o2 be Element of ( commaObjs (F,G)) : ( dom gg) = (o1 `11 ) & ( cod gg) = (o2 `11 ) & ( dom hh) = (o1 `12 ) & ( cod hh) = (o2 `12 ) & ((o2 `2 ) (*) (F . gg)) = ((G . hh) (*) (o1 `2 )) } by A12, A13, A14, A15, A23;

          then i in ( commaMorphs (F,G)) by Def2, A1;

          then

          reconsider i as Morphism of FG;

          

           A24: ( cod i) = (C9 . i)

          .= ( [ [o, o], [g, h]] `12 ) by A3

          .= b by MCART_1: 85;

          ( dom i) = (D9 . i)

          .= ( [ [o, o], [g, h]] `11 ) by A2

          .= b by MCART_1: 85;

          then i in ( Hom (b,b)) by A24;

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

        end;

        

         A25: for a be Element of FG holds ex i be Morphism of a, a st for b be Element of FG 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)

        proof

          let a be Element of FG;

          reconsider o = a as Element of ( commaObjs (F,G));

          set i = [ [o, o], [( id (o `11 )), ( id (o `12 ))]];

          reconsider g = ( id (o `11 )) as Morphism of C;

          reconsider h = ( id (o `12 )) as Morphism of D;

          

           A26: ( dom g) = (o `11 );

          

           A27: ( cod g) = (o `11 );

          

           A28: ( dom h) = (o `12 );

          

           A29: ( cod h) = (o `12 );

          o in ( commaObjs (F,G));

          then o in { [ [c, d], f] : f in ( Hom ((F . c),(G . d))) } by A1, Def1;

          then

          consider c, d, f such that

           A30: o = [ [c, d], f] and

           A31: f in ( Hom ((F . c),(G . d)));

          

           A32: (F . g) = ( id (F . (o `11 ))) by CAT_1: 71;

          

           A33: (G . h) = ( id (G . (o `12 ))) by CAT_1: 71;

          

           A34: c = (o `11 ) by A30, MCART_1: 85;

          

           A35: d = (o `12 ) by A30, MCART_1: 85;

          

           A36: ( cod (o `2 )) = ( cod f) by A30

          .= (G . d) by A31, CAT_1: 1

          .= (G . (o `12 )) by A35;

          ( dom (o `2 )) = (F . c) by A30, A31, CAT_1: 1

          .= (F . (o `11 )) by A34;

          

          then

           A37: ((o `2 ) (*) (F . g)) = (o `2 ) by A32, CAT_1: 22

          .= ((G . h) (*) (o `2 )) by A33, A36, CAT_1: 21;

          i in { [ [o1, o2], [gg, hh]] where gg be Morphism of C, hh be Morphism of D, o1 be Element of ( commaObjs (F,G)), o2 be Element of ( commaObjs (F,G)) : ( dom gg) = (o1 `11 ) & ( cod gg) = (o2 `11 ) & ( dom hh) = (o1 `12 ) & ( cod hh) = (o2 `12 ) & ((o2 `2 ) (*) (F . gg)) = ((G . hh) (*) (o1 `2 )) } by A26, A27, A28, A29, A37;

          then i in ( commaMorphs (F,G)) by Def2, A1;

          then

          reconsider i as Morphism of FG;

          

           A38: ( cod i) = (C9 . i)

          .= ( [ [o, o], [g, h]] `12 ) by A3

          .= a by MCART_1: 85;

          ( dom i) = (D9 . i)

          .= ( [ [o, o], [g, h]] `11 ) by A2

          .= a by MCART_1: 85;

          then i in ( Hom (a,a)) by A38;

          then

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

          take i;

          let b be Element of FG;

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

          proof

            assume

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

            let g be Morphism of a, b;

            reconsider gg = g as Element of ( commaMorphs (F,G));

            reconsider ii = i as Element of ( commaMorphs (F,G));

            

             A40: ( commaMorphs (F,G)) = { [ [o1, o2], [g1, h1]] : ( dom g1) = (o1 `11 ) & ( cod g1) = (o2 `11 ) & ( dom h1) = (o1 `12 ) & ( cod h1) = (o2 `12 ) & ((o2 `2 ) (*) (F . g1)) = ((G . h1) (*) (o1 `2 )) } by A1, Def2;

            gg in ( commaMorphs (F,G));

            then

            consider g1, h1, o1, o2 such that

             A41: gg = [ [o1, o2], [g1, h1]] and

             A42: ( dom g1) = (o1 `11 ) and ( cod g1) = (o2 `11 ) and

             A43: ( dom h1) = (o1 `12 ) and ( cod h1) = (o2 `12 ) & ((o2 `2 ) (*) (F . g1)) = ((G . h1) (*) (o1 `2 )) by A40;

            

             A44: ( dom ( commaComp (F,G))) = { [k1, k2] : (k1 `11 ) = (k2 `12 ) } by Def4;

            

             A45: (ii `21 ) = ( [ [o, o], [( id (o `11 )), ( id (o `12 ))]] `21 )

            .= ( id (o `11 )) by MCART_1: 85;

            

             A46: (ii `22 ) = ( [ [o, o], [( id (o `11 )), ( id (o `12 ))]] `22 )

            .= ( id (o `12 )) by MCART_1: 85;

            

             A47: o1 = ( [ [o1, o2], [g1, h1]] `11 ) by MCART_1: 85

            .= (gg `11 ) by A41;

            

             A48: o2 = ( [ [o1, o2], [g1, h1]] `12 ) by MCART_1: 85

            .= (gg `12 ) by A41;

            

             A49: g1 = ( [ [o1, o2], [g1, h1]] `21 ) by MCART_1: 85

            .= (gg `21 ) by A41;

            

             A50: h1 = ( [ [o1, o2], [g1, h1]] `22 ) by MCART_1: 85

            .= (gg `22 ) by A41;

            

             A51: ( dom g) = a by A39, CAT_1: 5;

            

             A52: ( dom g) = (gg `11 ) by A2

            .= ( [ [o1, o2], [g1, h1]] `11 ) by A41

            .= o1 by MCART_1: 85;

            

             A53: o1 = a by A39, A52, CAT_1: 5

            .= [ [c, d], f] by A30;

            

             A54: ( dom (gg `21 )) = ( dom ( [ [o1, o2], [g1, h1]] `21 )) by A41

            .= ( dom g1) by MCART_1: 85

            .= (o1 `11 ) by A42

            .= ( [ [c, d], f] `11 ) by A53

            .= (o `11 ) by A30;

            

             A55: ( dom (gg `22 )) = ( dom ( [ [o1, o2], [g1, h1]] `22 )) by A41

            .= ( dom h1) by MCART_1: 85

            .= (o1 `12 ) by A43

            .= ( [ [c, d], f] `12 ) by A53

            .= (o `12 ) by A30;

            

             A56: (ii `11 ) = ( [ [o, o], [( id (o `11 )), ( id (o `12 ))]] `11 )

            .= ( dom g) by A51, MCART_1: 85

            .= (D9 . gg)

            .= (gg `11 ) by A2;

            

             A57: (ii `11 ) = o by MCART_1: 85

            .= (ii `12 ) by MCART_1: 85;

            then (gg `11 ) = (ii `12 ) by A56;

            then

             A58: [gg, ii] in ( dom ( commaComp (F,G))) by A44;

            

            hence (g (*) i) = (( commaComp (F,G)) . (g,i)) by CAT_1:def 1

            .= (gg * ii) by A58, Def4

            .= [ [(gg `11 ), (gg `12 )], [((gg `21 ) (*) ( id (o `11 ))), ((gg `22 ) (*) (ii `22 ))]] by A1, A57, Def3, A56, A45

            .= [ [(gg `11 ), (gg `12 )], [(gg `21 ), ((gg `22 ) (*) (ii `22 ))]] by A54, CAT_1: 22

            .= [ [(gg `11 ), (gg `12 )], [(gg `21 ), (gg `22 )]] by A46, A55, CAT_1: 22

            .= g by A47, A48, A49, A50, A41;

          end;

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

          proof

            assume

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

            let g be Morphism of b, a;

            reconsider gg = g as Element of ( commaMorphs (F,G));

            reconsider ii = i as Element of ( commaMorphs (F,G));

            

             A60: ( commaMorphs (F,G)) = { [ [o1, o2], [g1, h1]] : ( dom g1) = (o1 `11 ) & ( cod g1) = (o2 `11 ) & ( dom h1) = (o1 `12 ) & ( cod h1) = (o2 `12 ) & ((o2 `2 ) (*) (F . g1)) = ((G . h1) (*) (o1 `2 )) } by A1, Def2;

            gg in ( commaMorphs (F,G));

            then

            consider g1, h1, o1, o2 such that

             A61: gg = [ [o1, o2], [g1, h1]] and ( dom g1) = (o1 `11 ) and

             A62: ( cod g1) = (o2 `11 ) and ( dom h1) = (o1 `12 ) and

             A63: ( cod h1) = (o2 `12 ) and ((o2 `2 ) (*) (F . g1)) = ((G . h1) (*) (o1 `2 )) by A60;

            

             A64: ( dom ( commaComp (F,G))) = { [k1, k2] : (k1 `11 ) = (k2 `12 ) } by Def4;

            

             A65: (ii `21 ) = ( [ [o, o], [( id (o `11 )), ( id (o `12 ))]] `21 )

            .= ( id (o `11 )) by MCART_1: 85;

            

             A66: (ii `22 ) = ( [ [o, o], [( id (o `11 )), ( id (o `12 ))]] `22 )

            .= ( id (o `12 )) by MCART_1: 85;

            

             A67: o1 = ( [ [o1, o2], [g1, h1]] `11 ) by MCART_1: 85

            .= (gg `11 ) by A61;

            

             A68: o2 = ( [ [o1, o2], [g1, h1]] `12 ) by MCART_1: 85

            .= (gg `12 ) by A61;

            

             A69: g1 = ( [ [o1, o2], [g1, h1]] `21 ) by MCART_1: 85

            .= (gg `21 ) by A61;

            

             A70: h1 = ( [ [o1, o2], [g1, h1]] `22 ) by MCART_1: 85

            .= (gg `22 ) by A61;

            

             A71: ( cod g) = a by A59, CAT_1: 5;

            

             A72: ( cod g) = (gg `12 ) by A3

            .= ( [ [o1, o2], [g1, h1]] `12 ) by A61

            .= o2 by MCART_1: 85;

            

             A73: o2 = a by A59, A72, CAT_1: 5

            .= [ [c, d], f] by A30;

            

             A74: ( cod (gg `21 )) = ( cod ( [ [o1, o2], [g1, h1]] `21 )) by A61

            .= ( cod g1) by MCART_1: 85

            .= (o2 `11 ) by A62

            .= ( [ [c, d], f] `11 ) by A73

            .= (o `11 ) by A30;

            

             A75: ( cod (gg `22 )) = ( cod ( [ [o1, o2], [g1, h1]] `22 )) by A61

            .= ( cod h1) by MCART_1: 85

            .= (o2 `12 ) by A63

            .= ( [ [c, d], f] `12 ) by A73

            .= (o `12 ) by A30;

            

             A76: (ii `11 ) = ( [ [o, o], [( id (o `11 )), ( id (o `12 ))]] `11 )

            .= ( cod g) by A71, MCART_1: 85

            .= (C9 . gg)

            .= (gg `12 ) by A3;

            

             A77: (ii `11 ) = o by MCART_1: 85

            .= (ii `12 ) by MCART_1: 85;

            (gg `12 ) = (ii `11 ) by A76;

            then

             A78: [ii, gg] in ( dom ( commaComp (F,G))) by A64;

            

            hence (i (*) g) = (( commaComp (F,G)) . (i,g)) by CAT_1:def 1

            .= (ii * gg) by A78, Def4

            .= [ [(gg `11 ), (gg `12 )], [((ii `21 ) (*) (gg `21 )), ((ii `22 ) (*) (gg `22 ))]] by A1, A77, Def3, A76

            .= [ [(gg `11 ), (gg `12 )], [(gg `21 ), ((ii `22 ) (*) (gg `22 ))]] by A74, A65, CAT_1: 21

            .= [ [(gg `11 ), (gg `12 )], [(gg `21 ), (gg `22 )]] by A66, A75, CAT_1: 21

            .= g by A67, A68, A69, A70, A61;

          end;

        end;

        

         A79: for f,g be Morphism of FG st ( dom g) = ( cod f) holds ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g)

        proof

          let f,g be Morphism of FG such that

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

          reconsider f1 = f, g1 = g as Element of ( commaMorphs (F,G));

          

           A81: ( dom g) = (g1 `11 ) & ( cod f) = (f1 `12 ) by A2, A3;

          then [g1, f1] in ( dom a9) by A4, A80;

          then

           A82: (g (*) f) = (a9 . (g,f)) & (a9 . (g1,f1)) = (g1 * f1) by Def4, CAT_1:def 1;

          

           A83: ( dom f) = (f `11 ) & ( cod g) = (g `12 ) by A2, A3;

          

           A84: ( dom (g (*) f)) = ((g (*) f) `11 ) & ( cod (g (*) f)) = ((g (*) f) `12 ) by A2, A3;

          (g1 * f1) = [ [(f1 `11 ), (g1 `12 )], [((g1 `21 ) (*) (f1 `21 )), ((g1 `22 ) (*) (f1 `22 ))]] by A1, A80, A81, Def3;

          hence thesis by A84, A83, A82, MCART_1: 85;

        end;

        

         A85: for f,g,h be Morphism of FG st ( dom h) = ( cod g) & ( dom g) = ( cod f) holds (h (*) (g (*) f)) = ((h (*) g) (*) f)

        proof

          let f,g,h be Morphism of FG;

          reconsider f1 = f, g1 = g, h1 = h, gf = (g (*) f), hg = (h (*) g) as Element of ( commaMorphs (F,G));

          assume that

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

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

          

           A88: ( dom g) = (g `11 ) & ( cod g) = (g `12 ) by A2, A3;

          ( dom (h (*) g)) = ( dom g) by A79, A86;

          then

           A89: ((h (*) g) (*) f) = [ [(f `11 ), (hg `12 )], [((hg `21 ) (*) (f1 `21 )), ((hg `22 ) (*) (f1 `22 ))]] by A5, A87;

          

           A90: ( dom h) = (h `11 ) & ( cod f) = (f `12 ) by A2, A3;

          ( cod (g (*) f)) = ( cod g) by A79, A87;

          then

           A91: (h (*) (g (*) f)) = [ [(gf `11 ), (h `12 )], [((h1 `21 ) (*) (gf `21 )), ((h1 `22 ) (*) (gf `22 ))]] by A5, A86;

          

           A92: ( dom (h1 `21 )) = ((h1 `11 ) `11 ) & ( cod (f1 `21 )) = ((f1 `12 ) `11 ) by A1, Th2;

          

           A93: ( dom (h1 `22 )) = ((h1 `11 ) `12 ) & ( cod (f1 `22 )) = ((f1 `12 ) `12 ) by A1, Th2;

          

           A94: ( dom (g1 `22 )) = ((g1 `11 ) `12 ) & ( cod (g1 `22 )) = ((g1 `12 ) `12 ) by A1, Th2;

          

           A95: (h (*) g) = [ [(g `11 ), (h `12 )], [((h1 `21 ) (*) (g1 `21 )), ((h1 `22 ) (*) (g1 `22 ))]] by A5, A86;

          then

           A96: ((h (*) g) `12 ) = (h `12 ) & (hg `21 ) = ((h1 `21 ) (*) (g1 `21 )) by MCART_1: 85;

          

           A97: (g (*) f) = [ [(f `11 ), (g `12 )], [((g1 `21 ) (*) (f1 `21 )), ((g1 `22 ) (*) (f1 `22 ))]] by A5, A87;

          then

           A98: ((g (*) f) `11 ) = (f `11 ) & (gf `21 ) = ((g1 `21 ) (*) (f1 `21 )) by MCART_1: 85;

          

           A99: (gf `22 ) = ((g1 `22 ) (*) (f1 `22 )) by A97, MCART_1: 85;

          

           A100: (hg `22 ) = ((h1 `22 ) (*) (g1 `22 )) by A95, MCART_1: 85;

          ( dom (g1 `21 )) = ((g1 `11 ) `11 ) & ( cod (g1 `21 )) = ((g1 `12 ) `11 ) by A1, Th2;

          then (((h1 `21 ) (*) (g1 `21 )) (*) (f1 `21 )) = ((h1 `21 ) (*) ((g1 `21 ) (*) (f1 `21 ))) by A86, A87, A88, A92, A90, CAT_1: 18;

          hence thesis by A86, A87, A88, A90, A94, A93, A91, A89, A96, A98, A100, A99, CAT_1: 18;

        end;

        for f,g be Morphism of FG holds [g, f] in ( dom the Comp of FG) iff ( dom g) = ( cod f)

        proof

          let f,g be Morphism of FG;

          reconsider f1 = f, g1 = g as Element of ( commaMorphs (F,G));

          

           A101: ( dom g) = (g1 `11 ) & ( cod f) = (f1 `12 ) by A2, A3;

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

          proof

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

            then

            consider k1, k2 such that

             A102: [g, f] = [k1, k2] and

             A103: (k1 `11 ) = (k2 `12 ) by A4;

            g = k1 by A102, XTUPLE_0: 1;

            hence thesis by A101, A102, A103, XTUPLE_0: 1;

          end;

          thus thesis by A4, A101;

        end;

        then

        reconsider FG as strict Category by A79, A85, A11, A25, CAT_1:def 6, CAT_1:def 7, CAT_1:def 8, CAT_1:def 9, CAT_1:def 10;

        take FG;

        thus thesis by A2, A3;

      end;

      uniqueness

      proof

        let E1,E2 be strict Category such that

         A104: the carrier of E1 = ( commaObjs (F,G)) and

         A105: the carrier' of E1 = ( commaMorphs (F,G)) and

         A106: for k holds (the Source of E1 . k) = (k `11 ) and

         A107: for k holds (the Target of E1 . k) = (k `12 ) and

         A108: the Comp of E1 = ( commaComp (F,G)) and

         A109: the carrier of E2 = ( commaObjs (F,G)) & the carrier' of E2 = ( commaMorphs (F,G)) and

         A110: for k holds (the Source of E2 . k) = (k `11 ) and

         A111: for k holds (the Target of E2 . k) = (k `12 ) and

         A112: the Comp of E2 = ( commaComp (F,G));

        now

          let x be Element of morph(E1);

          

          thus (the Target of E1 . x) = (x `12 ) by A105, A107

          .= (the Target of E2 . x) by A105, A111;

        end;

        then

         A113: the Target of E1 = the Target of E2 by A104, A105, A109, FUNCT_2: 63;

        now

          let x be Element of morph(E1);

          

          thus (the Source of E1 . x) = (x `11 ) by A105, A106

          .= (the Source of E2 . x) by A105, A110;

        end;

        then the Source of E1 = the Source of E2 by A104, A105, A109, FUNCT_2: 63;

        hence thesis by A104, A105, A108, A109, A112, A113;

      end;

    end

    theorem :: COMMACAT:3

    the carrier of ( 1Cat (x,y)) = {x} & the carrier' of ( 1Cat (x,y)) = {y};

    theorem :: COMMACAT:4

    

     Th4: for a,b be Object of ( 1Cat (x,y)) holds ( Hom (a,b)) = {y}

    proof

      let a,b be Object of ( 1Cat (x,y));

      thus ( Hom (a,b)) c= {y};

      y is Morphism of ( 1Cat (x,y)) by TARSKI:def 1;

      then y in ( Hom (a,b)) by CAT_1: 11;

      hence thesis by ZFMISC_1: 31;

    end;

    definition

      let C, c;

      :: COMMACAT:def6

      func 1Cat c -> strict Subcategory of C equals ( 1Cat (c,( id c)));

      coherence

      proof

         A1:

        now

          let a be Object of ( 1Cat (c,( id c)));

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

          hence for c1 st a = c1 holds ( id a) = ( id c1) by TARSKI:def 1;

        end;

         A2:

        now

          let a,b be Object of ( 1Cat (c,( id c)));

          

           A3: a = c & b = c by TARSKI:def 1;

          ( id c) in ( Hom (c,c)) & ( Hom (a,a)) = {( id c)} by Th4, CAT_1: 27;

          hence for c1, c2 st a = c1 & b = c2 holds ( Hom (a,b)) c= ( Hom (c1,c2)) by A3, ZFMISC_1: 31;

        end;

        set m = ( id c);

        set s = ((m,m) .--> m);

        

         A4: ( dom s) = { [m, m]} by FUNCOP_1: 13;

        

         A5: ( dom m) = c;

        

         A6: ( cod m) = c;

        

         A7: (s . (m,m)) = m by FUNCOP_1: 71;

         A8:

        now

          let x be object;

          assume

           A9: x in ( dom the Comp of ( 1Cat (c,m)));

          

          hence (the Comp of ( 1Cat (c,m)) . x) = m by A7, A4, TARSKI:def 1

          .= (m (*) m qua Morphism of C) by A6, CAT_1: 21

          .= (the Comp of C . (m,m)) by A5, A6, CAT_1: 16

          .= (the Comp of C . x) by A4, A9, TARSKI:def 1;

        end;

         [m, m] in ( dom the Comp of C) by A5, A6, CAT_1: 15;

        then ( dom the Comp of ( 1Cat (c,m))) c= ( dom the Comp of C) by A4, ZFMISC_1: 31;

        then obj(1Cat) = {c} & the Comp of ( 1Cat (c,( id c))) c= the Comp of C by A8, GRFUNC_1: 2;

        hence thesis by A2, A1, CAT_2:def 4;

      end;

    end

    definition

      let C, c;

      :: COMMACAT:def7

      func c comma C -> strict Category equals (( incl ( 1Cat c)) comma ( id C));

      coherence ;

      :: COMMACAT:def8

      func C comma c -> strict Category equals (( id C) comma ( incl ( 1Cat c)));

      coherence ;

    end