:: Cartesian Categories :: by Czes{\l}aw Byli\'nski :: :: Received October 27, 1992 :: Copyright (c) 1992-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies CAT_1, WELLORD1, XBOOLE_0, RELAT_1, FINSET_1, FUNCT_1, STRUCT_0, CAT_3, GRAPH_1, CARD_1, FUNCOP_1, PARTFUN1, NAT_1, ARYTM_3, SUBSET_1, TARSKI, ARYTM_1, FUNCT_4, FUNCT_6, ZFMISC_1, ALGSTR_1, MCART_1, DIRAF, PBOOLE, EQREL_1, CAT_4, MONOID_0, RELAT_2, BINOP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, ALGSTR_1, XCMPLX_0, ORDINAL1, CARD_1, FUNCT_4, STRUCT_0, GRAPH_1, CAT_1, CAT_3; constructors BINOP_1, REAL_1, NAT_1, ALGSTR_1, CAT_3, RELSET_1, XREAL_0, FUNCT_4; registrations XBOOLE_0, FUNCT_1, FINSET_1, XREAL_0, NAT_1, ORDINAL1, CARD_1, STRUCT_0, PARTFUN1, FUNCT_2, RELSET_1, CAT_1; requirements NUMERALS, SUBSET, BOOLE; definitions CAT_1, CAT_3; equalities CAT_1, FUNCOP_1, GRAPH_1; expansions 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, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes NAT_1; begin reserve o,m for set; 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, f9 being Morphism of b,a st f*f9 = id b & f9*f = id a; compatibility by CAT_1:48; 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 carrier of C ex a being Object of C, F9 being Projections_family of a, I st cods F9 = F & a is_a_product_wrt F9; end; theorem Th1: for C being Category holds C is with_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 is with_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 reconsider F = {} as Function of {},the carrier of C by RELSET_1:12; assume A1: for I being finite set, F being Function of I,the carrier of C ex a being Object of C, F9 being Projections_family of a,I st cods F9 = F & a is_a_product_wrt F9; then consider a being Object of C, F9 being Projections_family of a,{} such that cods F9 = F and A2: a is_a_product_wrt F9; thus ex a being Object of C st a is terminal by A2,CAT_3:50; let a,b be Object of C; set F = (0,1)-->(a,b); consider c being Object of C, F9 being Projections_family of c,{0,1} such that A3: cods F9 = F and A4: c is_a_product_wrt F9 by A1; take c, p1 = F9/.0, p2 = F9/.1; A5: 1 in {0,1} by TARSKI:def 2; then A6: p2 = F9.1 by FUNCT_2:def 13; A7: 0 in {0,1} by TARSKI:def 2; hence dom p1 = c & dom p2 = c by A5,CAT_3:41; F/.0 = a & F/.1 = b by CAT_3:3; hence cod p1 = a & cod p2 = b by A3,A7,A5,CAT_3:def 2; dom F9 = {0,1} & p1 = F9.0 by A7,FUNCT_2:def 1,def 13; then F9 = (0,1)-->(p1,p2) by A6,FUNCT_4:66; hence thesis by A4,CAT_3:54; end; given a being Object of C such that A8: a is terminal; defpred Q[Nat] means for I being finite set, F being Function of I,the carrier of C st card I = $1 ex a being Object of C, F9 being Projections_family of a,I st cods F9 = F & a is_a_product_wrt F9; assume A9: 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; A10: for n being Nat st Q[n] holds Q[n+1] proof let n be Nat such that A11: Q[n]; let I be finite set, F be Function of I,the carrier of C such that A12: card I = n+1; set x = the Element of I; reconsider Ix = I \ {x} as finite set; reconsider sx = {x} as finite set; reconsider G = F|(I\{x}) as Function of I\{x},the carrier of C by FUNCT_2:32; card(Ix) = card(I) - card(sx) by A12,CARD_1:27,CARD_2:44,ZFMISC_1:31 .= card(I) - 1 by CARD_1:30 .= n by A12,XCMPLX_1:26; then consider a being Object of C, G9 being Projections_family of a,I\{x} such that A13: cods G9 = G and A14: a is_a_product_wrt G9 by A11; consider c being Object of C, p1,p2 being Morphism of C such that A15: dom p1 = c and A16: dom p2 = c and A17: cod p1 = a and A18: cod p2 = F/.x and A19: c is_a_product_wrt p1,p2 by A9; set F9 = (G9*p1) +* (x .-->p2); A20: dom({x} -->p2) = {x} by FUNCT_2:def 1; rng F9 c= rng(G9*p1) \/ rng(x .-->p2) by FUNCT_4:17; then A21: rng F9 c= the carrier' of C by XBOOLE_1:1; dom(G9*p1) = I\{x} by FUNCT_2:def 1; then A22: dom(G9*p1) \/ dom(x .-->p2) = I \/ {x} by A20,XBOOLE_1:39 .= I by A12,CARD_1:27,ZFMISC_1:40; then dom F9 = I by FUNCT_4:def 1; then reconsider F9 as Function of I, the carrier' of C by A21,FUNCT_2:def 1 ,RELSET_1:4; A23: doms G9 = (I\{x})-->a by CAT_3:def 13; now let y be object; assume A24: y in I; now per cases; suppose y = x; then A25: y in {x} by TARSKI:def 1; F9/.y = F9.y by A24,FUNCT_2:def 13 .= (x .-->p2).y by A20,A25,FUNCT_4:13 .= p2 by A25,FUNCOP_1:7; hence (I --> c).y = dom(F9/.y) by A16,A24,FUNCOP_1:7 .= (doms F9)/.y by A24,CAT_3:def 1; end; suppose A26: y <> x; then A27: not y in {x} by TARSKI:def 1; A28: y in I\{x} by A24,A26,ZFMISC_1:56; F9/.y = F9.y by A24,FUNCT_2:def 13 .= (G9*p1).y by A20,A22,A24,A27,FUNCT_4:def 1 .= (G9*p1)/.y by A28,FUNCT_2:def 13; hence (doms F9)/.y = dom((G9*p1)/.y) by A24,CAT_3:def 1 .= (doms(G9*p1))/.y by A28,CAT_3:def 1 .= ((I\{x})-->c)/.y by A15,A17,A23,CAT_3:16 .= c by A24,A26,CAT_3:2,ZFMISC_1:56 .= (I --> c).y by A24,FUNCOP_1:7; end; end; hence (doms F9).y = (I --> c).y by A24,FUNCT_2:def 13; end; then reconsider F9 as Projections_family of c,I by CAT_3:def 13,FUNCT_2:12; take c,F9; A29: now let y be set; assume A30: y in I; now per cases; suppose A31: y = x; then A32: y in {x} by TARSKI:def 1; F9/.y = F9.y by A30,FUNCT_2:def 13 .= (x .-->p2).y by A20,A32,FUNCT_4:13 .= p2 by A32,FUNCOP_1:7; hence (cods F9)/.y = F/.y by A18,A30,A31,CAT_3:def 2; end; suppose A33: y <> x; then A34: not y in {x} by TARSKI:def 1; A35: y in I\{x} by A30,A33,ZFMISC_1:56; F9/.y = F9.y by A30,FUNCT_2:def 13 .= (G9*p1).y by A20,A22,A30,A34,FUNCT_4:def 1 .= (G9*p1)/.y by A35,FUNCT_2:def 13; hence (cods F9)/.y = cod((G9*p1)/.y) by A30,CAT_3:def 2 .= (cods(G9*p1))/.y by A35,CAT_3:def 2 .= G/.y by A13,A17,A23,CAT_3:16 .= G.y by A35,FUNCT_2:def 13 .= F.y by A30,A33,FUNCT_1:49,ZFMISC_1:56 .= F/.y by A30,FUNCT_2:def 13; end; end; hence (cods F9)/.y = F/.y; end; hence cods F9 = F by CAT_3:1; thus F9 is Projections_family of c,I; let d be Object of C; let F99 be Projections_family of d,I such that A36: cods F9 = cods F99; reconsider G99 = F99|(I\{x}) as Function of I\{x},the carrier' of C by FUNCT_2:32; now let y be set; assume A37: y in I\{x}; then G99/.y = G99.y by FUNCT_2:def 13 .= F99.y by A37,FUNCT_1:49 .= F99/.y by A37,FUNCT_2:def 13; hence doms(G99)/.y = dom(F99/.y) by A37,CAT_3:def 1 .= d by A37,CAT_3:41 .= ((I\{x})-->d)/.y by A37,CAT_3:2; end; then reconsider G99 as Projections_family of d,I\{x} by CAT_3:1,def 13; now let y be set; assume A38: y in I\{x}; then A39: G/.y = G.y by FUNCT_2:def 13 .= F.y by A38,FUNCT_1:49 .= F/.y by A38,FUNCT_2:def 13; F99/.y = F99.y by A38,FUNCT_2:def 13 .= G99.y by A38,FUNCT_1:49 .= G99/.y by A38,FUNCT_2:def 13; hence (cods G9)/.y = cod(G99/.y) by A13,A36,A38,A39,A29,CAT_3:1,def 2 .= (cods G99)/.y by A38,CAT_3:def 2; end; then consider h9 being Morphism of C such that A40: h9 in Hom(d,a) and A41: for k being Morphism of C st k in Hom(d,a) holds (for y being set st y in I\{x} holds (G9/.y)(*)k = G99/.y) iff h9 = k by A14,CAT_3:1; A42: x in {x} by TARSKI:def 1; set g = F99/.x; A43: dom g = d by A12,CARD_1:27,CAT_3:41; A44: F9/.x = F9.x by A12,CARD_1:27,FUNCT_2:def 13 .= (x .-->p2).x by A20,A42,FUNCT_4:13 .= p2 by A42,FUNCOP_1:7; then cod p2 = (cods F9)/.x by A12,CARD_1:27,CAT_3:def 2 .= cod g by A12,A36,CARD_1:27,CAT_3:def 2; then g in Hom(d,cod p2) by A43; then consider h being Morphism of C such that A45: h in Hom(d,c) and A46: for k being Morphism of C st k in Hom(d,c) holds p1(*)k = h9 & p2(*)k = g iff h = k by A17,A19,A40; take h; thus h in Hom(d,c) by A45; let k be Morphism of C such that A47: k in Hom(d,c); thus (for y being set st y in I holds (F9/.y)(*)k = F99/.y) implies h = k proof A48: cod k = c by A47,CAT_1:1; then A49: cod(p1(*)k) = a by A15,A17,CAT_1:17; assume A50: for y being set st y in I holds (F9/.y)(*)k = F99/.y; A51: for y being set st y in I\{x} holds (G9/.y)(*)(p1(*)k) = G99/.y proof let y be set; assume A52: y in I\{x}; then A53: not y in {x} by XBOOLE_0:def 5; A54: F9/.y = F9.y by A52,FUNCT_2:def 13 .= (G9*p1).y by A20,A22,A52,A53,FUNCT_4:def 1 .= (G9*p1)/.y by A52,FUNCT_2:def 13; dom(G9/.y) = a by A52,CAT_3:41; hence (G9/.y)(*)(p1(*)k) = ((G9/.y)(*)p1)(*)k by A15,A17,A48,CAT_1:18 .= ((G9*p1)/.y)(*)k by A52,CAT_3:def 5 .= F99/.y by A50,A52,A54 .= F99.y by A52,FUNCT_2:def 13 .= G99.y by A52,FUNCT_1:49 .= G99/.y by A52,FUNCT_2:def 13; end; dom k = d by A47,CAT_1:1; then dom(p1(*)k) = d by A15,A48,CAT_1:17; then p1(*)k in Hom(d,a) by A49; then A55: p1(*)k = h9 by A41,A51; p2(*)k = g by A12,A44,A50,CARD_1:27; hence thesis by A46,A47,A55; end; assume A56: h = k; let y be set such that A57: y in I; now per cases; suppose A58: y = x; then A59: y in {x} by TARSKI:def 1; F9/.y = F9.y by A57,FUNCT_2:def 13 .= (x .-->p2).y by A20,A59,FUNCT_4:13 .= p2 by A59,FUNCOP_1:7; hence thesis by A46,A47,A56,A58; end; suppose A60: y <> x; then A61: not y in {x} by TARSKI:def 1; A62: cod k = c by A47,CAT_1:1; A63: y in I\{x} by A57,A60,ZFMISC_1:56; A64: dom(G9/.y) = a by A57,A60,CAT_3:41,ZFMISC_1:56; F9/.y = F9.y by A57,FUNCT_2:def 13 .= (G9*p1).y by A20,A22,A57,A61,FUNCT_4:def 1 .= (G9*p1)/.y by A63,FUNCT_2:def 13 .= (G9/.y)(*)p1 by A63,CAT_3:def 5; hence (F9/.y)(*)k = (G9/.y)(*)(p1(*)k) by A15,A17,A62,A64,CAT_1:18 .= (G9/.y)(*)h9 by A46,A47,A56 .= G99/.y by A40,A41,A63 .= G99.y by A63,FUNCT_2:def 13 .= F99.y by A57,A60,FUNCT_1:49,ZFMISC_1:56 .= F99/.y by A57,FUNCT_2:def 13; end; end; hence thesis; end; let I be finite set, F be Function of I,the carrier of C; A65: card I = card I; A66: Q[ 0 ] proof let I be finite set, F be Function of I,the carrier of C; assume card I = 0; then A67: I = {}; {} is Function of {}, the carrier' of C by RELSET_1:12; then reconsider F9 = {} as Projections_family of a,I by A67,CAT_3:42; take a,F9; for x being set st x in I holds (cods F9)/.x = F/.x; hence cods F9 = F by CAT_3:1; thus thesis by A8,A67,CAT_3:50; end; for n being Nat holds Q[n] from NAT_1:sch 2(A66,A10); hence thesis by A65; end; definition struct (CatStr)ProdCatStr (# carrier,carrier' -> set, Source,Target -> Function of the carrier', the carrier, Comp -> PartFunc of [:the carrier', the carrier' :],the carrier', TerminalObj -> Element of the carrier, CatProd -> Function of [:the carrier,the carrier:],the carrier, Proj1,Proj2 -> Function of [:the carrier,the carrier:], the carrier' #); end; registration cluster non void non empty for ProdCatStr; existence proof set o = the set; take ProdCatStr(# {o},{o},o:->o,o:->o,(o,o):->o,Extract(o),(o,o):-> o,(o,o):->o,(o,o):->o #); thus thesis; end; end; definition let C be non void non empty ProdCatStr; func [1]C -> Object of C equals the TerminalObj of C; correctness; let a,b be Object of C; func a[x]b -> Object of C equals (the CatProd of C).(a,b); correctness; func pr1(a,b) -> Morphism of C equals (the Proj1 of C).(a,b); correctness; func pr2(a,b) -> Morphism of C equals (the Proj2 of C).(a,b); correctness; end; definition let o,m; func c1Cat(o,m) -> strict ProdCatStr equals ProdCatStr(# {o},{m},m:->o,m:->o,(m,m):->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #); correctness; end; registration let o,m be set; cluster c1Cat(o,m) -> non empty trivial non void trivial'; coherence; end; theorem the CatStr of c1Cat(o,m) = 1Cat(o,m); Lm1: c1Cat(o,m) is Category-like proof set C = c1Cat(o,m); set CP = the Comp of C, CD = the Source of C, CC = the Target of C; thus for f,g being Morphism of C holds [g,f] in dom CP iff dom g = cod f proof let f,g be Morphism of C; A1: dom CP = {[m,m]} by FUNCOP_1:13; f = m & g = m by TARSKI:def 1; hence thesis by A1,TARSKI:def 1; end; end; registration cluster strict Category-like reflexive transitive associative with_identities non void non empty for non void non empty ProdCatStr; existence proof c1Cat(0,1) is Category-like transitive reflexive associative with_identities by Lm1; hence thesis; end; end; registration let o,m be set; cluster c1Cat(o,m) -> Category-like reflexive transitive associative with_identities non empty non void; coherence by Lm1; end; theorem Th3: for a,b being Object of c1Cat(o,m) holds a = b proof let a,b be Object of c1Cat(o,m); a = o by TARSKI:def 1; hence thesis by TARSKI:def 1; end; theorem Th4: for f,g being Morphism of c1Cat(o,m) holds f = g proof let f,g be Morphism of c1Cat(o,m); f = m by TARSKI:def 1; hence thesis by TARSKI:def 1; end; theorem Th5: 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); cod f = o by TARSKI:def 1; then A1: cod f = b by TARSKI:def 1; dom f = o by TARSKI:def 1; then dom f = a by TARSKI:def 1; hence thesis by A1; 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 Th5; hence thesis by CAT_1:def 5; end; theorem for a,b being Object of c1Cat(o,m) holds Hom(a,b) <> {} by Th5; theorem Th8: 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); set f = the Morphism of b,a; thus Hom(b,a)<>{} by Th5; take f; thus thesis by Th4; end; theorem Th9: 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 Th3; let d be Object of c1Cat(o,m),f,g be Morphism of c1Cat(o,m) such that f in Hom(d,cod p1) and g in Hom(d,cod p2); take h = p1; thus h in Hom(d,c) by Th5; thus thesis by Th4; end; definition let IT be Category-like reflexive transitive associative with_identities non void non empty ProdCatStr; attr IT is Cartesian means :Def8: 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 Th10: for o,m being set holds c1Cat(o,m) is Cartesian by Th8,Th3,Th9; registration cluster strict Cartesian for Category-like reflexive transitive associative with_identities non void non empty ProdCatStr; existence proof c1Cat(0,1) is Cartesian by Th10; hence thesis; end; end; definition mode Cartesian_category is Cartesian Category-like non void non empty reflexive transitive associative with_identities non void non empty ProdCatStr; end; reserve C for Cartesian_category; reserve a,b,c,d,e,s for Object of C; theorem [1]C is terminal by Def8; theorem Th12: 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 Def8; then consider f being Morphism of a,[1]C such that A1: for g being Morphism of a,[1]C holds f = g; thus f1 = f by A1 .= f2 by A1; end; theorem Th13: Hom(a,[1]C) <> {} proof [1]C is terminal by Def8; hence thesis; end; definition let C,a; func term(a) -> Morphism of a,[1]C means not contradiction; existence; uniqueness by Th12; end; theorem Th14: term a = term(a,[1]C) proof [1]C is terminal by Def8; hence thesis by CAT_3:37; end; theorem dom(term a) = a & cod(term a) = [1]C proof [1]C is terminal & term a = term(a,[1]C) by Def8,Th14; hence thesis by CAT_3:35; end; theorem Hom(a,[1]C) = {term a} proof for f2 being Morphism of a,[1]C holds term a = f2 by Th12; hence thesis by Th13,CAT_1:8; end; theorem Th17: 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); a[x]b is_a_product_wrt p1,p2 by Def8; hence thesis by Def8; end; theorem Th18: 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); a[x]b is_a_product_wrt p1,p2 by Def8; hence thesis by Def8; 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 Th17; hence thesis by CAT_1:4; end; redefine 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 Th18; hence thesis by CAT_1:4; end; end; theorem Th19: 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 Def8; then A1: dom p1 = c & dom p2 = c; cod(p1) = a & cod(p2) = b by Def8; hence thesis by A1,CAT_1:1; end; theorem a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Def8; theorem C is with_finite_product proof A1: 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 Def8,Th17,Th18; end; [1]C is terminal by Def8; 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 A1: Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19; a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) & cod pr1(a,b) = a by Def8; hence thesis by A1,CAT_3:57; 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 :Def10: pr1(a,b)*it = f & pr2(a,b) *it = g; existence proof A2: a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Def8; Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19; then consider h being Morphism of c,a[x]b such that A3: 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,A2,CAT_3:55; take h; thus thesis by A3; end; uniqueness proof A4: a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Def8; Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19; 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,A4,CAT_3:55; let h1,h2 be Morphism of c,a[x]b such that A6: pr1(a,b)*h1 = f & pr2(a,b)*h1 = g and A7: pr1(a,b)*h2 = f & pr2(a,b)*h2 = g; h1 = h by A6,A5; hence thesis by A7,A5; end; end; theorem Th23: Hom(c,a) <> {} & Hom(c,b) <> {} implies Hom(c,a[x]b) <> {} proof A1: a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Def8; Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19; hence thesis by A1,CAT_3:55; end; theorem Th24: <:pr1(a,b),pr2(a,b):> = id(a[x]b) proof A1: Hom(a[x]b,b) <> {} by Th19; then A2: pr2(a,b)*(id(a[x]b)) = pr2(a,b) by CAT_1:29; A3: Hom(a[x]b,a) <> {} by Th19; then pr1(a,b)*(id(a[x]b)) = pr1(a,b) by CAT_1:29; hence thesis by A3,A1,A2,Def10; end; theorem Th25: 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)<>{} & Hom(c,b)<>{} and A2: Hom(d,c)<>{}; A3: Hom(c,a[x]b) <> {} by A1,Th23; A4: Hom(a[x]b,b) <> {} by Th19; (pr2(a,b)*<:f,g:>)*h = g*h by A1,Def10; then A5: pr2(a,b)*(<:f,g:>*h) = g*h by A2,A4,A3,CAT_1:25; A6: Hom(a[x]b,a) <> {} by Th19; A7: Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,CAT_1:24; (pr1(a,b)*<:f,g:>)*h = f*h by A1,Def10; then pr1(a,b)*(<:f,g:>*h) = f*h by A2,A6,A3,CAT_1:25; hence thesis by A5,A7,Def10; end; theorem Th26: 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 A1: Hom(c,a) <> {} & Hom(c,b) <> {}; then pr1(a,b)*<:f,g:> = f & pr2(a,b)*<:f,g:> = g by Def10; hence thesis by A1,Def10; 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: g is monic; let d be Object of C, f1,f2 be Morphism of d,c such that A6: Hom(d,c)<>{} and A7: <:f,g:>*f1 = <:f,g:>*f2; A8: Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A6,CAT_1:24; <:f*f1,g*f1:> = <:f,g:>*f1 & <:f*f2,g*f2:> = <:f,g:>*f2 by A1,A2,A6,Th25; then g*f1 = g*f2 by A7,A8,Th26; hence f1 = f2 by A5,A6; end; A9: now assume A10: f is monic; let d; let f1,f2 be Morphism of d,c such that A11: Hom(d,c)<>{} and A12: <:f,g:>*f1 = <:f,g:>*f2; A13: Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A11,CAT_1:24; <:f*f1,g*f1:> = <:f,g:>*f1 & <:f*f2,g*f2:> = <:f,g:>*f2 by A1,A2,A11,Th25; then f*f1 = f*f2 by A12,A13,Th26; hence f1 = f2 by A10,A11; end; Hom(c,a[x]b) <> {} by A1,A2,Th23; hence thesis by A3,A9,A4; end; theorem Th28: Hom(a,a[x][1]C) <> {} & Hom(a,[1]C[x]a) <> {} proof Hom(a,[1]C) <> {} & Hom(a,a) <> {} by Th13; hence thesis by Th23; end; definition let C,a; func lambda(a) -> Morphism of [1]C[x]a,a equals pr2([1]C,a); correctness; func lambda'(a) -> Morphism of a,[1]C[x]a equals <:term a,id a:>; correctness; func rho(a) -> Morphism of a[x][1]C,a equals pr1(a,[1]C); correctness; func rho'(a) -> Morphism of a,a[x][1]C equals <:id a,term a:>; correctness; end; theorem Th29: 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: (term a)*pr2([1]C,a) = pr1([1]C,a) by Th12; A2: Hom(a,[1]C) <> {} & Hom(a,a) <> {} by Th13; hence id a = lambda(a)*lambda'(a) by Def10; A3: Hom([1]C[x]a,a) <> {} by Th19; then (id a)*pr2([1]C,a) = pr2([1]C,a) by CAT_1:28; then <:term a,id a:>*pr2([1]C,a) = <:pr1([1]C,a),pr2([1]C,a):> by A2,A3,A1 ,Th25; hence id([1]C[x]a) = lambda'(a)*lambda(a) by Th24; thus id a = rho(a)*rho'(a) by A2,Def10; A4: (term a)*pr1(a,[1]C) = pr2(a,[1]C) by Th12; A5: Hom(a[x][1]C,a) <> {} by Th19; then (id a)*pr1(a,[1]C) = pr1(a,[1]C) by CAT_1:28; then <:id a,term a:>*pr1(a,[1]C) = <:pr1(a,[1]C),pr2(a,[1]C):> by A2,A5,A4 ,Th25; hence thesis by Th24; 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 Th19,Th28; take rho'(a), rho(a); thus thesis by Th29; end; thus Hom(a,[1]C[x]a) <> {} & Hom([1]C[x]a,a) <> {} by Th19,Th28; take lambda'(a), lambda(a); thus thesis by Th29; end; definition let C,a,b; func Switch(a,b) -> Morphism of a[x]b,b[x]a equals <:pr2(a,b),pr1(a,b):>; correctness; end; theorem Th31: Hom(a[x]b,b[x]a)<>{} proof Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19; hence thesis by Th23; end; theorem Th32: Switch(a,b)*Switch(b,a) = id(b[x]a) proof A1: Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19; A2: Hom(b[x]a,b) <> {} & Hom(b[x]a,a) <> {} by Th19; then Hom(b[x]a,a[x]b)<>{} by Th23; hence Switch(a,b)*Switch(b,a) = <:pr2(a,b)*<:pr2(b,a),pr1(b,a):>,pr1(a,b)*<: pr2(b,a),pr1(b,a):>:> by A1,Th25 .= <:pr1(b,a),pr1(a,b)*<:pr2(b,a),pr1(b,a):>:> by A2,Def10 .= <:pr1(b,a),pr2(b,a):> by A2,Def10 .= id(b[x]a) by Th24; 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 Th31; take Switch(a,b), Switch(b,a); thus thesis by Th32; end; definition let C,a; func Delta a -> Morphism of a,a[x]a equals <:id a,id a:>; correctness; end; theorem Hom(a,a[x]a) <> {} proof Hom(a,a) <> {}; hence thesis by Th23; 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) <> {}; Hom(b,b) <> {} & (id b)*f = f by A1,CAT_1:28; hence thesis by A1,Th25; 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 <: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 <:<:pr1(a,b [x]c),pr1(b,c)*pr2(a,b[x]c):>,pr2(b,c)*pr2(a,b[x]c):>; correctness; end; theorem Th36: 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)[x]c,a[x]b) <> {} by Th19; Hom(a[x]b,b) <> {} by Th19; then A2: Hom((a[x]b)[x]c,b) <> {} by A1,CAT_1:24; Hom(a[x]b,a) <> {} by Th19; then A3: Hom((a[x]b)[x]c,a) <> {} by A1,CAT_1:24; Hom((a[x]b)[x]c,c) <> {} by Th19; then Hom((a[x]b)[x]c,b[x]c) <> {} by A2,Th23; hence Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} by A3,Th23; A4: Hom(a[x](b[x]c),b[x]c) <> {} by Th19; Hom(b[x]c,c) <> {} by Th19; then A5: Hom(a[x](b[x]c),c) <> {} by A4,CAT_1:24; Hom(b[x]c,b) <> {} by Th19; then A6: Hom(a[x](b[x]c),b) <> {} by A4,CAT_1:24; Hom(a[x](b[x]c),a) <> {} by Th19; then Hom(a[x](b[x]c),a[x]b) <> {} by A6,Th23; hence thesis by A5,Th23; end; theorem Th37: 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 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):>; A1: Hom((a[x]b)[x]c,a[x]b) <> {} by Th19; A2: Hom(a[x]b,b) <> {} by Th19; then A3: Hom((a[x]b)[x]c,b) <> {} by A1,CAT_1:24; A4: Hom((a[x]b)[x]c,c) <> {} by Th19; then A5: Hom((a[x]b)[x]c,b[x]c) <> {} by A3,Th23; A6: Hom(a[x]b,a) <> {} by Th19; then A7: Hom((a[x]b)[x]c,a) <> {} by A1,CAT_1:24; A8: Hom(a[x](b[x]c),b[x]c) <> {} by Th19; A9: Hom(b[x]c,c) <> {} by Th19; then A10: Hom(a[x](b[x]c),c) <> {} by A8,CAT_1:24; A11: Hom(b[x]c,b) <> {} by Th19; then A12: Hom(a[x](b[x]c),b) <> {} by A8,CAT_1:24; A13: Hom(a[x](b[x]c),a) <> {} by Th19; then A14: Hom(a[x](b[x]c),a[x]b) <> {} by A12,Th23; A15: Hom(a[x](b[x]c),(a[x]b)[x]c) <> {} by Th36; then pr2(a,b)*pr1(a[x]b,c)*g = pr2(a,b)*(pr1(a[x]b,c)*g) by A1,A2,CAT_1:25 .= pr2(a,b)*l by A10,A14,Def10 .= pr1(b,c)*pr2(a,b[x]c) by A12,A13,Def10; then A16: k*g = <:pr1(b,c)*pr2(a,b[x]c),pr2(a[x]b,c)*g:> by A3,A4,A15,Th25 .= <:pr1(b,c)*pr2(a,b[x]c),pr2(b,c)*pr2(a,b[x]c):> by A10,A14,Def10 .= <:pr1(b,c),pr2(b,c):>*pr2(a,b[x]c) by A11,A8,A9,Th25 .= id(b[x]c)*pr2(a,b[x]c) by Th24 .= pr2(a,b[x]c) by A8,CAT_1:28; A17: Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} by Th36; then pr1(b,c)*pr2(a,b[x]c)*f = pr1(b,c)*(pr2(a,b[x]c)*f) by A11,A8,CAT_1:25 .= pr1(b,c)*k by A7,A5,Def10 .= pr2(a,b)*pr1(a[x]b,c) by A3,A4,Def10; then A18: l*f = <:pr1(a,b[x]c)*f,pr2(a,b)*pr1(a[x]b,c):> by A17,A12,A13,Th25 .= <:pr1(a,b)*pr1(a[x]b,c),pr2(a,b)*pr1(a[x]b,c):> by A7,A5,Def10 .= <:pr1(a,b),pr2(a,b):>*pr1(a[x]b,c) by A6,A1,A2,Th25 .= id(a[x]b)*pr1(a[x]b,c) by Th24 .= pr1(a[x]b,c) by A1,CAT_1:28; pr1(a,b)*pr1(a[x]b,c)*g = pr1(a,b)*(pr1(a[x]b,c)*g) by A6,A1,A15,CAT_1:25 .= pr1(a,b)*l by A10,A14,Def10 .= pr1(a,b[x]c) by A12,A13,Def10; hence Alpha(a,b,c)*Alpha'(a,b,c) = <:pr1(a,b[x]c),pr2(a,b[x]c):> by A7,A5,A15,A16 ,Th25 .= id(a[x](b[x]c)) by Th24; pr2(b,c)*pr2(a,b[x]c)*f = pr2(b,c)*(pr2(a,b[x]c)*f) by A17,A8,A9,CAT_1:25 .= pr2(b,c)*k by A7,A5,Def10 .= pr2(a[x]b,c) by A3,A4,Def10; hence Alpha'(a,b,c)*Alpha(a,b,c) = <:pr1(a[x]b,c),pr2(a[x]b,c):> by A17,A10 ,A14,A18,Th25 .= id((a[x]b)[x]c) by Th24; 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 Th36; take Alpha(a,b,c), Alpha'(a,b,c); thus thesis by Th37; 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 <: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 that A1: Hom(a,c) <> {} and A2: Hom(b,d) <> {}; Hom(a[x]b,b) <> {} by Th19; then A3: Hom(a[x]b,d) <> {} by A2,CAT_1:24; Hom(a[x]b,a) <> {} by Th19; then Hom(a[x]b,c) <> {} by A1,CAT_1:24; hence thesis by A3,Th23; end; theorem (id a)[x](id b) = id(a[x]b) proof Hom(a[x]b,b) <> {} by Th19; then A1: (id b)*pr2(a,b) = pr2(a,b) by CAT_1:28; Hom(a[x]b,a) <> {} by Th19; then (id a)*pr1(a,b) = pr1(a,b) by CAT_1:28; hence thesis by A1,Th24; end; theorem Th41: 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) <> {} & Hom(e,c) <> {}; A4: Hom(e,a[x]c) <> {} by A3,Th23; A5: Hom(a[x]c,c) <> {} by Th19; then A6: Hom(a[x]c,d) <> {} by A2,CAT_1:24; A7: Hom(a[x]c,a) <> {} by Th19; then A8: Hom(a[x]c,b) <> {} by A1,CAT_1:24; pr2(a,c)*<:g,k:> = k by A3,Def10; then A9: h*k = (h*pr2(a,c))*<:g,k:> by A2,A4,A5,CAT_1:25; pr1(a,c)*<:g,k:> = g by A3,Def10; then f*g = (f*pr1(a,c))*<:g,k:> by A1,A4,A7,CAT_1:25; hence thesis by A4,A8,A6,A9,Th25; 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) <> {}; Hom(c,c) <> {}; hence (f[x]g)*Delta(c) = <:f*(id c),g*(id c):> by A1,A2,Th41 .= <:f,g*(id c):> by A1,CAT_1:29 .= <:f,g:> by A2,CAT_1:29; 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,s) <> {} by Th19; then A6: Hom(e[x]s,c) <> {} by A4,CAT_1:24; A7: Hom(e[x]s,e) <> {} by Th19; then f*(g*pr1(e,s)) = (f*g)*pr1(e,s) by A1,A3,CAT_1:25; then A8: (f*g)[x](h*k) = <:f*(g*pr1(e,s)),h*(k*pr2(e,s)):> by A2,A4,A5,CAT_1:25; Hom(e[x]s,a) <> {} by A3,A7,CAT_1:24; hence thesis by A1,A2,A6,A8,Th41; 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 carrier of C ex a being Object of C, F9 being Injections_family of a,I st doms F9 = F & a is_a_coproduct_wrt F9; end; theorem Th44: for C being Category holds C is with_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 is with_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 reconsider F = {} as Function of {},the carrier of C by RELSET_1:12; A1: 0 in {0,1} by TARSKI:def 2; assume A2: for I being finite set, F being Function of I,the carrier of C ex a being Object of C, F9 being Injections_family of a,I st doms F9 = F & a is_a_coproduct_wrt F9; then consider a being Object of C, F9 being Injections_family of a,{} such that doms F9 = F and A3: a is_a_coproduct_wrt F9; thus ex a being Object of C st a is initial by A3,CAT_3:75; let a,b be Object of C; set F = (0,1)-->(a,b); consider c being Object of C, F9 being Injections_family of c,{0,1} such that A4: doms F9 = F and A5: c is_a_coproduct_wrt F9 by A2; take c, i1 = F9/.0, i2 = F9/.1; A6: 1 in {0,1} by TARSKI:def 2; then A7: i2 = F9.1 by FUNCT_2:def 13; F/.0 = a & F/.1 = b by CAT_3:3; hence dom i1 = a & dom i2 = b by A4,A1,A6,CAT_3:def 1; thus cod i1 = c & cod i2 = c by A1,A6,CAT_3:62; dom F9 = {0,1} & i1 = F9.0 by A1,FUNCT_2:def 1,def 13; then F9 = (0,1)-->(i1,i2) by A7,FUNCT_4:66; hence thesis by A5,CAT_3:79; end; given a being Object of C such that A8: a is initial; defpred Q[Nat] means for I being finite set, F being Function of I,the carrier of C st card I = $1 ex a being Object of C, F9 being Injections_family of a,I st doms F9 = F & a is_a_coproduct_wrt F9; assume A9: 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; A10: for n being Nat st Q[n] holds Q[n+1] proof let n be Nat such that A11: Q[n]; let I be finite set, F be Function of I,the carrier of C such that A12: card I = n+1; set x = the Element of I; reconsider Ix = I \ {x} as finite set; reconsider sx = {x} as finite set; reconsider G = F|(I\{x}) as Function of I\{x},the carrier of C by FUNCT_2:32; card(Ix) = card(I) - card(sx) by A12,CARD_1:27,CARD_2:44,ZFMISC_1:31 .= card(I) - 1 by CARD_1:30 .= n by A12,XCMPLX_1:26; then consider a being Object of C, G9 being Injections_family of a,I\{x} such that A13: doms G9 = G and A14: a is_a_coproduct_wrt G9 by A11; set b = F/.x; consider c being Object of C, i1,i2 being Morphism of C such that A15: dom i1 = a and A16: dom i2 = b and A17: cod i1 = c and A18: cod i2 = c and A19: c is_a_coproduct_wrt i1,i2 by A9; set F9 = (i1*G9) +* (x .-->i2); A20: dom({x} -->i2) = {x} by FUNCT_2:def 1; rng F9 c= rng(i1*G9) \/ rng(x .-->i2) by FUNCT_4:17; then A21: rng F9 c= the carrier' of C by XBOOLE_1:1; dom(i1*G9) = I\{x} by FUNCT_2:def 1; then A22: dom(i1*G9) \/ dom(x .-->i2) = I \/ {x} by A20,XBOOLE_1:39 .= I by A12,CARD_1:27,ZFMISC_1:40; then dom F9 = I by FUNCT_4:def 1; then reconsider F9 as Function of I, the carrier' of C by A21,FUNCT_2:def 1 ,RELSET_1:4; A23: cods G9 = (I\{x})-->a by CAT_3:def 16; now let y be object; assume A24: y in I; now per cases; suppose y = x; then A25: y in {x} by TARSKI:def 1; F9/.y = F9.y by A24,FUNCT_2:def 13 .= (x .-->i2).y by A20,A25,FUNCT_4:13 .= i2 by A25,FUNCOP_1:7; hence (I --> c).y = cod(F9/.y) by A18,A24,FUNCOP_1:7 .= (cods F9)/.y by A24,CAT_3:def 2; end; suppose A26: y <> x; then A27: not y in {x} by TARSKI:def 1; A28: y in I\{x} by A24,A26,ZFMISC_1:56; F9/.y = F9.y by A24,FUNCT_2:def 13 .= (i1*G9).y by A20,A22,A24,A27,FUNCT_4:def 1 .= (i1*G9)/.y by A28,FUNCT_2:def 13; hence (cods F9)/.y = cod((i1*G9)/.y) by A24,CAT_3:def 2 .= (cods(i1*G9))/.y by A28,CAT_3:def 2 .= ((I\{x})-->c)/.y by A15,A17,A23,CAT_3:17 .= c by A24,A26,CAT_3:2,ZFMISC_1:56 .= (I --> c).y by A24,FUNCOP_1:7; end; end; hence (cods F9).y = (I --> c).y by A24,FUNCT_2:def 13; end; then reconsider F9 as Injections_family of c,I by CAT_3:def 16,FUNCT_2:12; take c,F9; A29: now let y be set; assume A30: y in I; now per cases; suppose A31: y = x; then A32: y in {x} by TARSKI:def 1; F9/.y = F9.y by A30,FUNCT_2:def 13 .= (x .-->i2).y by A20,A32,FUNCT_4:13 .= i2 by A32,FUNCOP_1:7; hence (doms F9)/.y = F/.y by A16,A30,A31,CAT_3:def 1; end; suppose A33: y <> x; then A34: not y in {x} by TARSKI:def 1; A35: y in I\{x} by A30,A33,ZFMISC_1:56; F9/.y = F9.y by A30,FUNCT_2:def 13 .= (i1*G9).y by A20,A22,A30,A34,FUNCT_4:def 1 .= (i1*G9)/.y by A35,FUNCT_2:def 13; hence (doms F9)/.y = dom((i1*G9)/.y) by A30,CAT_3:def 1 .= (doms(i1*G9))/.y by A35,CAT_3:def 1 .= G/.y by A13,A15,A23,CAT_3:17 .= G.y by A35,FUNCT_2:def 13 .= F.y by A30,A33,FUNCT_1:49,ZFMISC_1:56 .= F/.y by A30,FUNCT_2:def 13; end; end; hence (doms F9)/.y = F/.y; end; hence doms F9 = F by CAT_3:1; thus F9 is Injections_family of c,I; let d be Object of C; let F99 be Injections_family of d,I such that A36: doms F9 = doms F99; reconsider G99 = F99|(I\{x}) as Function of I\{x},the carrier' of C by FUNCT_2:32; now let y be set; assume A37: y in I\{x}; then G99/.y = G99.y by FUNCT_2:def 13 .= F99.y by A37,FUNCT_1:49 .= F99/.y by A37,FUNCT_2:def 13; hence cods(G99)/.y = cod(F99/.y) by A37,CAT_3:def 2 .= d by A37,CAT_3:62 .= ((I\{x})-->d)/.y by A37,CAT_3:2; end; then reconsider G99 as Injections_family of d,I\{x} by CAT_3:1,def 16; now let y be set; assume A38: y in I\{x}; then A39: G/.y = G.y by FUNCT_2:def 13 .= F.y by A38,FUNCT_1:49 .= F/.y by A38,FUNCT_2:def 13; F99/.y = F99.y by A38,FUNCT_2:def 13 .= G99.y by A38,FUNCT_1:49 .= G99/.y by A38,FUNCT_2:def 13; hence (doms G9)/.y = dom(G99/.y) by A13,A29,A36,A38,A39,CAT_3:1,def 1 .= (doms G99)/.y by A38,CAT_3:def 1; end; then consider h9 being Morphism of C such that A40: h9 in Hom(a,d) and A41: for k being Morphism of C st k in Hom(a,d) holds (for y being set st y in I\{x} holds k(*)(G9/.y) = G99/.y) iff h9 = k by A14,CAT_3:1; A42: x in {x} by TARSKI:def 1; set g = F99/.x; A43: cod g = d by A12,CARD_1:27,CAT_3:62; A44: F9/.x = F9.x by A12,CARD_1:27,FUNCT_2:def 13 .= (x .-->i2).x by A20,A42,FUNCT_4:13 .= i2 by A42,FUNCOP_1:7; then dom i2 = (doms F9)/.x by A12,CARD_1:27,CAT_3:def 1 .= dom g by A12,A36,CARD_1:27,CAT_3:def 1; then g in Hom(dom i2,d) by A43; then consider h being Morphism of C such that A45: h in Hom(c,d) and A46: for k being Morphism of C st k in Hom(c,d) holds k(*)i1 = h9 & k(*)i2 = g iff h = k by A15,A19,A40; take h; thus h in Hom(c,d) by A45; let k be Morphism of C such that A47: k in Hom(c,d); thus (for y being set st y in I holds k(*)(F9/.y) = F99/.y) implies h = k proof A48: dom k = c by A47,CAT_1:1; then A49: dom(k(*)i1) = a by A15,A17,CAT_1:17; assume A50: for y being set st y in I holds k(*)(F9/.y) = F99/.y; A51: for y being set st y in I\{x} holds k(*)i1(*)(G9/.y) = G99/.y proof let y be set; assume A52: y in I\{x}; then A53: not y in {x} by XBOOLE_0:def 5; A54: F9/.y = F9.y by A52,FUNCT_2:def 13 .= (i1*G9).y by A20,A22,A52,A53,FUNCT_4:def 1 .= (i1*G9)/.y by A52,FUNCT_2:def 13; cod(G9/.y) = a by A52,CAT_3:62; hence k(*)i1(*)(G9/.y) = k(*)(i1(*)(G9/.y)) by A15,A17,A48,CAT_1:18 .= k(*)((i1*G9)/.y) by A52,CAT_3:def 6 .= F99/.y by A50,A52,A54 .= F99.y by A52,FUNCT_2:def 13 .= G99.y by A52,FUNCT_1:49 .= G99/.y by A52,FUNCT_2:def 13; end; cod k = d by A47,CAT_1:1; then cod(k(*)i1) = d by A17,A48,CAT_1:17; then k(*)i1 in Hom(a,d) by A49; then A55: k(*)i1 = h9 by A41,A51; k(*)i2 = g by A12,A44,A50,CARD_1:27; hence thesis by A46,A47,A55; end; assume A56: h = k; let y be set such that A57: y in I; now per cases; suppose A58: y = x; then A59: y in {x} by TARSKI:def 1; F9/.y = F9.y by A57,FUNCT_2:def 13 .= (x .-->i2).y by A20,A59,FUNCT_4:13 .= i2 by A59,FUNCOP_1:7; hence thesis by A46,A47,A56,A58; end; suppose A60: y <> x; then A61: not y in {x} by TARSKI:def 1; A62: dom k = c by A47,CAT_1:1; A63: y in I\{x} by A57,A60,ZFMISC_1:56; A64: cod(G9/.y) = a by A57,A60,CAT_3:62,ZFMISC_1:56; F9/.y = F9.y by A57,FUNCT_2:def 13 .= (i1*G9).y by A20,A22,A57,A61,FUNCT_4:def 1 .= (i1*G9)/.y by A63,FUNCT_2:def 13 .= i1(*)(G9/.y) by A63,CAT_3:def 6; hence k(*)(F9/.y) = k(*)i1(*)(G9/.y) by A15,A17,A62,A64,CAT_1:18 .= h9(*)(G9/.y) by A46,A47,A56 .= G99/.y by A40,A41,A63 .= G99.y by A63,FUNCT_2:def 13 .= F99.y by A57,A60,FUNCT_1:49,ZFMISC_1:56 .= F99/.y by A57,FUNCT_2:def 13; end; end; hence thesis; end; let I be finite set, F be Function of I,the carrier of C; A65: card I = card I; A66: Q[ 0 ] proof let I be finite set, F be Function of I,the carrier of C; assume card I = 0; then A67: I = {}; {} is Function of {}, the carrier' of C by RELSET_1:12; then reconsider F9 = {} as Injections_family of a,I by A67,CAT_3:63; take a,F9; for x being set st x in I holds (doms F9)/.x = F/.x; hence doms F9 = F by CAT_3:1; thus thesis by A8,A67,CAT_3:75; end; for n being Nat holds Q[n] from NAT_1:sch 2(A66,A10); hence thesis by A65; end; definition struct (CatStr)CoprodCatStr (# carrier,carrier' -> set, Source,Target -> Function of the carrier', the carrier, Comp -> PartFunc of [:the carrier', the carrier' :],the carrier', Initial -> Element of the carrier, Coproduct -> Function of [:the carrier,the carrier:] ,the carrier, Incl1,Incl2 -> Function of [:the carrier,the carrier:],the carrier' #); end; registration cluster non void non empty for CoprodCatStr; existence proof set o = the set; take CoprodCatStr(# {o},{o},o:->o,o:->o,(o,o):->o,Extract(o),(o,o) :->o,(o,o):->o,(o,o):->o #); thus thesis; end; end; definition let C be non void non empty CoprodCatStr; func EmptyMS C -> Object of C equals the Initial of C; correctness; let a,b be Object of C; func a+b -> Object of C equals (the Coproduct of C).(a,b); correctness; func in1(a,b) -> Morphism of C equals (the Incl1 of C).(a,b); correctness; func in2(a,b) -> Morphism of C equals (the Incl2 of C).(a,b); correctness; end; definition let o,m; func c1Cat*(o,m) -> strict CoprodCatStr equals CoprodCatStr(# {o},{m},m:->o,m:->o,(m,m):->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #); correctness; end; ::$CT registration let o,m; cluster c1Cat*(o,m) -> non void non empty trivial trivial'; coherence; end; Lm2: c1Cat*(o,m) is Category-like proof set C = c1Cat*(o,m); set CP = the Comp of C, CD = the Source of C, CC = the Target of C; thus for f,g being Morphism of C holds [g,f] in dom CP iff dom g=cod f proof let f,g be Morphism of C; A1: dom CP = {[m,m]} by FUNCOP_1:13; A2: f = m & g = m by TARSKI:def 1; thus [g,f] in dom CP implies dom g=cod f by ZFMISC_1:def 10; thus thesis by A1,A2,TARSKI:def 1; end; end; registration cluster strict Category-like reflexive transitive associative with_identities for non void non empty CoprodCatStr; existence proof c1Cat*(0,1) is reflexive transitive associative with_identities Category-like by Lm2; hence thesis; end; end; registration let o,m be set; cluster c1Cat*(o,m) -> Category-like reflexive transitive associative with_identities non void non empty; coherence by Lm2; end; theorem Th45: for a,b being Object of c1Cat*(o,m) holds a = b proof let a,b be Object of c1Cat*(o,m); a = o by TARSKI:def 1; hence thesis by TARSKI:def 1; end; theorem Th46: for f,g being Morphism of c1Cat*(o,m) holds f = g proof let f,g be Morphism of c1Cat*(o,m); f = m by TARSKI:def 1; hence thesis by TARSKI:def 1; end; theorem Th47: 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); cod f = o by TARSKI:def 1; then A1: cod f = b by TARSKI:def 1; dom f = o by TARSKI:def 1; then dom f = a by TARSKI:def 1; hence thesis by A1; 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 Th47; hence thesis by CAT_1:def 5; end; theorem for a,b being Object of c1Cat*(o,m) holds Hom(a,b) <> {} by Th47; theorem Th50: 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); set f = the Morphism of a,b; thus Hom(a,b)<>{} by Th47; take f; thus thesis by Th46; end; theorem Th51: 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 Th45; let d be Object of c1Cat*(o,m), f,g be Morphism of c1Cat*(o,m) such that f in Hom(dom i1,d) and g in Hom(dom i2,d); take h = i1; thus h in Hom(c,d) by Th47; thus thesis by Th46; end; definition let IT be Category-like reflexive transitive associative with_identities non void non empty CoprodCatStr; attr IT is Cocartesian means :Def26: 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 Th52: for o,m being set holds c1Cat*(o,m) is Cocartesian by Th50,Th45,Th51; registration cluster strict Cocartesian for reflexive transitive associative with_identities Category-like non void non empty CoprodCatStr; existence proof c1Cat*(0,1) is Cocartesian by Th52; hence thesis; end; end; definition mode Cocartesian_category is Cocartesian reflexive transitive associative with_identities Category-like non void non empty CoprodCatStr; end; reserve C for Cocartesian_category; reserve a,b,c,d,e,s for Object of C; theorem EmptyMS C is initial by Def26; theorem Th54: for f1,f2 being Morphism of EmptyMS C,a holds f1 = f2 proof let f1,f2 be Morphism of EmptyMS C,a; EmptyMS C is initial by Def26; then consider f being Morphism of EmptyMS C,a such that A1: for g being Morphism of EmptyMS C, a holds f = g; thus f1 = f by A1 .= f2 by A1; end; definition let C,a; func init a -> Morphism of EmptyMS C, a means not contradiction; existence; uniqueness by Th54; end; theorem Th55: Hom(EmptyMS C,a) <> {} proof EmptyMS C is initial by Def26; hence thesis; end; theorem Th56: init a = init(EmptyMS C,a) proof EmptyMS C is initial by Def26; hence thesis by CAT_3:40; end; theorem dom(init a) = EmptyMS C & cod(init a) = a proof EmptyMS C is initial & init a = init(EmptyMS C,a) by Def26,Th56; hence thesis by CAT_3:38; end; theorem Hom(EmptyMS C,a) = {init a} proof for f2 being Morphism of EmptyMS C,a holds init a = f2 by Th54; hence thesis by Th55,CAT_1:8; end; theorem Th59: 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); a+b is_a_coproduct_wrt i1,i2 by Def26; hence thesis by Def26; end; theorem Th60: 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); a+b is_a_coproduct_wrt i1,i2 by Def26; hence thesis by Def26; end; theorem Th61: 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 Def26; then A1: cod i1 = c & cod i2 = c; dom(i1) = a & dom(i2) = b by Def26; hence thesis by A1,CAT_1:1; end; theorem a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Def26; theorem C is with_finite_coproduct proof A1: 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 Def26,Th59,Th60; end; EmptyMS C is initial by Def26; hence thesis by A1,Th44; end; definition let C,a,b; redefine func in1(a,b) -> Morphism of a,a+b; coherence proof dom in1(a,b) = a & cod in1(a,b) = a+b by Th59; hence thesis by CAT_1:4; end; redefine func in2(a,b) -> Morphism of b,a+b; coherence proof dom in2(a,b) = b & cod in2(a,b) = a+b by Th60; hence thesis by CAT_1:4; end; end; theorem Hom(a,b) <> {} & Hom(b,a) <> {} implies in1(a,b) is coretraction & in2 (a,b) is coretraction proof A1: Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th61; a+b is_a_coproduct_wrt in1(a,b),in2(a,b) & dom in1(a,b) = a by Def26; hence thesis by A1,CAT_3:82; 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 Th59; hence thesis; end; redefine func in2(a,b) -> Morphism of b,a+b; coherence proof cod in2(a,b) = a+b & dom in2(a,b) = b by Th60; hence thesis; 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 :Def28: it*in1(a,b) = f & it*in2(a,b ) = g; existence proof A2: a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Def26; Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th61; then consider h being Morphism of a+b,c such that A3: for k being Morphism of a+b,c holds k*in1(a,b) = f & k*in2(a,b) = g iff h = k by A1,A2,CAT_3:81; take h; thus thesis by A3; end; uniqueness proof A4: Hom(b,a+b) <> {} by Th61; a+b is_a_coproduct_wrt in1(a,b),in2(a,b) & Hom(a,a+b) <> {} by Def26,Th61; 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,A4,CAT_3:81; let h1,h2 be Morphism of a+b,c such that A6: h1*in1(a,b) = f & h1*in2(a,b) = g and A7: h2*in1(a,b) = f & h2*in2(a,b) = g; h1 = h by A6,A5; hence thesis by A7,A5; end; end; theorem Th65: Hom(a,c) <> {} & Hom(b,c) <> {} implies Hom(a+b,c) <> {} proof A1: a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Def26; Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th61; hence thesis by A1,CAT_3:81; end; theorem Th66: [$in1(a,b),in2(a,b)$] = id(a+b) proof A1: Hom(b,a+b) <> {} by Th61; then A2: (id(a+b))*in2(a,b) = in2(a,b) by CAT_1:28; A3: Hom(a,a+b) <> {} by Th61; then (id(a+b))*in1(a,b) = in1(a,b) by CAT_1:28; hence thesis by A3,A1,A2,Def28; end; theorem Th67: 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)<>{} & Hom(b,c)<>{} and A2: Hom(c,d)<>{}; A3: Hom(a+b,c) <> {} by A1,Th65; A4: Hom(b,a+b) <> {} by Th61; h*([$f,g$]*in2(a,b)) = h*g by A1,Def28; then A5: h*[$f,g$]*in2(a,b) = h*g by A2,A4,A3,CAT_1:25; A6: Hom(a,a+b) <> {} by Th61; A7: Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,CAT_1:24; h*([$f,g$]*in1(a,b)) = h*f by A1,Def28; then h*[$f,g$]*in1(a,b) = h*f by A2,A6,A3,CAT_1:25; hence thesis by A5,A7,Def28; end; theorem Th68: 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 A1: Hom(a,c) <> {} & Hom(b,c) <> {}; then [$f,g$]*in1(a,b) = f & [$f,g$]*in2(a,b) = g by Def28; hence thesis by A1,Def28; 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: g is epi; let d be Object of C, f1,f2 be Morphism of c,d such that A6: Hom(c,d)<>{} and A7: f1*[$f,g$] = f2*[$f,g$]; A8: Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A6,CAT_1:24; [$f1*f,f1*g$] = f1*[$f,g$] & [$f2*f,f2*g$] = f2*[$f,g$] by A1,A2,A6,Th67; then f1*g = f2*g by A7,A8,Th68; hence f1 = f2 by A5,A6; end; A9: now assume A10: f is epi; let d; let f1,f2 be Morphism of c,d such that A11: Hom(c,d)<>{} and A12: f1*[$f,g$] = f2*[$f,g$]; A13: Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A11,CAT_1:24; [$f1*f,f1*g$] = f1*[$f,g$] & [$f2*f,f2*g$] = f2*[$f,g$] by A1,A2,A11,Th67; then f1*f = f2*f by A12,A13,Th68; hence f1 = f2 by A10,A11; end; Hom(a+b,c) <> {} by A1,A2,Th65; hence thesis by A3,A9,A4; end; theorem a, a+EmptyMS C are_isomorphic & a,EmptyMS C+a are_isomorphic proof A1: in2(EmptyMS C,a)*init a = in1(EmptyMS C,a) by Th54; A2: Hom(EmptyMS C,a) <> {} & Hom(a,a) <> {} by Th55; thus a,a+EmptyMS C are_isomorphic proof thus A3: Hom(a,a+EmptyMS C) <> {} by Th61; thus Hom(a+EmptyMS C,a) <> {} by A2,Th65; take g = in1(a,EmptyMS C), f = [$id a,init a$]; A4: in1(a,EmptyMS C)*init a = in2(a,EmptyMS C) by Th54; in1(a,EmptyMS C)*id(a) = in1(a,EmptyMS C) by A3,CAT_1:29; then g*f = [$in1(a,EmptyMS C),in2(a,EmptyMS C)$] by A2,A3,A4,Th67; hence thesis by A2,Def28,Th66; end; thus A5: Hom(a,EmptyMS C+a) <> {} by Th61; thus Hom(EmptyMS C+a,a) <> {} by A2,Th65; take g = in2(EmptyMS C,a), f = [$init a,id a$]; in2(EmptyMS C,a)*id(a) = in2(EmptyMS C,a) by A5,CAT_1:29; then g*f = [$in1(EmptyMS C,a),in2(EmptyMS C,a)$] by A2,A5,A1,Th67; hence thesis by A2,Def28,Th66; end; theorem a+b,b+a are_isomorphic proof A1: Hom(a,b+a) <> {} & Hom(b,b+a) <> {} by Th61; hence A2: Hom(a+b,b+a)<>{} by Th65; A3: Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th61; hence A4: Hom(b+a,a+b)<>{} by Th65; take f9 = [$in2(b,a),in1(b,a)$], f = [$in2(a,b),in1(a,b)$]; thus f9*f = [$f9*in2(a,b),f9*in1(a,b)$] by A2,A3,Th67 .= [$in1(b,a),f9*in1(a,b)$] by A1,Def28 .= [$in1(b,a),in2(b,a)$] by A1,Def28 .= id(b+a) by Th66; thus f*f9 = [$f*in2(b,a),f*in1(b,a)$] by A1,A4,Th67 .= [$in1(a,b),f*in1(b,a)$] by A3,Def28 .= [$in1(a,b),in2(a,b)$] by A3,Def28 .= id(a+b) by Th66; end; theorem (a+b)+c,a+(b+c) are_isomorphic proof 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)$]; A1: Hom(b+c,a+(b+c)) <> {} by Th61; A2: Hom(b,b+c) <> {} by Th61; then A3: Hom(b,a+(b+c)) <> {} by A1,CAT_1:24; A4: Hom(a,a+(b+c)) <> {} by Th61; then A5: Hom(a+b,a+(b+c)) <> {} by A3,Th65; A6: Hom(c,b+c) <> {} by Th61; then A7: Hom(c,a+(b+c)) <> {} by A1,CAT_1:24; hence A8: Hom((a+b)+c,a+(b+c)) <> {} by A5,Th65; A9: Hom(a+b,(a+b)+c) <> {} by Th61; A10: Hom(b,a+b) <> {} by Th61; then A11: Hom(b,(a+b)+c) <> {} by A9,CAT_1:24; A12: Hom(c,(a+b)+c) <> {} by Th61; then A13: Hom(b+c,(a+b)+c) <> {} by A11,Th65; A14: Hom(a,a+b) <> {} by Th61; then A15: Hom(a,(a+b)+c) <> {} by A9,CAT_1:24; hence A16: Hom(a+(b+c),(a+b)+c) <> {} by A13,Th65; take g = [$l,in2(a,b+c)*in2(b,c)$]; g*(in1(a+b,c)*in2(a,b)) = (g*in1(a+b,c))*in2(a,b) by A8,A9,A10,CAT_1:25 .= l*in2(a,b) by A7,A5,Def28 .= in2(a,b+c)*in1(b,c) by A3,A4,Def28; then A17: g*k = [$in2(a,b+c)*in1(b,c),g*in2(a+b,c)$] by A8,A11,A12,Th67 .= [$in2(a,b+c)*in1(b,c),in2(a,b+c)*in2(b,c)$] by A7,A5,Def28 .= in2(a,b+c)*[$in1(b,c),in2(b,c)$] by A2,A1,A6,Th67 .= in2(a,b+c)*id(b+c) by Th66 .= in2(a,b+c) by A1,CAT_1:29; take f = [$in1(a+b,c)*in1(a,b),k$]; f*(in2(a,b+c)*in1(b,c)) = (f*in2(a,b+c))*in1(b,c) by A2,A1,A16,CAT_1:25 .= k*in1(b,c) by A15,A13,Def28 .= in1(a+b,c)*in2(a,b) by A11,A12,Def28; then A18: f*l = [$f*in1(a,b+c),in1(a+b,c)*in2(a,b)$] by A3,A4,A16,Th67 .= [$in1(a+b,c)*in1(a,b),in1(a+b,c)*in2(a,b)$] by A15,A13,Def28 .= in1(a+b,c)*[$in1(a,b),in2(a,b)$] by A14,A9,A10,Th67 .= in1(a+b,c)*id(a+b) by Th66 .= in1(a+b,c) by A9,CAT_1:29; g*(in1(a+b,c)*in1(a,b)) = g*in1(a+b,c)*in1(a,b) by A8,A14,A9,CAT_1:25 .= l*in1(a,b) by A7,A5,Def28 .= in1(a,b+c) by A3,A4,Def28; hence g*f = [$in1(a,b+c),in2(a,b+c)$] by A8,A15,A13,A17,Th67 .= id(a+(b+c)) by Th66; f*(in2(a,b+c)*in2(b,c)) = (f*in2(a,b+c))*in2(b,c) by A1,A6,A16,CAT_1:25 .= k*in2(b,c) by A15,A13,Def28 .= in2(a+b,c) by A11,A12,Def28; hence f*g = [$in1(a+b,c),in2(a+b,c)$] by A7,A5,A16,A18,Th67 .= id((a+b)+c) by Th66; end; definition let C,a; func nabla a -> Morphism of a+a,a equals [$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 [$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 that A1: Hom(a,c) <> {} and A2: Hom(b,d) <> {}; Hom(d,c+d) <> {} by Th61; then A3: Hom(b,c+d) <> {} by A2,CAT_1:24; Hom(c,c+d) <> {} by Th61; then Hom(a,c+d) <> {} by A1,CAT_1:24; hence thesis by A3,Th65; end; theorem (id a)+(id b) = id(a+b) proof Hom(b,a+b) <> {} by Th61; then A1: in2(a,b)*(id b) = in2(a,b) by CAT_1:29; Hom(a,a+b) <> {} by Th61; then in1(a,b)*(id a) = in1(a,b) by CAT_1:29; hence thesis by A1,Th66; end; theorem Th75: 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) <> {} & Hom(d,e) <> {}; A4: Hom(c+d,e) <> {} by A3,Th65; A5: Hom(d,c+d) <> {} by Th61; then A6: Hom(b,c+d) <> {} by A2,CAT_1:24; A7: Hom(c,c+d) <> {} by Th61; then A8: Hom(a,c+d) <> {} by A1,CAT_1:24; [$g,k$]*in2(c,d) = k by A3,Def28; then A9: k*h = [$g,k$]*(in2(c,d)*h) by A2,A4,A5,CAT_1:25; [$g,k$]*in1(c,d) = g by A3,Def28; then g*f = [$g,k$]*(in1(c,d)*f) by A1,A4,A7,CAT_1:25; hence thesis by A4,A8,A6,A9,Th67; 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) <> {}; Hom(c,c) <> {}; hence nabla(c)*(f+g) = [$(id c)*f,(id c)*g$] by A1,A2,Th75 .= [$f,(id c)*g$] by A1,CAT_1:28 .= [$f,g$] by A2,CAT_1:28; 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(s,e+s) <> {} by Th61; then A6: Hom(d,e+s) <> {} by A4,CAT_1:24; A7: Hom(e,e+s) <> {} by Th61; then in1(e,s)*g*f = in1(e,s)*(g*f) by A1,A3,CAT_1:25; then A8: (g*f)+(k*h) = [$in1(e,s)*g*f,in2(e,s)*k*h$] by A2,A4,A5,CAT_1:25; Hom(c,e+s) <> {} by A3,A7,CAT_1:24; hence thesis by A1,A2,A6,A8,Th75; end;