The Mizar article:

Cartesian Categories

by
Czeslaw Bylinski

Received October 27, 1992

Copyright (c) 1992 Association of Mizar Users

MML identifier: CAT_4
[ MML identifier index ]


environ

 vocabulary FUNCT_1, CAT_1, WELLORD1, BOOLE, FINSET_1, CAT_3, RELAT_1,
      FUNCOP_1, FINSEQ_4, CARD_1, ARYTM_1, FUNCT_4, FUNCT_6, PARTFUN1, FUNCT_3,
      ALGSTR_1, DIRAF, EQREL_1, CAT_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, DOMAIN_1, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCT_2, ALGSTR_1, REAL_1, NAT_1, CARD_1, FUNCT_4,
      CAT_1, CAT_3;
 constructors DOMAIN_1, ALGSTR_1, REAL_1, NAT_1, CAT_3, FINSEQ_4, PARTFUN1,
      XREAL_0, XBOOLE_0;
 clusters SUBSET_1, FINSET_1, RELSET_1, RELAT_1, FUNCT_1, NAT_1, ZFMISC_1,
      XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE;
 definitions CAT_1, CAT_3;
 theorems TARSKI, ZFMISC_1, FUNCT_2, FUNCOP_1, FUNCT_4, CARD_1, CARD_2, CAT_1,
      CAT_3, FUNCT_1, RELSET_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1;
 schemes NAT_1;

begin

reserve o,m,r for set;

definition let o,m,r;
 func (o,m) :-> r -> Function of [:{o},{m}:],{r} means
     not contradiction;
 existence;
 uniqueness by FUNCT_2:66;
end;

definition let C be Category, a,b be Object of C;
 redefine pred a,b are_isomorphic means
    Hom(a,b)<>{} & Hom(b,a)<>{} &
   ex f being Morphism of a,b, f' being Morphism of b,a
    st f*f' = id b & f'*f = id a;
 compatibility by CAT_1:81;
end;

begin :: Cartesian Categories

definition let C be Category;
 attr C is with_finite_product means
    for I being finite set, F being Function of I,the Objects of C
   ex a being Object of C, F' being Projections_family of a,I
    st cods F' = F & a is_a_product_wrt F';
  synonym C has_finite_product;
end;

theorem Th1:
   for C being Category holds
    C has_finite_product iff
     (ex a being Object of C st a is terminal) &
     for a,b being Object of C
      ex c being Object of C, p1,p2 being Morphism of C
       st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b &
        c is_a_product_wrt p1,p2
 proof let C be Category;
  thus C has_finite_product implies
    (ex a being Object of C st a is terminal) &
    for a,b being Object of C
     ex c being Object of C, p1,p2 being Morphism of C
      st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b &
       c is_a_product_wrt p1,p2
   proof assume
A1:  for I being finite set, F being Function of I,the Objects of C
     ex a being Object of C, F' being Projections_family of a,I
      st cods F' = F & a is_a_product_wrt F';
    reconsider F = {} as Function of {},the Objects of C by FUNCT_2:55,RELAT_1:
60;
    consider a being Object of C, F' being Projections_family of a,{}
    such that cods F' = F and
A2:   a is_a_product_wrt F' by A1;
      a is terminal by A2,CAT_3:55;
    hence ex a being Object of C st a is terminal;
    let a,b be Object of C;
    set F = (0,1)-->(a,b);
    consider c being Object of C, F' being Projections_family of c,{0,1}
    such that
A3:   cods F' = F and
A4:   c is_a_product_wrt F' by A1;
    take c, p1 = F'/.0, p2 = F'/.1;
A5:   0 in {0,1} & 1 in {0,1} by TARSKI:def 2;
    hence dom p1 = c & dom p2 = c by CAT_3:45;
      F/.0 = a & F/.1 = b by CAT_3:7;
    hence cod p1 = a & cod p2 = b by A3,A5,CAT_3:def 4;
A6:  dom F' = {0,1} by FUNCT_2:def 1;
      p1 = F'.0 & p2 = F'.1 by A5,CAT_3:def 1;
    then 0 <> 1 & F' = (0,1)-->(p1,p2) by A6,FUNCT_4:69;
    hence c is_a_product_wrt p1,p2 by A4,CAT_3:59;
   end;
  given a being Object of C such that
A7: a is terminal;
  assume
A8:for a,b being Object of C
     ex c being Object of C, p1,p2 being Morphism of C
      st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b &
       c is_a_product_wrt p1,p2;
 defpred Q[Nat] means
  for I being finite set, F being Function of I,the Objects of C
    st card I = $1
   ex a being Object of C, F' being Projections_family of a,I
    st cods F' = F & a is_a_product_wrt F';
A9: Q[ 0 ]
  proof let I be finite set, F be Function of I,the Objects of C;
   assume A10: card I = 0;
then A11:  I = {} by CARD_2:59;
     {} is Function of {}, the Morphisms of C by FUNCT_2:55,RELAT_1:60;
   then reconsider F' = {} as Projections_family of a,I by A11,CAT_3:46;
   take a,F';
     for x being set st x in I holds (cods F')/.x = F/.x by A10,CARD_2:59;
   hence cods F' = F by CAT_3:1;
   thus thesis by A7,A11,CAT_3:55;
  end;
A12: for n being Nat st Q[n] holds Q[n+1]
   proof let n be Nat such that
A13:  Q[n];
    let I be finite set, F be Function of I,the Objects of C such that
A14:  card I = n+1;
    consider x being Element of I;
    reconsider Ix = I \ {x} as finite set;
A15: {x} c= I by A14,CARD_1:47,ZFMISC_1:37;
    reconsider sx = {x} as finite set;
A16:   card(Ix) = card(I) - card(sx) by A15,CARD_2:63
                 .= card(I) - 1 by CARD_1:79
                 .= n by A14,XCMPLX_1:26;
A17:  I\{x} c= I & the Objects of C <> {} by XBOOLE_1:36;
    then reconsider G = F|(I\{x}) as Function of I\{x},the Objects of C
     by FUNCT_2:38;
    consider a being Object of C, G' being Projections_family of a,I\{x}
    such that
A18:   cods G' = G and
A19:   a is_a_product_wrt G' by A13,A16;
    consider c being Object of C, p1,p2 being Morphism of C
     such that
A20:   dom p1 = c & dom p2 = c and
A21:   cod p1 = a & cod p2 = F/.x and
A22:  c is_a_product_wrt p1,p2 by A8;
    set F' = (G'*p1) +* ({x} -->p2);
A23:    dom(G'*p1) = I\{x} & dom({x} -->p2) = {x} by FUNCT_2:def 1;
    then A24: dom(G'*p1) \/ dom({x} -->p2) = I \/ {x} by XBOOLE_1:39
                                    .= I by A14,CARD_1:47,ZFMISC_1:46;
    then A25:  dom F' = I by FUNCT_4:def 1;
A26:  rng F' c= rng(G'*p1) \/ rng({x} -->p2) by FUNCT_4:18;
      rng(G'*p1) c= the Morphisms of C & rng({x} -->p2) c= the Morphisms of C
     by RELSET_1:12;
    then rng(G'*p1) \/ rng({x} -->p2) c= the Morphisms of C by XBOOLE_1:8;
    then rng F' c= the Morphisms of C by A26,XBOOLE_1:1;
    then reconsider F' as Function of I, the Morphisms of C
     by A25,FUNCT_2:def 1,RELSET_1:11;
A27:  doms G' = (I\{x})-->a by CAT_3:def 14;
      now let y be set;
     assume
A28:     y in I;
       now per cases;
      suppose y = x;
then A29:     y in {x} by TARSKI:def 1;
         F'/.y = F'.y by A28,CAT_3:def 1
            .= ({x} -->p2).y by A23,A29,FUNCT_4:14
            .= p2 by A29,FUNCOP_1:13;
       hence (I --> c).y = dom(F'/.y) by A20,A28,FUNCOP_1:13
                        .= (doms F')/.y by A28,CAT_3:def 3;
      suppose
A30:     y <> x;
then A31:     not y in {x} by TARSKI:def 1;
A32:     y in I\{x} by A28,A30,ZFMISC_1:64;
         F'/.y = F'.y by A28,CAT_3:def 1
            .= (G'*p1).y by A23,A24,A28,A31,FUNCT_4:def 1
            .= (G'*p1)/.y by A32,CAT_3:def 1;
       hence (doms F')/.y = dom((G'*p1)/.y) by A28,CAT_3:def 3
                         .= (doms(G'*p1))/.y by A32,CAT_3:def 3
                         .= ((I\{x})-->c)/.y by A20,A21,A27,CAT_3:20
                         .= c by A32,CAT_3:2
                         .= (I --> c).y by A28,FUNCOP_1:13;
     end;
     hence (doms F').y = (I --> c).y by A28,CAT_3:def 1;
    end;
    then doms F' = I --> c by FUNCT_2:18;
    then reconsider F' as Projections_family of c,I by CAT_3:def 14;
    take c,F';
      now let y be set;
     assume
A33:     y in I;
       now per cases;
      suppose
A34:     y = x;
then A35:     y in {x} by TARSKI:def 1;
         F'/.y = F'.y by A33,CAT_3:def 1
            .= ({x} -->p2).y by A23,A35,FUNCT_4:14
            .= p2 by A35,FUNCOP_1:13;
       hence (cods F')/.y = F/.y by A21,A33,A34,CAT_3:def 4;
      suppose
A36:     y <> x;
then A37:     not y in {x} by TARSKI:def 1;
A38:     y in I\{x} by A33,A36,ZFMISC_1:64;
         F'/.y = F'.y by A33,CAT_3:def 1
            .= (G'*p1).y by A23,A24,A33,A37,FUNCT_4:def 1
            .= (G'*p1)/.y by A38,CAT_3:def 1;
       hence (cods F')/.y = cod((G'*p1)/.y) by A33,CAT_3:def 4
                         .= (cods(G'*p1))/.y by A38,CAT_3:def 4
                         .= G/.y by A18,A21,A27,CAT_3:20
                         .= G.y by A38,CAT_3:def 1
                         .= F.y by A38,FUNCT_1:72
                         .= F/.y by A33,CAT_3:def 1;
     end;
     hence (cods F')/.y = F/.y;
    end;
    hence
A39:  cods F' = F by CAT_3:1;
    thus F' is Projections_family of c,I;
    let d be Object of C;
    let F'' be Projections_family of d,I such that
A40:  cods F' = cods F'';
    reconsider G'' = F''|(I\{x}) as Function of I\{x},the Morphisms of C
     by A17,FUNCT_2:38;
      now let y be set;
     assume
A41:   y in I\{x};
then A42:   y in I by XBOOLE_0:def 4;
       G''/.y = G''.y by A41,CAT_3:def 1
           .= F''.y by A41,FUNCT_1:72
           .= F''/.y by A42,CAT_3:def 1;
     hence doms(G'')/.y = dom(F''/.y) by A41,CAT_3:def 3
                       .= d by A42,CAT_3:45
                       .= ((I\{x})-->d)/.y by A41,CAT_3:2;
    end;
    then doms G'' = I\{x} --> d by CAT_3:1;
    then reconsider G'' as Projections_family of d,I\{x} by CAT_3:def 14;
      now let y be set;
     assume
A43:   y in I\{x};
then A44:   y in I by XBOOLE_0:def 4;
then A45:  F''/.y = F''.y by CAT_3:def 1
           .= G''.y by A43,FUNCT_1:72
           .= G''/.y by A43,CAT_3:def 1;
       G/.y = G.y by A43,CAT_3:def 1
         .= F.y by A43,FUNCT_1:72
         .= F/.y by A44,CAT_3:def 1;
     hence (cods G')/.y = cod(G''/.y) by A18,A39,A40,A44,A45,CAT_3:def 4
                       .= (cods G'')/.y by A43,CAT_3:def 4;
    end;
    then cods G' = cods G'' by CAT_3:1;
    then consider h' being Morphism of C such that
A46:  h' in Hom(d,a) and
A47:  for k being Morphism of C st k in Hom(d,a) holds
       (for y being set st y in I\{x} holds (G'/.y)*k = G''/.y) iff h' = k
       by A19,CAT_3:def 15;
   set g = F''/.x;
A48:  dom g = d by A14,CARD_1:47,CAT_3:45;
A49:  x in {x} by TARSKI:def 1;
A50:  F'/.x = F'.x by A14,CARD_1:47,CAT_3:def 1
        .= ({x} -->p2).x by A23,A49,FUNCT_4:14
        .= p2 by A49,FUNCOP_1:13;
   then cod p2 = (cods F')/.x by A14,CARD_1:47,CAT_3:def 4
              .= cod g by A14,A40,CARD_1:47,CAT_3:def 4;
   then g in Hom(d,cod p2) by A48,CAT_1:18;
   then consider h being Morphism of C such that
A51:  h in Hom(d,c) and
A52:  for k being Morphism of C st k in Hom(d,c)
       holds p1*k = h' & p2*k = g iff h = k by A21,A22,A46,CAT_3:def 16;
    take h;
    thus h in Hom(d,c) by A51;
    let k be Morphism of C such that
A53:  k in Hom(d,c);
    thus (for y being set st y in I holds (F'/.y)*k = F''/.y) implies h = k
     proof assume
A54:     for y being set st y in I holds (F'/.y)*k = F''/.y;
      then A55:     p2*k = g by A14,A50,CARD_1:47;
A56:     dom k = d & cod k = c by A53,CAT_1:18;
        then dom(p1*k) = d & cod(p1*k) = a by A20,A21,CAT_1:42;
then A57:     p1*k in Hom(d,a) by CAT_1:18;
        for y being set st y in I\{x} holds (G'/.y)*(p1*k) = G''/.y
       proof let y be set;
        assume
A58:       y in I\{x};
then A59:      y in I & not y in {x} by XBOOLE_0:def 4;
then A60:      F'/.y = F'.y by CAT_3:def 1
             .= (G'*p1).y by A23,A24,A59,FUNCT_4:def 1
             .= (G'*p1)/.y by A58,CAT_3:def 1;
          dom(G'/.y) = a by A58,CAT_3:45;
        hence (G'/.y)*(p1*k) = ((G'/.y)*p1)*k by A20,A21,A56,CAT_1:43
                            .= ((G'*p1)/.y)*k by A58,CAT_3:def 7
                            .= F''/.y by A54,A59,A60
                            .= F''.y by A59,CAT_3:def 1
                            .= G''.y by A58,FUNCT_1:72
                            .= G''/.y by A58,CAT_3:def 1;
       end;
      then p1*k = h' by A47,A57;
      hence h = k by A52,A53,A55;
     end;
    assume
A61:  h = k;
    let y be set such that
A62:  y in I;
       now per cases;
      suppose
A63:     y = x;
then A64:     y in {x} by TARSKI:def 1;
         F'/.y = F'.y by A62,CAT_3:def 1
            .= ({x} -->p2).y by A23,A64,FUNCT_4:14
            .= p2 by A64,FUNCOP_1:13;
       hence thesis by A52,A53,A61,A63;
      suppose
A65:     y <> x;
then A66:     not y in {x} by TARSKI:def 1;
A67:     y in I\{x} by A62,A65,ZFMISC_1:64;
then A68:     cod k = c & dom(G'/.y) = a by A53,CAT_1:18,CAT_3:45;
         F'/.y = F'.y by A62,CAT_3:def 1
            .= (G'*p1).y by A23,A24,A62,A66,FUNCT_4:def 1
            .= (G'*p1)/.y by A67,CAT_3:def 1
            .= (G'/.y)*p1 by A67,CAT_3:def 7;
       hence (F'/.y)*k = (G'/.y)*(p1*k) by A20,A21,A68,CAT_1:43
                      .= (G'/.y)*h' by A52,A53,A61
                      .= G''/.y by A46,A47,A67
                      .= G''.y by A67,CAT_3:def 1
                      .= F''.y by A67,FUNCT_1:72
                      .= F''/.y by A62,CAT_3:def 1;
     end;
    hence thesis;
   end;
A69: for n being Nat holds Q[n] from Ind(A9,A12);
  let I be finite set, F be Function of I,the Objects of C;
    card I = card I;
  hence thesis by A69;
 end;

definition
  struct (CatStr)ProdCatStr
   (# Objects,Morphisms -> non empty set,
     Dom,Cod -> Function of the Morphisms, the Objects,
     Comp -> PartFunc of [:the Morphisms, the Morphisms :],the Morphisms,
     Id -> Function of the Objects, the Morphisms,
     TerminalObj -> Element of the Objects,
     CatProd -> Function of [:the Objects,the Objects:],the Objects,
     Proj1,Proj2 -> Function of [:the Objects,the Objects:],the Morphisms
    #);
end;

definition let C be ProdCatStr;
 func [1]C -> Object of C equals
:Def4:  the TerminalObj of C;
   correctness;
  let a,b be Object of C;
  func a[x]b -> Object of C equals
:Def5:  (the CatProd of C).[a,b];
   correctness;
 func pr1(a,b) -> Morphism of C equals
:Def6:  (the Proj1 of C).[a,b];
   correctness;
 func pr2(a,b) -> Morphism of C equals
:Def7:  (the Proj2 of C).[a,b];
   correctness;
end;

definition let o,m;
 func c1Cat(o,m) -> strict ProdCatStr equals
:Def8:  ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
                        Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #);
 correctness;
end;

theorem
     the CatStr of c1Cat(o,m) = 1Cat(o,m)
 proof
    c1Cat(o,m) = ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
                      Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def8;
  hence thesis by CAT_1:def 9;
 end;

Lm1: c1Cat(o,m) is Category-like
 proof
  set C = c1Cat(o,m);
A1: C = ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
                    Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def8;
  set CP = the Comp of C, CD = the Dom of C, CC = the Cod of C,
      CI = the Id of C;
  thus for f,g being Morphism of C holds
      [g,f] in dom CP iff CD.g=CC.f
    proof let f,g be Morphism of C;
       f = m & g = m & dom CP = {[m,m]} by A1,CAT_1:7,TARSKI:def 1;
     hence thesis by A1,TARSKI:def 1;
    end;
  thus for f,g being Morphism of C
    st CD.g=CC.f holds CD.(CP.[g,f]) = CD.f & CC.(CP.[g,f]) = CC.g
    proof let f,g be Morphism of C;
       CP.[g,f] = m by A1,CAT_1:9;
     then reconsider gf = CP.[g,f] as Morphism of C by A1,TARSKI:def 1;
       CD.f = o & CC.g = o & CD.gf = o & CC.gf = o by A1,FUNCT_2:65;
     hence thesis;
    end;
  thus for f,g,h being Morphism of C
      st CD.h = CC.g & CD.g = CC.f
     holds CP.[h,CP.[g,f]] = CP.[CP.[h,g],f]
   proof let f,g,h be Morphism of C;
       CP.[g,f] = m & CP.[h,g] = m by A1,CAT_1:9;
     then reconsider gf = CP.[g,f],hg = CP.[h,g] as Morphism of C
      by A1,TARSKI:def 1; CP.[h,gf] = m & CP.[hg,f] = m by A1,CAT_1:9;
    hence thesis;
   end;
  let b be Object of C;
    b = o by A1,TARSKI:def 1;
  hence CD.(CI.b) = b & CC.(CI.b) = b by A1,FUNCT_2:65;
  thus for f being Morphism of C st CC.f = b holds CP.[CI.b,f] = f
    proof let f be Morphism of C; f = m by A1,TARSKI:def 1;
     hence thesis by A1,CAT_1:9;
    end;
  let g be Morphism of C;
  assume CD.g = b;
    g = m by A1,TARSKI:def 1;
  hence CP.[g,CI.b] = g by A1,CAT_1:9;
 end;

definition
 cluster strict Category-like ProdCatStr;
  existence
 proof c1Cat(0,1) is Category-like by Lm1; hence thesis; end;
end;

definition let o,m be set;
 cluster c1Cat(o,m) -> Category-like;
  coherence by Lm1;
end;

theorem Th3:
   for a being Object of c1Cat(o,m) holds a = o
 proof let a be Object of c1Cat(o,m);
    c1Cat(o,m) = ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
                      Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def8;
  hence thesis by TARSKI:def 1;
 end;

theorem Th4:
   for a,b being Object of c1Cat(o,m) holds a = b
 proof let a,b be Object of c1Cat(o,m);
    a = o & b = o by Th3; hence thesis;
 end;

theorem Th5:
   for f being Morphism of c1Cat(o,m) holds f = m
 proof let f be Morphism of c1Cat(o,m);
    c1Cat(o,m) = ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
                      Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def8;
  hence thesis by TARSKI:def 1;
 end;

theorem Th6:
   for f,g being Morphism of c1Cat(o,m) holds f = g
 proof let f,g be Morphism of c1Cat(o,m);
    f = m & g = m by Th5; hence thesis;
 end;

theorem Th7:
   for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m)
     holds f in Hom(a,b)
 proof let a,b be Object of c1Cat(o,m), f be Morphism of c1Cat(o,m);
    dom f = o & cod f = o by Th3; then dom f = a & cod f = b by Th3;
  hence f in Hom(a,b) by CAT_1:18;
 end;

theorem
     for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m)
    holds f is Morphism of a,b
 proof let a,b be Object of c1Cat(o,m), f be Morphism of c1Cat(o,m);
    f in Hom(a,b) by Th7; hence thesis by CAT_1:def 7;
 end;

theorem
    for a,b being Object of c1Cat(o,m) holds Hom(a,b) <> {} by Th7;

theorem Th10:
   for a being Object of c1Cat(o,m) holds a is terminal
 proof let a be Object of c1Cat(o,m);
  let b be Object of c1Cat(o,m);
  thus Hom(b,a)<>{} by Th7;
  consider f being Morphism of b,a;
  take f; thus thesis by Th6;
 end;

theorem Th11:
   for c being Object of c1Cat(o,m), p1,p2 being Morphism of c1Cat(o,m)
    holds c is_a_product_wrt p1,p2
 proof let c be Object of c1Cat(o,m), p1,p2 be Morphism of c1Cat(o,m);
  thus dom p1 = c & dom p2 = c by Th4;
  let d be Object of c1Cat(o,m),f,g be Morphism of c1Cat(o,m) such that
   f in Hom(d,cod p1) & g in Hom(d,cod p2);
  take h = p1;
  thus h in Hom(d,c) by Th7;
  thus thesis by Th6;
 end;

definition let IT be Category-like ProdCatStr;
 attr IT is Cartesian means
:Def9:
  the TerminalObj of IT is terminal &
  for a,b being Object of IT holds
   cod((the Proj1 of IT).[a,b]) = a & cod((the Proj2 of IT).[a,b]) = b &
    (the CatProd of IT).[a,b]
     is_a_product_wrt (the Proj1 of IT).[a,b],(the Proj2 of IT).[a,b];
end;

theorem Th12:
   for o,m being set holds c1Cat(o,m) is Cartesian
 proof let o,m be set;
  set 1PCat = c1Cat(o,m);
  thus the TerminalObj of 1PCat is terminal by Th10;
  let a,b be Object of 1PCat;
  thus cod((the Proj1 of 1PCat).[a,b]) = a by Th4;
  thus cod((the Proj2 of 1PCat).[a,b]) = b by Th4;
  thus (the CatProd of 1PCat).[a,b]
    is_a_product_wrt (the Proj1 of 1PCat).[a,b],(the Proj2 of 1PCat).[a,b]
   by Th11;
 end;

definition
 cluster strict Cartesian (Category-like ProdCatStr);
  existence
 proof c1Cat(0,1) is Cartesian by Th12;
  hence thesis;
 end;
end;

definition
  mode Cartesian_category is Cartesian (Category-like ProdCatStr);
end;

reserve C for Cartesian_category;
reserve a,b,c,d,e,s for Object of C;

theorem Th13:
   [1]C is terminal
 proof [1]C = the TerminalObj of C by Def4; hence thesis by Def9; end;

theorem Th14: for f1,f2 being Morphism of a,[1]C holds f1 = f2
 proof let f1,f2 be Morphism of a,[1]C;
    [1]C is terminal by Th13;
  then consider f being Morphism of a,[1]C such that
A1: for g being Morphism of a,[1]C holds f = g by CAT_1:def 15;
  thus f1 = f by A1 .= f2 by A1;
 end;

theorem Th15:
   Hom(a,[1]C) <> {}
 proof [1]C is terminal by Th13; hence thesis by CAT_1:def 15; end;

definition let C,a;
 func term(a) -> Morphism of a,[1]C means not contradiction;
  existence;
  uniqueness by Th14;
end;

theorem Th16:
   term a = term(a,[1]C)
 proof [1]C is terminal by Th13; hence thesis by CAT_3:41; end;

theorem
     dom(term a) = a & cod(term a) = [1]C
 proof [1]C is terminal & term a = term(a,[1]C) by Th13,Th16;
  hence thesis by CAT_3:39;
 end;

theorem
     Hom(a,[1]C) = {term a}
 proof
A1: Hom(a,[1]C) <> {} by Th15;
    for f2 being Morphism of a,[1]C holds term a = f2 by Th14;
  hence thesis by A1,CAT_1:26;
 end;

theorem Th19:
   dom pr1(a,b) = a[x]b & cod pr1(a,b) = a
 proof
  set p1 = (the Proj1 of C).[a,b], p2 = (the Proj2 of C).[a,b];
    (the CatProd of C).[a,b] is_a_product_wrt p1,p2 by Def9;
  then a[x]b is_a_product_wrt p1,p2 by Def5;
  then dom p1 = a[x]b & cod p1 = a by Def9,CAT_3:def 16;
  hence thesis by Def6;
 end;

theorem Th20:
   dom pr2(a,b) = a[x]b & cod pr2(a,b) = b
 proof
  set p1 = (the Proj1 of C).[a,b], p2 = (the Proj2 of C).[a,b];
    (the CatProd of C).[a,b] is_a_product_wrt p1,p2 by Def9;
  then a[x]b is_a_product_wrt p1,p2 by Def5;
  then dom p2 = a[x]b & cod p2 = b by Def9,CAT_3:def 16;
  hence thesis by Def7;
 end;

definition let C,a,b;
 redefine func pr1(a,b) -> Morphism of a[x]b,a;
  coherence
 proof dom pr1(a,b) = a[x]b & cod pr1(a,b) = a by Th19;
  hence thesis by CAT_1:22;
 end;
 func pr2(a,b) -> Morphism of a[x]b,b;
  coherence
 proof dom pr2(a,b) = a[x]b & cod pr2(a,b) = b by Th20;
  hence thesis by CAT_1:22;
 end;
end;

theorem Th21:
   Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {}
 proof
  set c = (the CatProd of C).[a,b],
    p1 = (the Proj1 of C).[a,b], p2 = (the Proj2 of C).[a,b];
    c is_a_product_wrt p1,p2 by Def9;
  then dom p1 = c & dom p2 = c & cod(p1) = a & cod(p2) = b by Def9,CAT_3:def 16
;
  then Hom(c,a) <> {} & Hom(c,b) <> {} by CAT_1:18;
  hence thesis by Def5;
 end;

theorem Th22:
   a[x]b is_a_product_wrt pr1(a,b),pr2(a,b)
 proof
    (the CatProd of C).[a,b] = a[x]b & (the Proj1 of C).[a,b] = pr1(a,b) &
  (the Proj2 of C).[a,b] = pr2(a,b) by Def5,Def6,Def7;
  hence thesis by Def9;
 end;

theorem
     C has_finite_product
 proof
A1:   [1]C is terminal by Th13;
    for a,b
   ex c being Object of C, p1,p2 being Morphism of C
    st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b &
     c is_a_product_wrt p1,p2
   proof let a,b;
    take a[x]b, pr1(a,b), pr2(a,b);
    thus thesis by Th19,Th20,Th22;
   end;
  hence thesis by A1,Th1;
 end;

theorem
     Hom(a,b) <> {} & Hom(b,a) <> {}
    implies pr1(a,b) is retraction & pr2(a,b) is retraction
 proof
    a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) &
   cod pr1(a,b) = a & cod pr2(a,b) = b by Th19,Th20,Th22;
  hence thesis by CAT_3:62;
 end;

definition let C,a,b,c;
  let f be Morphism of c,a, g be Morphism of c,b;
assume A1: Hom(c,a) <> {} & Hom(c,b) <> {};
 func <:f,g:> -> Morphism of c,a[x]b means
:Def11:  pr1(a,b)*it = f & pr2(a,b)*it = g;
  existence
 proof Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} &
  a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Th21,Th22;
  then consider h being Morphism of c,a[x]b such that
A2: for h1 being Morphism of c,a[x]b
     holds pr1(a,b)*h1 = f & pr2(a,b)*h1 = g iff h = h1 by A1,CAT_3:60;
  take h; thus thesis by A2;
 end;
  uniqueness
 proof let h1,h2 be Morphism of c,a[x]b such that
A3: pr1(a,b)*h1 = f & pr2(a,b)*h1 = g and
A4: pr1(a,b)*h2 = f & pr2(a,b)*h2 = g;
    Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} &
  a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Th21,Th22;
  then consider h being Morphism of c,a[x]b such that
A5: for h1 being Morphism of c,a[x]b
     holds pr1(a,b)*h1 = f & pr2(a,b)*h1 = g iff h = h1 by A1,CAT_3:60;
    h1 = h & h2 = h by A3,A4,A5;
  hence thesis;
 end;
end;

theorem Th25:
   Hom(c,a) <> {} & Hom(c,b) <> {} implies Hom(c,a[x]b) <> {}
 proof Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} &
  a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Th21,Th22;
  hence thesis by CAT_3:60;
 end;

theorem Th26:
   <:pr1(a,b),pr2(a,b):> = id(a[x]b)
 proof
A1: Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21;
  then pr1(a,b)*(id(a[x]b)) = pr1(a,b) & pr2(a,b)*(id(a[x]b)) = pr2(a,b)
    by CAT_1:58;
  hence thesis by A1,Def11;
 end;

theorem Th27:
  for f being Morphism of c,a, g being Morphism of c,b, h being Morphism of d,c
     st Hom(c,a)<>{} & Hom(c,b)<>{} & Hom(d,c)<>{}
    holds <:f*h,g*h:> = <:f,g:>*h
 proof let f be Morphism of c,a, g be Morphism of c,b, h be Morphism of d,c;
   assume that
A1: Hom(c,a)<>{} and
A2: Hom(c,b)<>{} and
A3: Hom(d,c)<>{};
    Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} & Hom(c,a[x]b) <> {} &
   (pr1(a,b)*<:f,g:>)*h = f*h & (pr2(a,b)*<:f,g:>)*h = g*h
     by A1,A2,Def11,Th21,Th25;
  then pr1(a,b)*(<:f,g:>*h) = f*h & pr2(a,b)*(<:f,g:>*h) = g*h &
    Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A3,CAT_1:52,54;
  hence thesis by Def11;
 end;

theorem Th28:
   for f,k being Morphism of c,a, g,h being Morphism of c,b
     st Hom(c,a) <> {} & Hom(c,b) <> {} & <:f,g:> = <:k,h:>
    holds f = k & g = h
 proof let f,k be Morphism of c,a, g,h be Morphism of c,b;
  assume Hom(c,a) <> {} & Hom(c,b) <> {};
  then pr1(a,b)*<:f,g:> = f & pr1(a,b)*<:k,h:> = k &
     pr2(a,b)*<:f,g:> = g & pr2(a,b)*<:k,h:> = h by Def11;
  hence thesis;
 end;

theorem
     for f being Morphism of c,a, g being Morphism of c,b
    st Hom(c,a) <> {} & Hom(c,b) <> {} & (f is monic or g is monic)
   holds <:f,g:> is monic
 proof let f be Morphism of c,a, g be Morphism of c,b;
  assume that
A1: Hom(c,a) <> {} and
A2: Hom(c,b) <> {} and
A3: f is monic or g is monic;
A4: now assume
A5:   f is monic;
     let d;
     let f1,f2 be Morphism of d,c such that
A6:   Hom(d,c)<>{} and
A7:   <:f,g:>*f1 = <:f,g:>*f2;
       <:f*f1,g*f1:> = <:f,g:>*f1 & <:f*f2,g*f2:> = <:f,g:>*f2 &
     Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A6,Th27,CAT_1:52;
     then f*f1 = f*f2 by A7,Th28;
     hence f1 = f2 by A1,A5,A6,CAT_1:60;
    end;
A8: Hom(c,a[x]b) <> {} by A1,A2,Th25;
     now assume
A9:  g is monic;
    let d be Object of C, f1,f2 be Morphism of d,c such that
A10:  Hom(d,c)<>{} and
A11:  <:f,g:>*f1 = <:f,g:>*f2;
      <:f*f1,g*f1:> = <:f,g:>*f1 & <:f*f2,g*f2:> = <:f,g:>*f2 &
      Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A10,Th27,CAT_1:52;
    then g*f1 = g*f2 by A11,Th28;
    hence f1 = f2 by A2,A9,A10,CAT_1:60;
   end;
  hence thesis by A3,A4,A8,CAT_1:60;
 end;

theorem Th30:
   Hom(a,a[x][1]C) <> {} & Hom(a,[1]C[x]a) <> {}
 proof
    Hom(a,[1]C) <> {} & Hom(a,a) <> {} by Th15,CAT_1:56;
  hence thesis by Th25;
 end;

definition let C,a;
 func lambda(a) -> Morphism of [1]C[x]a,a equals
:Def12:  pr2([1]C,a);
  correctness;
 func lambda'(a) -> Morphism of a,[1]C[x]a equals
:Def13:  <:term a,id a:>;
  correctness;
 func rho(a) -> Morphism of a[x][1]C,a equals
:Def14:  pr1(a,[1]C);
  correctness;
 func rho'(a) -> Morphism of a,a[x][1]C equals
:Def15:  <:id a,term a:>;
  correctness;
end;

theorem Th31:
   lambda(a)*lambda'(a) = id a & lambda'(a)*lambda(a) = id([1]C[x]a) &
   rho(a)*rho'(a) = id a & rho'(a)*rho(a) = id(a[x][1]C)
 proof
A1: Hom(a,[1]C) <> {} & Hom(a,a) <> {} by Th15,CAT_1:56;
A2: Hom([1]C[x]a,a) <> {} by Th21;
   then (id a)*pr2([1]C,a) = pr2([1]C,a) & (term a)*pr2([1]C,a) = pr1([1]C,a)
     & Hom([1]C[x]a,[1]C)<>{} by Th14,Th21,CAT_1:57;
   then A3:<:term a,id a:>*pr2([1]C,a) = <:pr1([1]C,a),pr2([1]C,a):> by A1,A2,
Th27;
     pr2([1]C,a)*<:term a,id a:> = id a by A1,Def11;
  hence id a = lambda(a)*<:term a,id a:> by Def12
            .= lambda(a)*lambda'(a) by Def13;
     <:term a,id a:>*pr2([1]C,a) = id([1]C[x]a) by A3,Th26;
  hence id([1]C[x]a) = <:term a,id a:>*lambda(a) by Def12
                    .= lambda'(a)*lambda(a) by Def13;
A4: Hom(a[x][1]C,a) <> {} by Th21;
   then (id a)*pr1(a,[1]C) = pr1(a,[1]C) & (term a)*pr1(a,[1]C) = pr2(a,[1]C)
     & Hom(a[x][1]C,[1]C)<>{} by Th14,Th21,CAT_1:57;
   then A5: <:id a,term a:>*pr1(a,[1]C) = <:pr1(a,[1]C),pr2(a,[1]C):> by A1,A4,
Th27;
     pr1(a,[1]C)*<:id a,term a:> = id a by A1,Def11;
   hence id a = rho(a)*<:id a,term a:> by Def14
             .= rho(a)*rho'(a) by Def15;
     <:id a,term a:>*pr1(a,[1]C) = id(a[x][1]C) by A5,Th26;
   hence id(a[x][1]C) = <:id a,term a:>*rho(a) by Def14
                     .= rho'(a)*rho(a) by Def15;
 end;

theorem
     a, a[x][1]C are_isomorphic & a,[1]C[x]a are_isomorphic
 proof
  thus a,a[x][1]C are_isomorphic
   proof thus Hom(a,a[x][1]C) <> {} & Hom(a[x][1]C,a) <> {} by Th21,Th30;
    take rho'(a), rho(a);
    thus thesis by Th31;
   end;
  thus Hom(a,[1]C[x]a) <> {} & Hom([1]C[x]a,a) <> {} by Th21,Th30;
  take lambda'(a), lambda(a);
  thus thesis by Th31;
 end;

definition let C,a,b;
 func Switch(a,b) -> Morphism of a[x]b,b[x]a equals
:Def16:  <:pr2(a,b),pr1(a,b):>;
  correctness;
end;

theorem Th33:
  Hom(a[x]b,b[x]a)<>{}
 proof
    Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21;
  hence thesis by Th25;
 end;


theorem Th34:
   Switch(a,b)*Switch(b,a) = id(b[x]a)
 proof
A1: Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21;
A2: Hom(b[x]a,b) <> {} & Hom(b[x]a,a) <> {} by Th21;
then A3: Hom(b[x]a,a[x]b)<>{} by Th25;
  thus Switch(a,b)*Switch(b,a)
     = <:pr2(a,b),pr1(a,b):>*Switch(b,a) by Def16
    .= <:pr2(a,b),pr1(a,b):>*<:pr2(b,a),pr1(b,a):> by Def16
    .= <:pr2(a,b)*<:pr2(b,a),pr1(b,a):>,pr1(a,b)*<:pr2(b,a),pr1(b,a):>:>
        by A1,A3,Th27
    .= <:pr1(b,a),pr1(a,b)*<:pr2(b,a),pr1(b,a):>:> by A2,Def11
    .= <:pr1(b,a),pr2(b,a):> by A2,Def11
    .= id(b[x]a) by Th26;
 end;

theorem
     a[x]b,b[x]a are_isomorphic
 proof
  thus Hom(a[x]b,b[x]a)<>{} & Hom(b[x]a,a[x]b)<>{} by Th33;
  take Switch(a,b), Switch(b,a);
  thus thesis by Th34;
 end;

definition let C,a;
 func Delta a -> Morphism of a,a[x]a equals
:Def17:  <:id a,id a:>;
  correctness;
end;

theorem
     Hom(a,a[x]a) <> {}
 proof Hom(a,a) <> {} by CAT_1:56; hence thesis by Th25; end;

theorem
     for f being Morphism of a,b st Hom(a,b) <> {}
    holds <:f,f:> = Delta(b)*f
 proof let f be Morphism of a,b such that
A1: Hom(a,b) <> {};
A2: Hom(b,b) <> {} by CAT_1:56;
    (id b)*f = f by A1,CAT_1:57;
  hence <:f,f:> = <:id b, id b:>*f by A1,A2,Th27
               .= Delta(b)*f by Def17;
 end;

definition let C,a,b,c;
 func Alpha(a,b,c) -> Morphism of (a[x]b)[x]c,a[x](b[x]c) equals
:Def18:  <:pr1(a,b)*pr1(a[x]b,c),<:pr2(a,b)*pr1(a[x]b,c),pr2(a[x]b,c):>:>;
  correctness;
 func Alpha'(a,b,c) -> Morphism of a[x](b[x]c),(a[x]b)[x]c equals
:Def19:  <:<:pr1(a,b[x]c),pr1(b,c)*pr2(a,b[x]c):>,pr2(b,c)*pr2(a,b[x]c):>;
  correctness;
end;

theorem Th38:
   Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} & Hom(a[x](b[x]c),(a[x]b)[x]c) <> {}
 proof
A1: Hom(a[x]b,a) <> {} by Th21;
A2: Hom((a[x]b)[x]c,a[x]b) <> {} by Th21;
then A3: Hom((a[x]b)[x]c,a) <> {} by A1,CAT_1:52;
   Hom(a[x]b,b) <> {} by Th21;
then A4: Hom((a[x]b)[x]c,b) <> {} by A2,CAT_1:52;
   Hom((a[x]b)[x]c,c) <> {} by Th21;
   then Hom((a[x]b)[x]c,b[x]c) <> {} by A4,Th25;
  hence Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} by A3,Th25;
A5: Hom(b[x]c,b) <> {} by Th21;
A6: Hom(a[x](b[x]c),b[x]c) <> {} by Th21;
then A7: Hom(a[x](b[x]c),b) <> {} by A5,CAT_1:52;
   Hom(b[x]c,c) <> {} by Th21;
then A8: Hom(a[x](b[x]c),c) <> {} by A6,CAT_1:52;
   Hom(a[x](b[x]c),a) <> {} by Th21;
   then Hom(a[x](b[x]c),a[x]b) <> {} by A7,Th25;
  hence Hom(a[x](b[x]c),(a[x]b)[x]c) <> {} by A8,Th25;
 end;

theorem Th39:
   Alpha(a,b,c)*Alpha'(a,b,c) = id(a[x](b[x]c)) &
   Alpha'(a,b,c)*Alpha(a,b,c) = id((a[x]b)[x]c)
 proof
A1: Hom(a[x]b,a) <> {} by Th21;
A2: Hom((a[x]b)[x]c,a[x]b) <> {} by Th21;
then A3: Hom((a[x]b)[x]c,a) <> {} by A1,CAT_1:52;
A4: Hom(a[x]b,b) <> {} by Th21;
then A5: Hom((a[x]b)[x]c,b) <> {} by A2,CAT_1:52;
A6: Hom((a[x]b)[x]c,c) <> {} by Th21;
then A7: Hom((a[x]b)[x]c,b[x]c) <> {} by A5,Th25;
A8: Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} by Th38;
A9: Hom(b[x]c,b) <> {} by Th21;
A10: Hom(a[x](b[x]c),b[x]c) <> {} by Th21;
then A11: Hom(a[x](b[x]c),b) <> {} by A9,CAT_1:52;
A12: Hom(b[x]c,c) <> {} by Th21;
then A13: Hom(a[x](b[x]c),c) <> {} by A10,CAT_1:52;
A14: Hom(a[x](b[x]c),a) <> {} by Th21;
then A15: Hom(a[x](b[x]c),a[x]b) <> {} by A11,Th25;
A16: Hom(a[x](b[x]c),(a[x]b)[x]c) <> {} by Th38;
  set k = <:pr2(a,b)*pr1(a[x]b,c),pr2(a[x]b,c):>;
  set l = <:pr1(a,b[x]c),pr1(b,c)*pr2(a,b[x]c):>;
  set f = <:pr1(a,b)*pr1(a[x]b,c),k:>;
  set g = <:l,pr2(b,c)*pr2(a,b[x]c):>;
A17: pr1(a,b)*pr1(a[x]b,c)*g
      = pr1(a,b)*(pr1(a[x]b,c)*g) by A1,A2,A16,CAT_1:54
     .= pr1(a,b)*l by A13,A15,Def11
     .= pr1(a,b[x]c) by A11,A14,Def11;
     pr2(a,b)*pr1(a[x]b,c)*g = pr2(a,b)*(pr1(a[x]b,c)*g) by A2,A4,A16,CAT_1:54
                          .= pr2(a,b)*l by A13,A15,Def11
                          .= pr1(b,c)*pr2(a,b[x]c) by A11,A14,Def11;
   then A18:  k*g = <:pr1(b,c)*pr2(a,b[x]c),pr2(a[x]b,c)*g:> by A5,A6,A16,Th27
        .= <:pr1(b,c)*pr2(a,b[x]c),pr2(b,c)*pr2(a,b[x]c):> by A13,A15,Def11
        .= <:pr1(b,c),pr2(b,c):>*pr2(a,b[x]c) by A9,A10,A12,Th27
        .= id(b[x]c)*pr2(a,b[x]c) by Th26
        .= pr2(a,b[x]c) by A10,CAT_1:57;
  thus Alpha(a,b,c)*Alpha'(a,b,c)
      = Alpha(a,b,c)*g by Def19
     .= f*g by Def18
     .= <:pr1(a,b[x]c),pr2(a,b[x]c):> by A3,A7,A16,A17,A18,Th27
     .= id(a[x](b[x]c)) by Th26;
     pr1(b,c)*pr2(a,b[x]c)*f = pr1(b,c)*(pr2(a,b[x]c)*f) by A8,A9,A10,CAT_1:54
                          .= pr1(b,c)*k by A3,A7,Def11
                          .= pr2(a,b)*pr1(a[x]b,c) by A5,A6,Def11;
   then A19:  l*f = <:pr1(a,b[x]c)*f,pr2(a,b)*pr1(a[x]b,c):> by A8,A11,A14,Th27
        .= <:pr1(a,b)*pr1(a[x]b,c),pr2(a,b)*pr1(a[x]b,c):> by A3,A7,Def11
        .= <:pr1(a,b),pr2(a,b):>*pr1(a[x]b,c) by A1,A2,A4,Th27
        .= id(a[x]b)*pr1(a[x]b,c) by Th26
        .= pr1(a[x]b,c) by A2,CAT_1:57;
A20: pr2(b,c)*pr2(a,b[x]c)*f
      = pr2(b,c)*(pr2(a,b[x]c)*f) by A8,A10,A12,CAT_1:54
     .= pr2(b,c)*k by A3,A7,Def11
     .= pr2(a[x]b,c) by A5,A6,Def11;
  thus Alpha'(a,b,c)*Alpha(a,b,c)
      = Alpha'(a,b,c)*f by Def18
     .= g*f by Def19
     .= <:pr1(a[x]b,c),pr2(a[x]b,c):> by A8,A13,A15,A19,A20,Th27
     .= id((a[x]b)[x]c) by Th26;
 end;

theorem
     (a[x]b)[x]c,a[x](b[x]c) are_isomorphic
 proof
  thus Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} & Hom(a[x](b[x]c),(a[x]b)[x]c) <> {}
    by Th38;
  take Alpha(a,b,c), Alpha'(a,b,c);
  thus thesis by Th39;
 end;

definition let C,a,b,c,d;
  let f be Morphism of a,b, g be Morphism of c,d;
 func f[x]g -> Morphism of a[x]c,b[x]d equals
:Def20:  <:f*pr1(a,c),g*pr2(a,c):>;
  correctness;
end;

theorem
     Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a[x]b,c[x]d) <> {}
 proof assume
A1: Hom(a,c) <> {} & Hom(b,d) <> {};
    Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21;
  then Hom(a[x]b,c) <> {} & Hom(a[x]b,d) <> {} by A1,CAT_1:52;
  hence thesis by Th25;
 end;

theorem
     (id a)[x](id b) = id(a[x]b)
 proof Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21;
  then (id a)*pr1(a,b) = pr1(a,b) & (id b)*pr2(a,b) = pr2(a,b) by CAT_1:57;
  then (id a)[x](id b) = <:pr1(a,b),pr2(a,b):> by Def20;
  hence thesis by Th26;
 end;

theorem Th43:
   for f being Morphism of a,b, h being Morphism of c,d,
       g being Morphism of e,a, k being Morphism of e,c
     st Hom(a,b) <> {} & Hom(c,d) <> {} & Hom(e,a) <> {} & Hom(e,c) <> {}
    holds (f[x]h)*<:g,k:> = <:f*g,h*k:>
 proof let f be Morphism of a,b, h be Morphism of c,d;
  let g be Morphism of e,a, k be Morphism of e,c;
  assume that
A1: Hom(a,b) <> {} and
A2: Hom(c,d) <> {} and
A3: Hom(e,a) <> {} and
A4: Hom(e,c) <> {};
A5: Hom(e,a[x]c) <> {} by A3,A4,Th25;
    Hom(a[x]c,a) <> {} & Hom(a[x]c,c) <> {} &
      pr1(a,c)*<:g,k:> = g & pr2(a,c)*<:g,k:> = k by A3,A4,Def11,Th21;
  then Hom(a[x]c,b) <> {} & Hom(a[x]c,d) <> {} &
       f*g = (f*pr1(a,c))*<:g,k:> & h*k = (h*pr2(a,c))*<:g,k:>
   by A1,A2,A5,CAT_1:52,54;
  then <:f*g,h*k:> = <:f*pr1(a,c),h*pr2(a,c):>*<:g,k:> by A5,Th27;
  hence thesis by Def20;
 end;

theorem
     for f being Morphism of c,a, g being Morphism of c,b
    st Hom(c,a) <> {} & Hom(c,b) <> {} holds <:f,g:> = (f[x]g)*Delta(c)
 proof let f be Morphism of c,a, g be Morphism of c,b such that
A1: Hom(c,a) <> {} and
A2: Hom(c,b) <> {};
A3: Hom(c,c) <> {} by CAT_1:56;
   thus (f[x]g)*Delta(c) = (f[x]g)*<:id c,id c:> by Def17
                        .= <:f*(id c),g*(id c):> by A1,A2,A3,Th43
                        .= <:f,g*(id c):> by A1,CAT_1:58
                        .= <:f,g:> by A2,CAT_1:58;
 end;

theorem
     for f being Morphism of a,b, h being Morphism of c,d,
       g being Morphism of e,a, k being Morphism of s,c
      st Hom(a,b) <> {} & Hom(c,d) <> {} & Hom(e,a) <> {} & Hom(s,c) <> {}
     holds (f[x]h)*(g[x]k) = (f*g)[x](h*k)
 proof let f be Morphism of a,b, h be Morphism of c,d;
  let g be Morphism of e,a, k be Morphism of s,c;
  assume that
A1: Hom(a,b) <> {} and
A2: Hom(c,d) <> {} and
A3: Hom(e,a) <> {} and
A4: Hom(s,c) <> {};
A5: Hom(e[x]s,e) <> {} & Hom(e[x]s,s) <> {} by Th21;
  then f*(g*pr1(e,s)) = (f*g)*pr1(e,s) & h*(k*pr2(e,s)) = (h*k)*pr2(e,s)
    by A1,A2,A3,A4,CAT_1:54;
  then Hom(e[x]s,a) <> {} & Hom(e[x]s,c) <> {} &
       (f*g)[x](h*k) = <:f*(g*pr1(e,s)),h*(k*pr2(e,s)):> &
       g[x]k = <:g*pr1(e,s),k*pr2(e,s):>
     by A3,A4,A5,Def20,CAT_1:52;
  hence thesis by A1,A2,Th43;
 end;

begin :: Categories with Finite Coproducts

definition let C be Category;
 attr C is with_finite_coproduct means
     for I being finite set, F being Function of I,the Objects of C
   ex a being Object of C, F' being Injections_family of a,I
    st doms F' = F & a is_a_coproduct_wrt F';
  synonym C has_finite_coproduct;
end;

theorem Th46:
   for C being Category holds
    C has_finite_coproduct iff
     (ex a being Object of C st a is initial) &
     for a,b being Object of C
      ex c being Object of C, i1,i2 being Morphism of C
       st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c &
        c is_a_coproduct_wrt i1,i2
 proof let C be Category;
  thus C has_finite_coproduct implies
    (ex a being Object of C st a is initial) &
    for a,b being Object of C
     ex c being Object of C, i1,i2 being Morphism of C
      st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c &
       c is_a_coproduct_wrt i1,i2
   proof assume
A1:  for I being finite set, F being Function of I,the Objects of C
     ex a being Object of C, F' being Injections_family of a,I
      st doms F' = F & a is_a_coproduct_wrt F';
    reconsider F = {} as Function of {},the Objects of C by FUNCT_2:55,RELAT_1:
60;
    consider a being Object of C, F' being Injections_family of a,{}
    such that doms F' = F and
A2:   a is_a_coproduct_wrt F' by A1;
      a is initial by A2,CAT_3:81;
    hence ex a being Object of C st a is initial;
    let a,b be Object of C;
    set F = (0,1)-->(a,b);
    consider c being Object of C, F' being Injections_family of c,{0,1}
    such that
A3:   doms F' = F and
A4:   c is_a_coproduct_wrt F' by A1;
    take c, i1 = F'/.0, i2 = F'/.1;
A5:   0 in {0,1} & 1 in {0,1} by TARSKI:def 2;
      F/.0 = a & F/.1 = b by CAT_3:7;
    hence dom i1 = a & dom i2 = b by A3,A5,CAT_3:def 3;
    thus cod i1 = c & cod i2 = c by A5,CAT_3:67;
A6:  dom F' = {0,1} by FUNCT_2:def 1;
      i1 = F'.0 & i2 = F'.1 by A5,CAT_3:def 1;
    then 0 <> 1 & F' = (0,1)-->(i1,i2) by A6,FUNCT_4:69;
    hence c is_a_coproduct_wrt i1,i2 by A4,CAT_3:85;
   end;
  given a being Object of C such that
A7: a is initial;
  assume
A8:  for a,b being Object of C
      ex c being Object of C, i1,i2 being Morphism of C
       st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c &
        c is_a_coproduct_wrt i1,i2;
 defpred Q[Nat] means
  for I being finite set, F being Function of I,the Objects of C
    st card I = $1
   ex a being Object of C, F' being Injections_family of a,I
    st doms F' = F & a is_a_coproduct_wrt F';
A9: Q[ 0 ]
  proof let I be finite set, F be Function of I,the Objects of C;
   assume A10: card I = 0;
then A11:  I = {} by CARD_2:59;
     {} is Function of {}, the Morphisms of C by FUNCT_2:55,RELAT_1:60;
   then reconsider F' = {} as Injections_family of a,I by A11,CAT_3:68;
   take a,F';
     for x being set st x in I holds (doms F')/.x = F/.x by A10,CARD_2:59;
   hence doms F' = F by CAT_3:1;
   thus thesis by A7,A11,CAT_3:81;
  end;
A12: for n being Nat st Q[n] holds Q[n+1]
   proof let n be Nat such that
A13:  Q[n];
    let I be finite set, F be Function of I,the Objects of C such that
A14:  card I = n+1;
    consider x being Element of I;
    reconsider Ix = I \ {x} as finite set;
A15: {x} c= I by A14,CARD_1:47,ZFMISC_1:37;
    reconsider sx = {x} as finite set;
A16:   card(Ix) = card(I) - card(sx) by A15,CARD_2:63
                 .= card(I) - 1 by CARD_1:79
                 .= n by A14,XCMPLX_1:26;
A17:  I\{x} c= I & the Objects of C <> {} by XBOOLE_1:36;
    then reconsider G = F|(I\{x}) as Function of I\{x},the Objects of C
     by FUNCT_2:38;
    consider a being Object of C, G' being Injections_family of a,I\{x}
    such that
A18:   doms G' = G and
A19:   a is_a_coproduct_wrt G' by A13,A16;
    set b = F/.x;
    consider c being Object of C, i1,i2 being Morphism of C
     such that
A20:   dom i1 = a & dom i2 = b and
A21:   cod i1 = c & cod i2 = c and
A22:  c is_a_coproduct_wrt i1,i2 by A8;
    set F' = (i1*G') +* ({x} -->i2);
A23:    dom(i1*G') = I\{x} & dom({x} -->i2) = {x} by FUNCT_2:def 1;
    then A24: dom(i1*G') \/ dom({x} -->i2) = I \/ {x} by XBOOLE_1:39
                                    .= I by A14,CARD_1:47,ZFMISC_1:46;
    then A25:  dom F' = I by FUNCT_4:def 1;
A26:  rng F' c= rng(i1*G') \/ rng({x} -->i2) by FUNCT_4:18;
      rng(i1*G') c= the Morphisms of C & rng({x} -->i2) c= the Morphisms of C
     by RELSET_1:12;
    then rng(i1*G') \/ rng({x} -->i2) c= the Morphisms of C by XBOOLE_1:8;
    then rng F' c= the Morphisms of C by A26,XBOOLE_1:1;
    then reconsider F' as Function of I, the Morphisms of C
     by A25,FUNCT_2:def 1,RELSET_1:11;
A27:  cods G' = (I\{x})-->a by CAT_3:def 17;
      now let y be set;
     assume
A28:     y in I;
       now per cases;
      suppose y = x;
then A29:      y in {x} by TARSKI:def 1;
         F'/.y = F'.y by A28,CAT_3:def 1
            .= ({x} -->i2).y by A23,A29,FUNCT_4:14
            .= i2 by A29,FUNCOP_1:13;
       hence (I --> c).y = cod(F'/.y) by A21,A28,FUNCOP_1:13
                        .= (cods F')/.y by A28,CAT_3:def 4;
      suppose
A30:      y <> x;
then A31:      not y in {x} by TARSKI:def 1;
A32:      y in I\{x} by A28,A30,ZFMISC_1:64;
         F'/.y = F'.y by A28,CAT_3:def 1
            .= (i1*G').y by A23,A24,A28,A31,FUNCT_4:def 1
            .= (i1*G')/.y by A32,CAT_3:def 1;
       hence (cods F')/.y = cod((i1*G')/.y) by A28,CAT_3:def 4
                         .= (cods(i1*G'))/.y by A32,CAT_3:def 4
                         .= ((I\{x})-->c)/.y by A20,A21,A27,CAT_3:21
                         .= c by A32,CAT_3:2
                         .= (I --> c).y by A28,FUNCOP_1:13;
     end;
     hence (cods F').y = (I --> c).y by A28,CAT_3:def 1;
    end;
    then cods F' = I --> c by FUNCT_2:18;
    then reconsider F' as Injections_family of c,I by CAT_3:def 17;
    take c,F';
      now let y be set;
     assume
A33:     y in I;
       now per cases;
      suppose
A34:      y = x;
then A35:      y in {x} by TARSKI:def 1;
         F'/.y = F'.y by A33,CAT_3:def 1
            .= ({x} -->i2).y by A23,A35,FUNCT_4:14
            .= i2 by A35,FUNCOP_1:13;
       hence (doms F')/.y = F/.y by A20,A33,A34,CAT_3:def 3;
      suppose
A36:      y <> x;
then A37:      not y in {x} by TARSKI:def 1;
A38:      y in I\{x} by A33,A36,ZFMISC_1:64;
         F'/.y = F'.y by A33,CAT_3:def 1
            .= (i1*G').y by A23,A24,A33,A37,FUNCT_4:def 1
            .= (i1*G')/.y by A38,CAT_3:def 1;
       hence (doms F')/.y = dom((i1*G')/.y) by A33,CAT_3:def 3
                         .= (doms(i1*G'))/.y by A38,CAT_3:def 3
                         .= G/.y by A18,A20,A27,CAT_3:21
                         .= G.y by A38,CAT_3:def 1
                         .= F.y by A38,FUNCT_1:72
                         .= F/.y by A33,CAT_3:def 1;
     end;
     hence (doms F')/.y = F/.y;
    end;
    hence
A39:  doms F' = F by CAT_3:1;
    thus F' is Injections_family of c,I;
    let d be Object of C;
    let F'' be Injections_family of d,I such that
A40:  doms F' = doms F'';
    reconsider G'' = F''|(I\{x}) as Function of I\{x},the Morphisms of C
     by A17,FUNCT_2:38;
      now let y be set;
     assume
A41:    y in I\{x};
then A42:    y in I by XBOOLE_0:def 4;
       G''/.y = G''.y by A41,CAT_3:def 1
           .= F''.y by A41,FUNCT_1:72
           .= F''/.y by A42,CAT_3:def 1;
     hence cods(G'')/.y = cod(F''/.y) by A41,CAT_3:def 4
                       .= d by A42,CAT_3:67
                       .= ((I\{x})-->d)/.y by A41,CAT_3:2;
    end;
    then cods G'' = I\{x} --> d by CAT_3:1;
    then reconsider G'' as Injections_family of d,I\{x} by CAT_3:def 17;
      now let y be set;
     assume
A43:    y in I\{x};
then A44:    y in I by XBOOLE_0:def 4;
then A45:  F''/.y = F''.y by CAT_3:def 1
           .= G''.y by A43,FUNCT_1:72
           .= G''/.y by A43,CAT_3:def 1;
       G/.y = G.y by A43,CAT_3:def 1
         .= F.y by A43,FUNCT_1:72
         .= F/.y by A44,CAT_3:def 1;
     hence (doms G')/.y = dom(G''/.y) by A18,A39,A40,A44,A45,CAT_3:def 3
                       .= (doms G'')/.y by A43,CAT_3:def 3;
    end;
    then doms G' = doms G'' by CAT_3:1;
    then consider h' being Morphism of C such that
A46:  h' in Hom(a,d) and
A47:  for k being Morphism of C st k in Hom(a,d) holds
       (for y being set st y in I\{x} holds k*(G'/.y) = G''/.y) iff h' = k
       by A19,CAT_3:def 18;
   set g = F''/.x;
A48:  cod g = d by A14,CARD_1:47,CAT_3:67;
A49:  x in {x} by TARSKI:def 1;
A50:  F'/.x = F'.x by A14,CARD_1:47,CAT_3:def 1
        .= ({x} -->i2).x by A23,A49,FUNCT_4:14
        .= i2 by A49,FUNCOP_1:13;
   then dom i2 = (doms F')/.x by A14,CARD_1:47,CAT_3:def 3
              .= dom g by A14,A40,CARD_1:47,CAT_3:def 3;
   then g in Hom(dom i2,d) by A48,CAT_1:18;
   then consider h being Morphism of C such that
A51:  h in Hom(c,d) and
A52:  for k being Morphism of C st k in Hom(c,d)
       holds k*i1 = h' & k*i2 = g iff h = k by A20,A22,A46,CAT_3:def 19;
    take h;
    thus h in Hom(c,d) by A51;
    let k be Morphism of C such that
A53:  k in Hom(c,d);
    thus (for y being set st y in I holds k*(F'/.y) = F''/.y) implies h = k
     proof assume
A54:     for y being set st y in I holds k*(F'/.y) = F''/.y;
      then A55:     k*i2 = g by A14,A50,CARD_1:47;
A56:     cod k = d & dom k = c by A53,CAT_1:18;
        then cod(k*i1) = d & dom(k*i1) = a by A20,A21,CAT_1:42;
then A57:     k*i1 in Hom(a,d) by CAT_1:18;
        for y being set st y in I\{x} holds k*i1*(G'/.y) = G''/.y
       proof let y be set;
        assume
A58:       y in I\{x};
then A59:      y in I & not y in {x} by XBOOLE_0:def 4;
then A60:      F'/.y = F'.y by CAT_3:def 1
             .= (i1*G').y by A23,A24,A59,FUNCT_4:def 1
             .= (i1*G')/.y by A58,CAT_3:def 1;
          cod(G'/.y) = a by A58,CAT_3:67;
        hence k*i1*(G'/.y) = k*(i1*(G'/.y)) by A20,A21,A56,CAT_1:43
                          .= k*((i1*G')/.y) by A58,CAT_3:def 8
                          .= F''/.y by A54,A59,A60
                          .= F''.y by A59,CAT_3:def 1
                          .= G''.y by A58,FUNCT_1:72
                          .= G''/.y by A58,CAT_3:def 1;
       end;
      then k*i1 = h' by A47,A57;
      hence h = k by A52,A53,A55;
     end;
    assume
A61:  h = k;
    let y be set such that
A62:  y in I;
       now per cases;
      suppose
A63:     y = x;
then A64:     y in {x} by TARSKI:def 1;
         F'/.y = F'.y by A62,CAT_3:def 1
            .= ({x} -->i2).y by A23,A64,FUNCT_4:14
            .= i2 by A64,FUNCOP_1:13;
       hence thesis by A52,A53,A61,A63;
      suppose
A65:     y <> x;
then A66:     not y in {x} by TARSKI:def 1;
A67:     y in I\{x} by A62,A65,ZFMISC_1:64;
then A68:     dom k = c & cod(G'/.y) = a by A53,CAT_1:18,CAT_3:67;
         F'/.y = F'.y by A62,CAT_3:def 1
            .= (i1*G').y by A23,A24,A62,A66,FUNCT_4:def 1
            .= (i1*G')/.y by A67,CAT_3:def 1
            .= i1*(G'/.y) by A67,CAT_3:def 8;
       hence k*(F'/.y) = k*i1*(G'/.y) by A20,A21,A68,CAT_1:43
                      .= h'*(G'/.y) by A52,A53,A61
                      .= G''/.y by A46,A47,A67
                      .= G''.y by A67,CAT_3:def 1
                      .= F''.y by A67,FUNCT_1:72
                      .= F''/.y by A62,CAT_3:def 1;
     end;
    hence thesis;
   end;
A69: for n being Nat holds Q[n] from Ind(A9,A12);
  let I be finite set, F be Function of I,the Objects of C;
    card I = card I;
  hence thesis by A69;
 end;

definition
  struct (CatStr)CoprodCatStr
   (# Objects,Morphisms -> non empty set,
     Dom,Cod -> Function of the Morphisms, the Objects,
     Comp -> PartFunc of [:the Morphisms, the Morphisms :],the Morphisms,
     Id -> Function of the Objects, the Morphisms,
     Initial -> Element of the Objects,
     Coproduct -> Function of [:the Objects,the Objects:],the Objects,
     Incl1,Incl2 -> Function of [:the Objects,the Objects:],the Morphisms
   #);
end;

definition let C be CoprodCatStr;
 func [0]C -> Object of C equals
:Def22:  the Initial of C;
   correctness;
  let a,b be Object of C;
 func a+b -> Object of C equals
:Def23:  (the Coproduct of C).[a,b];
   correctness;
 func in1(a,b) -> Morphism of C equals
:Def24:  (the Incl1 of C).[a,b];
   correctness;
 func in2(a,b) -> Morphism of C equals
:Def25:  (the Incl2 of C).[a,b];
   correctness;
end;

definition let o,m;
 func c1Cat*(o,m) -> strict CoprodCatStr equals
:Def26:  CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
                 Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #);
 correctness;
end;

theorem
     the CatStr of c1Cat*(o,m) = 1Cat(o,m)
 proof
    c1Cat*(o,m) = CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
                      Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def26;
  hence thesis by CAT_1:def 9;
 end;

Lm2: c1Cat*(o,m) is Category-like
 proof
  set C = c1Cat*(o,m);
A1: C = CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
                      Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def26;
  set CP = the Comp of C, CD = the Dom of C, CC = the Cod of C,
      CI = the Id of C;
  thus for f,g being Morphism of C holds
      [g,f] in dom CP iff CD.g=CC.f
    proof let f,g be Morphism of C;
       f = m & g = m & dom CP = {[m,m]} by A1,CAT_1:7,TARSKI:def 1;
     hence thesis by A1,TARSKI:def 1;
    end;
  thus for f,g being Morphism of C
    st CD.g=CC.f holds CD.(CP.[g,f]) = CD.f & CC.(CP.[g,f]) = CC.g
    proof let f,g be Morphism of C;
       CP.[g,f] = m by A1,CAT_1:9;
     then reconsider gf = CP.[g,f] as Morphism of C by A1,TARSKI:def 1;
       CD.f = o & CC.g = o & CD.gf = o & CC.gf = o by A1,FUNCT_2:65;
     hence thesis;
    end;
  thus for f,g,h being Morphism of C
      st CD.h = CC.g & CD.g = CC.f
     holds CP.[h,CP.[g,f]] = CP.[CP.[h,g],f]
   proof let f,g,h be Morphism of C;
       CP.[g,f] = m & CP.[h,g] = m by A1,CAT_1:9;
     then reconsider gf = CP.[g,f],hg = CP.[h,g] as Morphism of C
      by A1,TARSKI:def 1; CP.[h,gf] = m & CP.[hg,f] = m by A1,CAT_1:9;
    hence thesis;
   end;
  let b be Object of C;
    b = o by A1,TARSKI:def 1;
  hence CD.(CI.b) = b & CC.(CI.b) = b by A1,FUNCT_2:65;
  thus for f being Morphism of C st CC.f = b holds CP.[CI.b,f] = f
    proof let f be Morphism of C; f = m by A1,TARSKI:def 1;
     hence thesis by A1,CAT_1:9;
    end;
  let g be Morphism of C;
  assume CD.g = b;
    g = m by A1,TARSKI:def 1; hence CP.[g,CI.b] = g by A1,CAT_1:9;
 end;

definition
 cluster strict Category-like CoprodCatStr;
  existence
 proof c1Cat*(0,1) is Category-like by Lm2; hence thesis; end;
end;

definition let o,m be set;
 cluster c1Cat*(o,m) -> Category-like;
  coherence by Lm2;
end;

theorem Th48:
   for a being Object of c1Cat*(o,m) holds a = o
 proof let a be Object of c1Cat*(o,m);
    c1Cat*(o,m) = CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
                       Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def26;
  hence thesis by TARSKI:def 1;
 end;

theorem Th49:
   for a,b being Object of c1Cat*(o,m) holds a = b
 proof let a,b be Object of c1Cat*(o,m);
    a = o & b = o by Th48; hence thesis;
 end;

theorem Th50:
   for f being Morphism of c1Cat*(o,m) holds f = m
 proof let f be Morphism of c1Cat*(o,m);
    c1Cat*(o,m) = CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
                       Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def26;
  hence thesis by TARSKI:def 1;
 end;

theorem Th51:
   for f,g being Morphism of c1Cat*(o,m) holds f = g
 proof let f,g be Morphism of c1Cat*(o,m);
    f = m & g = m by Th50; hence thesis;
 end;

theorem Th52:
   for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*(o,m)
     holds f in Hom(a,b)
 proof let a,b be Object of c1Cat*(o,m), f be Morphism of c1Cat*(o,m);
    dom f = o & cod f = o by Th48; then dom f = a & cod f = b by Th48;
  hence f in Hom(a,b) by CAT_1:18;
 end;

theorem
     for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*(o,m)
    holds f is Morphism of a,b
 proof let a,b be Object of c1Cat*(o,m), f be Morphism of c1Cat*(o,m);
    f in Hom(a,b) by Th52; hence thesis by CAT_1:def 7;
 end;

theorem
    for a,b being Object of c1Cat*(o,m) holds Hom(a,b) <> {} by Th52;

theorem Th55:
   for a being Object of c1Cat*(o,m) holds a is initial
 proof let a be Object of c1Cat*(o,m);
  let b be Object of c1Cat*(o,m);
  thus Hom(a,b)<>{} by Th52;
  consider f being Morphism of a,b;
  take f; thus thesis by Th51;
 end;

theorem Th56:
   for c being Object of c1Cat*(o,m),
    i1,i2 being Morphism of c1Cat*(o,m) holds c is_a_coproduct_wrt i1,i2
 proof
  let c be Object of c1Cat*(o,m), i1,i2 be Morphism of c1Cat*(o,m);
  thus cod i1 = c & cod i2 = c by Th49;
  let d be Object of c1Cat*(o,m), f,g be Morphism of c1Cat*(o,m) such that
   f in Hom(dom i1,d) & g in Hom(dom i2,d);
  take h = i1;
  thus h in Hom(c,d) by Th52;
  thus thesis by Th51;
 end;

definition let IT be Category-like CoprodCatStr;
 attr IT is Cocartesian means
:Def27:
  the Initial of IT is initial &
  for a,b being Object of IT holds
     dom((the Incl1 of IT).[a,b]) = a & dom((the Incl2 of IT).[a,b]) = b &
     (the Coproduct of IT).[a,b]
       is_a_coproduct_wrt (the Incl1 of IT).[a,b],(the Incl2 of IT).[a,b];
end;

theorem Th57:
   for o,m being set holds c1Cat*(o,m) is Cocartesian
 proof let o,m be set;
  set 1PCat = c1Cat*(o,m);
  thus the Initial of 1PCat is initial by Th55;
  let a,b be Object of 1PCat;
  thus dom((the Incl1 of 1PCat).[a,b]) = a by Th49;
  thus dom((the Incl2 of 1PCat).[a,b]) = b by Th49;
  thus (the Coproduct of 1PCat).[a,b]
    is_a_coproduct_wrt (the Incl1 of 1PCat).[a,b],(the Incl2 of 1PCat).[a,b]
   by Th56;
 end;

definition
 cluster strict Cocartesian (Category-like CoprodCatStr);
  existence
 proof c1Cat*(0,1) is Cocartesian by Th57;
  hence thesis;
 end;
end;

definition
  mode Cocartesian_category is Cocartesian (Category-like CoprodCatStr);
end;

reserve C for Cocartesian_category;
reserve a,b,c,d,e,s for Object of C;

theorem Th58:
   [0]C is initial
 proof [0]C = the Initial of C by Def22; hence thesis by Def27; end;

theorem Th59:
   for f1,f2 being Morphism of [0]C,a holds f1 = f2
 proof let f1,f2 be Morphism of [0]C,a;
    [0]C is initial by Th58;
  then consider f being Morphism of [0]C,a such that
A1: for g being Morphism of [0]C, a holds f = g by CAT_1:def 16;
  thus f1 = f by A1 .= f2 by A1;
 end;

definition let C,a;
 func init a -> Morphism of [0]C, a means not contradiction;
  existence;
  uniqueness by Th59;
end;

theorem Th60:
   Hom([0]C,a) <> {}
 proof [0]C is initial by Th58; hence thesis by CAT_1:def 16; end;

theorem Th61:
   init a = init([0]C,a)
 proof [0]C is initial by Th58; hence thesis by CAT_3:44; end;

theorem
     dom(init a) = [0]C & cod(init a) = a
 proof [0]C is initial & init a = init([0]C,a) by Th58,Th61;
  hence thesis by CAT_3:42;
 end;

theorem
     Hom([0]C,a) = {init a}
 proof
A1: Hom([0]C,a) <> {} by Th60;
    for f2 being Morphism of [0]C,a holds init a = f2 by Th59;
  hence thesis by A1,CAT_1:26;
 end;

theorem Th64:
   dom in1(a,b) = a & cod in1(a,b) = a+b
 proof
  set i1 = (the Incl1 of C).[a,b], i2 = (the Incl2 of C).[a,b];
    (the Coproduct of C).[a,b] is_a_coproduct_wrt i1,i2 by Def27;
  then a+b is_a_coproduct_wrt i1,i2 by Def23;
  then cod i1 = a+b & dom i1 = a by Def27,CAT_3:def 19;
  hence thesis by Def24;
 end;

theorem Th65:
   dom in2(a,b) = b & cod in2(a,b) = a+b
 proof
  set i1 = (the Incl1 of C).[a,b], i2 = (the Incl2 of C).[a,b];
    (the Coproduct of C).[a,b] is_a_coproduct_wrt i1,i2 by Def27;
  then a+b is_a_coproduct_wrt i1,i2 by Def23;
  then cod i2 = a+b & dom i2 = b by Def27,CAT_3:def 19;
  hence thesis by Def25;
 end;

theorem Th66:
   Hom(a,a+b) <> {} & Hom(b,a+b) <> {}
 proof
  set c = (the Coproduct of C).[a,b];
  set i1 = (the Incl1 of C).[a,b], i2 = (the Incl2 of C).[a,b];
    c is_a_coproduct_wrt i1,i2 by Def27;
  then cod i1 = c & cod i2 = c & dom(i1) = a & dom(i2) = b
   by Def27,CAT_3:def 19;
  then Hom(a,c) <> {} & Hom(b,c) <> {} by CAT_1:18;
  hence thesis by Def23;
 end;

theorem Th67:
   a+b is_a_coproduct_wrt in1(a,b),in2(a,b)
 proof
  set i1 = (the Incl1 of C).[a,b], i2 = (the Incl2 of C).[a,b];
    (the Coproduct of C).[a,b] = a+b & i1 = in1(a,b) & i2 = in2(a,b)
    by Def23,Def24,Def25;
  hence thesis by Def27;
 end;

theorem
     C has_finite_coproduct
 proof
A1:   [0]C is initial by Th58;
    for a,b
   ex c being Object of C, i1,i2 being Morphism of C
    st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c &
     c is_a_coproduct_wrt i1,i2
   proof let a,b;
    take a+b, in1(a,b), in2(a,b);
    thus thesis by Th64,Th65,Th67;
   end;
  hence thesis by A1,Th46;
 end;

theorem
     Hom(a,b) <> {} & Hom(b,a) <> {}
    implies in1(a,b) is coretraction & in2(a,b) is coretraction
 proof
    a+b is_a_coproduct_wrt in1(a,b),in2(a,b) &
   dom in1(a,b) = a & dom in2(a,b) = b by Th64,Th65,Th67;
  hence thesis by CAT_3:88;
 end;

definition let C,a,b; redefine
 func in1(a,b) -> Morphism of a,a+b;
  coherence
 proof cod in1(a,b) = a+b & dom in1(a,b) = a by Th64;
  hence thesis by CAT_1:22;
 end;
 func in2(a,b) -> Morphism of b,a+b;
  coherence
 proof cod in2(a,b) = a+b & dom in2(a,b) = b by Th65;
  hence thesis by CAT_1:22;
 end;
end;

definition let C,a,b,c;
  let f be Morphism of a,c, g be Morphism of b,c;
assume A1: Hom(a,c) <> {} & Hom(b,c) <> {};
 func [$f,g$] -> Morphism of a+b,c means
:Def29:  it*in1(a,b) = f & it*in2(a,b) = g;
  existence
 proof Hom(a,a+b) <> {} & Hom(b,a+b) <> {} &
  a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Th66,Th67;
  then consider h being Morphism of a+b,c such that
A2: for k being Morphism of a+b,c
     holds k*in1(a,b) = f & k*in2(a,b) = g iff h = k by A1,CAT_3:87;
  take h; thus thesis by A2;
 end;
  uniqueness
 proof let h1,h2 be Morphism of a+b,c such that
A3: h1*in1(a,b) = f & h1*in2(a,b) = g and
A4: h2*in1(a,b) = f & h2*in2(a,b) = g;
    a+b is_a_coproduct_wrt in1(a,b),in2(a,b) &
   Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th66,Th67;
  then consider h being Morphism of a+b,c such that
A5: for k being Morphism of a+b,c
     holds k*in1(a,b) = f & k*in2(a,b) = g iff h = k by A1,CAT_3:87;
    h1 = h & h2 = h by A3,A4,A5;
  hence thesis;
 end;
end;

theorem Th70:
   Hom(a,c) <> {} & Hom(b,c) <> {} implies Hom(a+b,c) <> {}
 proof Hom(a,a+b) <> {} & Hom(b,a+b) <> {} &
  a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Th66,Th67;
  hence thesis by CAT_3:87;
 end;

theorem Th71:
   [$in1(a,b),in2(a,b)$] = id(a+b)
 proof
A1: Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th66;
  then (id(a+b))*in1(a,b) = in1(a,b) & (id(a+b))*in2(a,b) = in2(a,b)
    by CAT_1:57;
  hence thesis by A1,Def29;
 end;

theorem Th72:
  for f being Morphism of a,c, g being Morphism of b,c, h being Morphism of c,d
     st Hom(a,c)<>{} & Hom(b,c)<>{} & Hom(c,d)<>{}
    holds [$h*f,h*g$] = h*[$f,g$]
 proof let f be Morphism of a,c, g be Morphism of b,c, h be Morphism of c,d;
  assume that
A1: Hom(a,c)<>{} and
A2: Hom(b,c)<>{} and
A3: Hom(c,d)<>{};
    Hom(a,a+b) <> {} & Hom(b,a+b) <> {} & Hom(a+b,c) <> {} &
   h*([$f,g$]*in1(a,b)) = h*f & h*([$f,g$]*in2(a,b)) = h*g
     by A1,A2,Def29,Th66,Th70;
  then h*[$f,g$]*in1(a,b) = h*f & h*[$f,g$]*in2(a,b) = h*g &
    Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A3,CAT_1:52,54;
  hence thesis by Def29;
 end;

theorem Th73:
   for f,k being Morphism of a,c, g,h being Morphism of b,c
     st Hom(a,c) <> {} & Hom(b,c) <> {} & [$f,g$] = [$k,h$]
    holds f = k & g = h
 proof let f,k be Morphism of a,c, g,h be Morphism of b,c;
  assume Hom(a,c) <> {} & Hom(b,c) <> {};
  then [$f,g$]*in1(a,b) = f & [$k,h$]*in1(a,b) = k &
     [$f,g$]*in2(a,b) = g & [$k,h$]*in2(a,b) = h by Def29;
  hence thesis;
 end;

theorem
     for f being Morphism of a,c, g being Morphism of b,c
    st Hom(a,c) <> {} & Hom(b,c) <> {} & (f is epi or g is epi)
   holds [$f,g$] is epi
 proof
  let f be Morphism of a,c, g be Morphism of b,c;
  assume that
A1: Hom(a,c) <> {} and
A2: Hom(b,c) <> {} and
A3: f is epi or g is epi;
A4: now assume
A5:   f is epi;
     let d;
     let f1,f2 be Morphism of c,d such that
A6:   Hom(c,d)<>{} and
A7:   f1*[$f,g$] = f2*[$f,g$];
       [$f1*f,f1*g$] = f1*[$f,g$] & [$f2*f,f2*g$] = f2*[$f,g$] &
      Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A6,Th72,CAT_1:52;
     then f1*f = f2*f by A7,Th73;
     hence f1 = f2 by A1,A5,A6,CAT_1:65;
    end;
A8: Hom(a+b,c) <> {} by A1,A2,Th70;
     now assume
A9:  g is epi;
    let d be Object of C, f1,f2 be Morphism of c,d such that
A10:  Hom(c,d)<>{} and
A11:  f1*[$f,g$] = f2*[$f,g$];
      [$f1*f,f1*g$] = f1*[$f,g$] & [$f2*f,f2*g$] = f2*[$f,g$] &
      Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A10,Th72,CAT_1:52;
    then f1*g = f2*g by A11,Th73;
    hence f1 = f2 by A2,A9,A10,CAT_1:65;
   end;
  hence thesis by A3,A4,A8,CAT_1:65;
 end;

theorem
     a, a+[0]C are_isomorphic & a,[0]C+a are_isomorphic
 proof
A1: Hom([0]C,a) <> {} & Hom(a,a) <> {} by Th60,CAT_1:56;
   thus a,a+[0]C are_isomorphic
    proof thus
A2:    Hom(a,a+[0]C) <> {} by Th66;
     thus Hom(a+[0]C,a) <> {} by A1,Th70;
     take g = in1(a,[0]C), f = [$id a,init a$];
       in1(a,[0]C)*id(a) = in1(a,[0]C) & in1(a,[0]C)*init a = in2(a,[0]C)
       & Hom([0]C,a+[0]C)<>{} by A2,Th59,Th66,CAT_1:58;
     then g*f = [$in1(a,[0]C),in2(a,[0]C)$] by A1,A2,Th72;
     hence thesis by A1,Def29,Th71;
    end;
   thus
A3: Hom(a,[0]C+a) <> {} by Th66;
   thus Hom([0]C+a,a) <> {} by A1,Th70;
   take g = in2([0]C,a), f = [$init a,id a$];
     in2([0]C,a)*id(a) = in2([0]C,a) & in2([0]C,a)*init a = in1([0]C,a)
     & Hom([0]C,[0]C+a)<>{} by A3,Th59,Th66,CAT_1:58;
   then g*f = [$in1([0]C,a),in2([0]C,a)$] by A1,A3,Th72;
   hence thesis by A1,Def29,Th71;
 end;

theorem
     a+b,b+a are_isomorphic
 proof
A1: Hom(a,b+a) <> {} & Hom(b,b+a) <> {} by Th66;
  hence
A2: Hom(a+b,b+a)<>{} by Th70;
A3: Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th66;
  hence
A4: Hom(b+a,a+b)<>{} by Th70;
  take f' = [$in2(b,a),in1(b,a)$], f = [$in2(a,b),in1(a,b)$];
  thus f'*f
     = [$f'*in2(a,b),f'*in1(a,b)$] by A2,A3,Th72
    .= [$in1(b,a),f'*in1(a,b)$] by A1,Def29
    .= [$in1(b,a),in2(b,a)$] by A1,Def29
    .= id(b+a) by Th71;
  thus f*f'
     = [$f*in2(b,a),f*in1(b,a)$] by A1,A4,Th72
    .= [$in1(a,b),f*in1(b,a)$] by A3,Def29
    .= [$in1(a,b),in2(a,b)$] by A3,Def29
    .= id(a+b) by Th71;
 end;

theorem
     (a+b)+c,a+(b+c) are_isomorphic
 proof
A1: Hom(b,b+c) <> {} by Th66;
A2: Hom(b+c,a+(b+c)) <> {} by Th66;
then A3: Hom(b,a+(b+c)) <> {} by A1,CAT_1:52;
A4: Hom(c,b+c) <> {} by Th66;
then A5: Hom(c,a+(b+c)) <> {} by A2,CAT_1:52;
A6: Hom(a,a+(b+c)) <> {} by Th66;
then A7: Hom(a+b,a+(b+c)) <> {} by A3,Th70;
  hence
A8: Hom((a+b)+c,a+(b+c)) <> {} by A5,Th70;
A9: Hom(a,a+b) <> {} by Th66;
A10: Hom(a+b,(a+b)+c) <> {} by Th66;
then A11: Hom(a,(a+b)+c) <> {} by A9,CAT_1:52;
A12: Hom(b,a+b) <> {} by Th66;
then A13: Hom(b,(a+b)+c) <> {} by A10,CAT_1:52;
A14: Hom(c,(a+b)+c) <> {} by Th66;
then A15: Hom(b+c,(a+b)+c) <> {} by A13,Th70;
  hence
A16: Hom(a+(b+c),(a+b)+c) <> {} by A11,Th70;
  set k = [$in1(a+b,c)*in2(a,b),in2(a+b,c)$];
  set l = [$in1(a,b+c),in2(a,b+c)*in1(b,c)$];
  take g = [$l,in2(a,b+c)*in2(b,c)$];
  take f = [$in1(a+b,c)*in1(a,b),k$];
    now
   thus g*(in1(a+b,c)*in1(a,b))
      = g*in1(a+b,c)*in1(a,b) by A8,A9,A10,CAT_1:54
     .= l*in1(a,b) by A5,A7,Def29
     .= in1(a,b+c) by A3,A6,Def29;
     g*(in1(a+b,c)*in2(a,b)) = (g*in1(a+b,c))*in2(a,b) by A8,A10,A12,CAT_1:54
                          .= l*in2(a,b) by A5,A7,Def29
                          .= in2(a,b+c)*in1(b,c) by A3,A6,Def29;
   hence g*k
       = [$in2(a,b+c)*in1(b,c),g*in2(a+b,c)$] by A8,A13,A14,Th72
      .= [$in2(a,b+c)*in1(b,c),in2(a,b+c)*in2(b,c)$] by A5,A7,Def29
      .= in2(a,b+c)*[$in1(b,c),in2(b,c)$] by A1,A2,A4,Th72
      .= in2(a,b+c)*id(b+c) by Th71
      .= in2(a,b+c) by A2,CAT_1:58;
  end;
  hence g*f = [$in1(a,b+c),in2(a,b+c)$] by A8,A11,A15,Th72
           .= id(a+(b+c)) by Th71;
    now
     f*(in2(a,b+c)*in1(b,c)) = (f*in2(a,b+c))*in1(b,c) by A1,A2,A16,CAT_1:54
                          .= k*in1(b,c) by A11,A15,Def29
                          .= in1(a+b,c)*in2(a,b) by A13,A14,Def29;
   hence f*l
       = [$f*in1(a,b+c),in1(a+b,c)*in2(a,b)$] by A3,A6,A16,Th72
      .= [$in1(a+b,c)*in1(a,b),in1(a+b,c)*in2(a,b)$] by A11,A15,Def29
      .= in1(a+b,c)*[$in1(a,b),in2(a,b)$] by A9,A10,A12,Th72
      .= in1(a+b,c)*id(a+b) by Th71
      .= in1(a+b,c) by A10,CAT_1:58;
   thus f*(in2(a,b+c)*in2(b,c))
      = (f*in2(a,b+c))*in2(b,c) by A2,A4,A16,CAT_1:54
     .= k*in2(b,c) by A11,A15,Def29
     .= in2(a+b,c) by A13,A14,Def29;
  end;
  hence f*g = [$in1(a+b,c),in2(a+b,c)$] by A5,A7,A16,Th72
           .= id((a+b)+c) by Th71;
 end;

definition let C,a;
 func nabla a -> Morphism of a+a,a equals
:Def30:  [$id a,id a$];
  correctness;
end;

definition let C,a,b,c,d;
  let f be Morphism of a,c, g be Morphism of b,d;
 func f+g -> Morphism of a+b,c+d equals
:Def31:  [$in1(c,d)*f,in2(c,d)*g$];
  correctness;
end;

theorem
     Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a+b,c+d) <> {}
 proof assume
A1: Hom(a,c) <> {} & Hom(b,d) <> {};
    Hom(c,c+d) <> {} & Hom(d,c+d) <> {} by Th66;
  then Hom(a,c+d) <> {} & Hom(b,c+d) <> {} by A1,CAT_1:52;
  hence thesis by Th70;
 end;

theorem
     (id a)+(id b) = id(a+b)
 proof Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th66;
  then in1(a,b)*(id a) = in1(a,b) & in2(a,b)*(id b) = in2(a,b) by CAT_1:58;
  then (id a)+(id b) = [$in1(a,b),in2(a,b)$] by Def31;
  hence thesis by Th71;
 end;

theorem Th80:
   for f being Morphism of a,c, h being Morphism of b,d,
       g being Morphism of c,e, k being Morphism of d,e
     st Hom(a,c) <> {} & Hom(b,d) <> {} & Hom(c,e) <> {} & Hom(d,e) <> {}
    holds [$g,k$]*(f+h) = [$g*f,k*h$]
 proof let f be Morphism of a,c, h be Morphism of b,d;
  let g be Morphism of c,e, k be Morphism of d,e;
  assume that
A1: Hom(a,c) <> {} and
A2: Hom(b,d) <> {} and
A3: Hom(c,e) <> {} and
A4: Hom(d,e) <> {};
A5: Hom(c+d,e) <> {} by A3,A4,Th70;
    Hom(c,c+d) <> {} & Hom(d,c+d) <> {} &
      [$g,k$]*in1(c,d) = g & [$g,k$]*in2(c,d) = k by A3,A4,Def29,Th66;
  then Hom(a,c+d) <> {} & Hom(b,c+d) <> {} &
       g*f = [$g,k$]*(in1(c,d)*f) & k*h = [$g,k$]*(in2(c,d)*h)
   by A1,A2,A5,CAT_1:52,54;
  then [$g*f,k*h$] = [$g,k$]*[$in1(c,d)*f,in2(c,d)*h$] by A5,Th72;
  hence thesis by Def31;
 end;

theorem
     for f being Morphism of a,c, g being Morphism of b,c
    st Hom(a,c) <> {} & Hom(b,c) <> {} holds nabla(c)*(f+g) = [$f,g$]
 proof let f be Morphism of a,c, g be Morphism of b,c such that
A1: Hom(a,c) <> {} and
A2: Hom(b,c) <> {};
A3: Hom(c,c) <> {} by CAT_1:56;
  thus nabla(c)*(f+g) = [$id c,id c$]*(f+g) by Def30
                     .= [$(id c)*f,(id c)*g$] by A1,A2,A3,Th80
                     .= [$f,(id c)*g$] by A1,CAT_1:57
                     .= [$f,g$] by A2,CAT_1:57;
 end;

theorem
     for f being Morphism of a,c, h being Morphism of b,d,
       g being Morphism of c,e, k being Morphism of d,s
      st Hom(a,c) <> {} & Hom(b,d) <> {} & Hom(c,e) <> {} & Hom(d,s) <> {}
     holds (g+k)*(f+h) = (g*f)+(k*h)
 proof let f be Morphism of a,c, h be Morphism of b,d;
  let g be Morphism of c,e, k be Morphism of d,s;
  assume that
A1: Hom(a,c) <> {} and
A2: Hom(b,d) <> {} and
A3: Hom(c,e) <> {} and
A4: Hom(d,s) <> {};
A5: Hom(e,e+s) <> {} & Hom(s,e+s) <> {} by Th66;
  then in1(e,s)*g*f = in1(e,s)*(g*f) & in2(e,s)*k*h = in2(e,s)*(k*h)
    by A1,A2,A3,A4,CAT_1:54;
  then Hom(c,e+s) <> {} & Hom(d,e+s) <> {} &
    (g*f)+(k*h) = [$in1(e,s)*g*f,in2(e,s)*k*h$] &
     g+k = [$in1(e,s)*g,in2(e,s)*k$] by A3,A4,A5,Def31,CAT_1:52;
  hence thesis by A1,A2,Th80;
 end;

Back to top