:: Categorial Categories and Slice Categories :: by Grzegorz Bancerek :: :: Received October 24, 1994 :: Copyright (c) 1994-2012 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 XBOOLE_0, SUBSET_1, ZFMISC_1, MCART_1, CAT_1, STRUCT_0, RELAT_1, GRAPH_1, FUNCT_1, CARD_1, TARSKI, PARTFUN1, CAT_2, REALSET1, GROUP_6, SETFAM_1, GRCAT_1, FUNCT_3, CAT_5, MONOID_0, RELAT_2, BINOP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, MCART_1, DOMAIN_1, RELAT_1, REALSET1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, BINOP_1, STRUCT_0, GRAPH_1, CAT_1, CAT_2; constructors SETFAM_1, PARTFUN1, REALSET1, NATTRA_1, FUNCOP_1, RELSET_1, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, REALSET1, CAT_1, CAT_2, STRUCT_0, RELAT_1, XTUPLE_0; requirements SUBSET, BOOLE; definitions TARSKI, FUNCT_1, CAT_1, CAT_2, XBOOLE_0, REALSET1, BINOP_1, GRAPH_1, XTUPLE_0; theorems TARSKI, ZFMISC_1, SETFAM_1, MCART_1, FUNCT_1, FUNCT_2, GRFUNC_1, PARTFUN1, CAT_1, CAT_2, NATTRA_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, BINOP_1, XTUPLE_0; schemes FUNCT_1, FUNCT_2, BINOP_1, XBOOLE_0; begin :: Categories with Triple-like Morphisms theorem Th1: for C being Category, D being non empty non void CatStr st the CatStr of C = the CatStr of D holds D is Category-like transitive associative reflexive with_identities proof let C be Category, D be non empty non void CatStr such that A1: the CatStr of C = the CatStr of D; thus A2: for f,g being Morphism of D holds [g,f] in dom(the Comp of D) iff dom g=cod f proof let f,g be Morphism of D; reconsider ff=f, gg=g as Morphism of C by A1; A3: [gg,ff] in dom(the Comp of D) iff dom gg=cod ff by A1,CAT_1:def 6; thus [g,f] in dom(the Comp of D) implies dom g=cod f proof assume A4: [g,f] in dom the Comp of D; thus dom g = dom gg by A1 .= cod ff by A4,A1,CAT_1:def 6 .= cod f by A1; end; thus thesis by A1,A3; end; thus A5: for f,g being Morphism of D st dom g=cod f holds dom(g(*)f) = dom f & cod(g(*)f) = cod g proof let f,g be Morphism of D; reconsider ff=f, gg=g as Morphism of C by A1; assume A6: dom g = cod f; A7: dom gg = cod ff by A1,A6; then [gg,ff] in dom(the Comp of C) by CAT_1:def 6; then A8: (the Comp of C).(gg,ff) = gg(*)ff by CAT_1:def 1; dom(gg(*)ff) = dom ff & cod(gg(*)ff) = cod gg by A7,CAT_1:def 7; hence thesis by A1,A8,A6,A2,CAT_1:def 1; end; A9: for f,g being Morphism of D st cod g = dom f for ff,gg being Morphism of C st ff=f & gg=g holds f(*)g = ff(*)gg proof let f,g be Morphism of D such that A10: cod g = dom f; let ff,gg be Morphism of C such that A11: ff=f & gg=g; A12: cod gg = dom ff by A10,A11,A1; thus f(*)g = (the Comp of D).(f,g) by CAT_1:def 1,A10,A2 .= (the Comp of C).(ff,gg) by A1,A11 .= ff(*)gg by A12,CAT_1:16; end; thus for f,g,h being Morphism of D st dom h = cod g & dom g = cod f holds h(*)(g(*)f) = (h(*)g)(*)f proof let f,g,h being Morphism of D; reconsider ff=f, gg=g, hh=h as Morphism of C by A1; assume that A13: dom h = cod g and A14: dom g = cod f; A15: dom hh = cod gg & dom gg = cod ff by A13,A14,A1; A16: g(*)f = gg(*)ff by A14,A9; A17: h(*)g = hh(*)gg by A13,A9; A18: dom(h(*)g) = dom g by A13,A5; cod(g(*)f) = cod g by A14,A5; hence h(*)(g(*)f) = hh(*)(gg(*)ff) by A9,A16,A13 .= hh(*)gg(*)ff by A15,CAT_1:def 8 .= (h(*)g)(*)f by A14,A9,A17,A18; end; thus D is reflexive proof let b be Element of D; reconsider bb = b as Element of C by A1; reconsider ii = id bb as Morphism of D by A1; A19: cod ii = cod id bb by A1 .= b; dom ii = dom id bb by A1 .= b; then id bb in Hom(b,b) by A19; hence Hom(b,b)<>{}; end; let a be Element of D; reconsider aa = a as Element of C by A1; reconsider ii = id aa as Morphism of D by A1; A20: cod ii = cod id aa by A1 .= a; dom ii = dom id aa by A1 .= a; then reconsider ii as Morphism of a,a by A20,CAT_1:4; take ii; let b be Element of D; reconsider bb = b as Element of C by A1; thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g proof assume A21: Hom(a,b)<>{}; let g be Morphism of a,b; reconsider gg = g as Morphism of C by A1; A22: cod gg = cod g by A1 .= bb by A21,CAT_1:5; A23: cod id aa = aa; A24: dom gg = dom g by A1 .= aa by A21,CAT_1:5; then gg in Hom(aa,bb) by A22; then reconsider gg as Morphism of aa,bb by CAT_1:def 5; A25: dom g = dom gg by A1 .= a by A24; cod ii = cod id aa by A1 .= a; hence g(*)ii = (the Comp of D).(g,ii) by CAT_1:def 1,A25,A2 .= (the Comp of C).(gg,id aa) by A1 .= gg(*)id aa by A23,A24,CAT_1:16 .= g by A24,CAT_1:22; end; assume A26: Hom(b,a)<>{}; let g be Morphism of b,a; reconsider gg = g as Morphism of C by A1; A27: dom gg = dom g by A1 .= bb by A26,CAT_1:5; A28: dom id aa = aa; A29: cod gg = cod g by A1 .= aa by A26,CAT_1:5; then gg in Hom(bb,aa) by A27; then reconsider gg as Morphism of bb,aa by CAT_1:def 5; A30: cod g = cod gg by A1 .= a by A29; dom ii = dom id aa by A1 .= a; hence ii(*)g = (the Comp of D).(ii,g) by CAT_1:def 1,A30,A2 .= (the Comp of C).(id aa,gg) by A1 .= (id aa)(*)gg by A28,A29,CAT_1:16 .= g by A29,CAT_1:21; end; Lm1: for C,D being Category st the CatStr of C = the CatStr of D holds for c being Element of C, d being Element of D st c = d holds id c = id d proof let C,D be Category such that A1: the CatStr of C = the CatStr of D; let c be Element of C, d be Element of D such that A2: c = d; reconsider ii = id c as Morphism of D by A1; A3: cod ii = cod id c by A1 .= d by A2; A4: dom ii = dom id c by A1 .= d by A2; then reconsider ii as Morphism of d,d by A3,CAT_1:4; for b being Object of D holds (Hom(d,b) <> {} implies for f being Morphism of d,b holds f(*)ii = f) & (Hom(b,d) <> {} implies for f being Morphism of b,d holds ii(*)f = f) proof let b be Object of D; reconsider bb = b as Element of C by A1; thus Hom(d,b) <> {} implies for f being Morphism of d,b holds f(*)ii = f proof assume A5: Hom(d,b) <> {}; let f be Morphism of d,b; reconsider ff=f as Morphism of C by A1; A6: dom ff = dom f by A1 .= c by A2,A5,CAT_1:5; A7: cod id c = c .= dom ff by A6; cod ii = d by A3 .= dom f by A5,CAT_1:5; hence f(*)ii = (the Comp of D).(f,ii) by CAT_1:16 .= (the Comp of C).(ff,id c) by A1 .= ff(*)id c by A7,CAT_1:16 .= f by A6,CAT_1:22; end; assume A8: Hom(b,d) <> {}; let f be Morphism of b,d; reconsider ff=f as Morphism of C by A1; A9: cod ff = cod f by A1 .= c by A2,A8,CAT_1:5; A10: dom id c = c .= cod ff by A9; dom ii = d by A4 .= cod f by A8,CAT_1:5; hence ii(*)f = (the Comp of D).(ii,f) by CAT_1:16 .= (the Comp of C).(id c,ff) by A1 .= (id c)(*)ff by A10,CAT_1:16 .= f by A9,CAT_1:21; end; hence id c = id d by CAT_1:def 12; end; definition let IT be non void non empty CatStr; attr IT is with_triple-like_morphisms means :Def1: for f being Morphism of IT ex x being set st f = [[dom f, cod f], x]; end; registration cluster with_triple-like_morphisms for strict Category; existence proof take C = 1Cat(0, [[0,0], 1]); let f be Morphism of C; take 1; dom f = 0 by TARSKI:def 1; hence thesis by TARSKI:def 1; end; end; theorem Th2: for C being with_triple-like_morphisms non void non empty CatStr, f being Morphism of C holds dom f = f`11 & cod f = f`12 & f = [[dom f, cod f], f`2] proof let C be with_triple-like_morphisms non void non empty CatStr; let f be Morphism of C; ex x being set st ( f = [[dom f, cod f], x]) by Def1; hence thesis by MCART_1:7,85; end; definition let C be with_triple-like_morphisms non void non empty CatStr; let f be Morphism of C; redefine func f`11 -> Object of C; coherence proof f`11 = dom f by Th2; hence thesis; end; redefine func f`12 -> Object of C; coherence proof f`12 = cod f by Th2; hence thesis; end; end; scheme CatEx { A, B() -> non empty set, P[set, set, set], F(set,set) -> set }: ex C being with_triple-like_morphisms strict Category st the carrier of C = A() & (for a,b being Element of A(), f being Element of B() st P[a,b,f] holds [[a,b],f] is Morphism of C) & (for m being Morphism of C ex a,b being Element of A(), f being Element of B() st m = [[a,b],f] & P[a,b,f]) & for m1,m2 being (Morphism of C), a1,a2,a3 being Element of A(), f1,f2 being Element of B() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], F(f2,f1)] provided A1: for a,b,c being Element of A(), f,g being Element of B() st P[a,b,f] & P[b,c,g] holds F(g,f) in B() & P[a,c,F(g,f)] and A2: for a being Element of A() ex f being Element of B() st P[a,a,f] & for b being Element of A(), g being Element of B() holds (P[a,b,g] implies F(g,f) = g) & (P[b,a,g] implies F(f,g) = g) and A3: for a,b,c,d being Element of A(), f,g,h being Element of B() st P[a,b,f] & P[b,c,g] & P[c,d,h] holds F(h, F(g,f)) = F(F(h,g), f) proof set M = {[[a,b],f] where a is Element of A(), b is Element of A(), f is Element of B(): P[a,b,f]}; set a0 = the Element of A(); consider f0 being Element of B() such that A4: P[a0,a0,f0] and for b being Element of A(), g being Element of B() holds (P[a0,b,g] implies F(g,f0) = g) & (P[b,a0,g] implies F(f0,g) = g) by A2; A5: [[a0,a0],f0] in M by A4; M c= [:[:A(),A():],B():] proof let x be set; assume x in M; then ex a, b being Element of A(), f being Element of B() st x = [[a,b],f] & P[a,b,f]; hence thesis; end; then reconsider M as non empty Subset of [:[:A(),A():],B():] by A5; A6: now let m be Element of M; m in M; then consider a,b being Element of A(), f being Element of B() such that A7: m = [[a,b],f] and A8: P[a,b,f]; A9: m`11 = a by A7,MCART_1:85; m`12 = b by A7,MCART_1:85; hence m = [[m`11,m`12],m`2] & P[m`11,m`12,m`2] by A7,A8,A9,MCART_1:7; end; deffunc f(Element of M) = $1`11; consider DM being Function of M, A() such that A10: for m being Element of M holds DM.m = f(m) from FUNCT_2:sch 4; deffunc g(Element of M) = $1`12; consider CM being Function of M, A() such that A11: for m being Element of M holds CM.m = g(m) from FUNCT_2:sch 4; deffunc f(set,set) = [[$2`11,$1`12],F($1`2,$2`2)]; defpred P[set,set] means $1`11 = $2`12 & $1 in M & $2 in M; A12: now let x,y be set; assume A13: P[x,y]; then consider ax, bx being Element of A(), fx being Element of B() such that A14: x = [[ax,bx],fx] and A15: P[ax,bx,fx]; consider ay, b2 being Element of A(), fy being Element of B() such that A16: y = [[ay,b2],fy] and A17: P[ay,b2,fy] by A13; A18: x`11 = ax by A14,MCART_1:85; A19: x`12 = bx by A14,MCART_1:85; A20: y`11 = ay by A16,MCART_1:85; A21: y`12 = b2 by A16,MCART_1:85; A22: x`2 = fx by A14,MCART_1:7; A23: y`2 = fy by A16,MCART_1:7; A24: F(fx,fy) in B() by A1,A13,A15,A17,A18,A21; P[ay,bx,F(fx,fy)] by A1,A13,A15,A17,A18,A21; hence f(x,y) in M by A19,A20,A22,A23,A24; end; consider CC being PartFunc of [:M,M:], M such that A25: for x,y being set holds [x,y] in dom CC iff x in M & y in M & P[x,y] and A26: for x,y being set st [x,y] in dom CC holds CC.(x,y) = f(x,y) from BINOP_1:sch 6(A12); defpred II[Element of A(), set] means ex f being Element of B() st $2 = [[$1,$1], f] & P[$1,$1,f] & for b being Element of A(), g being Element of B() holds (P[$1,b,g] implies F(g,f) = g) & (P[b,$1,g] implies F(f,g) = g); A27: now let a be Element of A(); consider f being Element of B() such that A28: P[a,a,f] and A29: for b being Element of A(), g being Element of B() holds (P[a,b,g] implies F(g,f) = g) & (P[b,a,g] implies F(f,g) = g) by A2; [[a,a],f] in M by A28; then reconsider y = [[a,a],f] as Element of M; take y; thus II[a,y] by A28,A29; end; consider I being Function of A(), M such that A30: for o being Element of A() holds II[o,I.o] from FUNCT_2:sch 3(A27); set C = CatStr (# A(),M,DM,CM,CC #); A31: C is Category-like proof thus now let f,g be Morphism of C; A32: [g,f] in dom CC iff g in M & f in M & g`11 = f`12 & g in M & f in M by A25; DM.g = g`11 by A10; hence [g,f] in dom(the Comp of C) iff dom g=cod f by A11,A32; end; end; A33: for f,g be Morphism of C holds [g,f] in dom(the Comp of C) iff dom g=cod f by A31,CAT_1:def 6; A34: C is transitive proof let f,g be Morphism of C; A35: (the Source of C).f = f`11 by A10; A36: (the Source of C).g = g`11 by A10; A37: (the Target of C).f = f`12 by A11; A38: (the Target of C).g = g`12 by A11; assume A39: dom g=cod f; then A40: CC.(g,f) = [[f`11,g`12],F(g`2,f`2)] by A26,A25,A36,A37; A41: (CC.[g,f])`11 = f`11 by A40,MCART_1:85; A42: (the Comp of C).(g,f) = g(*)f by A39,CAT_1:def 1,A25,A36,A37; (CC.[g,f])`12 = g`12 by A40,MCART_1:85; hence dom(g(*)f) = dom f & cod(g(*)f) = cod g by A10,A11,A35,A38,A41,A42; end; A43: C is associative proof let f,g,h be Morphism of C; A44: (the Source of C).g = g`11 by A10; A45: (the Source of C).h = h`11 by A10; A46: (the Target of C).f = f`12 by A11; A47: (the Target of C).g = g`12 by A11; assume that A48: dom h = cod g and A49: dom g = cod f; A50: [g,f] in dom CC by A25,A44,A46,A49; A51: [h,g] in dom CC by A25,A45,A47,A48; A52: CC.[g,f] in rng CC by A50,FUNCT_1:def 3; CC.[h,g] in rng CC by A51,FUNCT_1:def 3; then reconsider gf = CC.(g,f), hg = CC.(h,g) as Element of M by A52; A53: gf = [[f`11,g`12],F(g`2,f`2)] by A26,A25,A44,A46,A49; A54: hg = [[g`11,h`12],F(h`2,g`2)] by A26,A25,A45,A47,A48; A55: DM.gf = gf`11 by A10; A56: DM.hg = hg`11 by A10; A57: CM.gf = gf`12 by A11; A58: CM.hg = hg`12 by A11; A59: DM.gf = f`11 by A53,A55,MCART_1:85; A60: CM.gf = g`12 by A53,A57,MCART_1:85; A61: CM.hg = h`12 by A54,A58,MCART_1:85; A62: [h,gf] in dom CC by A25,A45,A11,A48,A57,A60; A63: [hg,f] in dom CC by A25,A44,A46,A49,A56,A54,MCART_1:85; reconsider f9 = f, g9 = g, h9 = h as Element of M; A64: P[f9`11,f9`12,f9`2] by A6; A65: P[g9`11,g9`12,g9`2] by A6; A66: P[h9`11,h9`12,h9`2] by A6; A67: (the Comp of C).(h,g) = h(*)g by CAT_1:def 1,A33,A48; A68: dom(h(*)g) = dom g by A34,CAT_1:def 7,A48; A69: (the Comp of C).(g,f) = g(*)f by CAT_1:def 1,A33,A49; cod(g(*)f) = cod g by A34,CAT_1:def 7,A49; hence h(*)(g(*)f) = (the Comp of C).(h,(the Comp of C).(g,f)) by A69,CAT_1:def 1,A33,A48 .= [[f`11,h`12], F(h`2,gf`2)] by A26,A55,A59,A62 .= [[f`11,h`12], F(h9`2,F(g9`2,f9`2))] by A53,MCART_1:7 .= [[f`11,h`12], F(F(h9`2,g9`2),f9`2)] by A3,A44,A45,A46,A47,A48,A49 ,A64,A65,A66 .= [[f`11,h`12], F(hg`2,f`2)] by A54,MCART_1:7 .= (the Comp of C).((the Comp of C).(h,g),f) by A26,A58,A61,A63 .= h(*)g(*)f by A67,A33,A49,CAT_1:def 1,A68; end; A70: C is reflexive proof let b be Object of C; consider f being Element of B() such that A71: I.b = [[b,b], f] and P[b,b,f] and for c being Element of A(), g being Element of B() holds (P[b,c,g] implies F(g,f) = g) & (P[c,b,g] implies F(f,g) = g) by A30; reconsider bb = b as Element of A(); reconsider Ib = I.bb as Element of M; reconsider ii = I.bb as Morphism of C; A72: cod ii = (I.b)`12 by A11 .= b by A71,MCART_1:85; dom ii = (I.b)`11 by A10 .= b by A71,MCART_1:85; then I.b in Hom(b,b) by A72; hence Hom(b,b)<>{}; end; C is with_identities proof let a be Object of C; consider f being Element of B() such that A73: I.a = [[a,a], f] and P[a,a,f] and A74: for c being Element of A(), g being Element of B() holds (P[a,c,g] implies F(g,f) = g) & (P[c,a,g] implies F(f,g) = g) by A30; reconsider aa = a as Element of A(); reconsider Ia = I.aa as Element of M; reconsider ii = I.aa as Morphism of C; A75: cod ii = (I.a)`12 by A11 .= a by A73,MCART_1:85; dom ii = (I.a)`11 by A10 .= a by A73,MCART_1:85; then reconsider ii as Morphism of a,a by A75,CAT_1:4; take ii; let b be Element of C; thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g proof assume A76: Hom(a,b)<>{}; let g be Morphism of a,b; reconsider bb = b as Element of A(); g in M; then consider a1,b1 being Element of A(), f1 being Element of B() such that A77: g =[[a1,b1],f1] and A78: P[a1,b1,f1]; A79: a = dom g by A76,CAT_1:5 .= DM.g .= [[a1,b1],f1]`11 by A77,A10 .= a1 by MCART_1:85; then A80: F(f1,f) = f1 by A74,A78; A81: [[a,a], f]`11 = a1 by A79,MCART_1:85; A82: [[a,a], f]`2 = f; A83: [[a1,b1],f1]`12 = b1 by MCART_1:85; A84: [[a1,b1],f1]`2 = f1; g`11 = [[a1,b1],f1]`11 by A77 .= a by A79,MCART_1:85 .= [[a,a], f]`12 by MCART_1:85 .= ii`12 by A73; then A85: [g,ii] in dom CC by A25; hence g(*)ii = (the Comp of C).(g,ii) by CAT_1:def 1 .= CC.(g,ii) .= [[ii`11,g`12],F(g`2,ii`2)] by A26,A85 .= [[a1,b1],f1] by A80,A81,A82,A83,A84,A77,A73 .= g by A77; end; thus Hom(b,a)<>{} implies for f being Morphism of b,a holds ii(*)f = f proof assume A86: Hom(b,a)<>{}; let g be Morphism of b,a; reconsider bb = b as Element of A(); g in M; then consider b1,a1 being Element of A(), f1 being Element of B() such that A87: g =[[b1,a1],f1] and A88: P[b1,a1,f1]; A89: a = cod g by A86,CAT_1:5 .= CM.g .= [[b1,a1],f1]`12 by A87,A11 .= a1 by MCART_1:85; then A90: F(f,f1) = f1 by A74,A88; A91: [[a,a], f]`12 = a1 by A89,MCART_1:85; A92: [[a,a], f]`2 = f; A93: [[b1,a1],f1]`11 = b1 by MCART_1:85; A94: [[b1,a1],f1]`2 = f1; g`12 = [[b1,a1],f1]`12 by A87 .= a by A89,MCART_1:85 .= [[a,a], f]`11 by MCART_1:85 .= ii`11 by A73; then A95: [ii,g] in dom CC by A25; hence ii(*)g = (the Comp of C).(ii,g) by CAT_1:def 1 .= CC.(ii,g) .= [[g`11,ii`12],F(ii`2,g`2)] by A26,A95 .= [[b1,a1],f1] by A90,A91,A92,A93,A94,A87,A73 .= g by A87; end; end; then reconsider C as strict Category by A31,A34,A43,A70; C is with_triple-like_morphisms proof let f be Morphism of C; f in M; then consider a, b being Element of A(), g being Element of B() such that A96: f = [[a,b],g] and P[a,b,g]; take g; A97: dom f = f`11 by A10 .= a by A96,MCART_1:85; cod f = f`12 by A11 .= b by A96,MCART_1:85; hence thesis by A96,A97; end; then reconsider C as with_triple-like_morphisms strict Category; take C; thus the carrier of C = A(); hereby let a,b be Element of A(), f be Element of B(); assume P[a,b,f]; then [[a,b],f] in M; hence [[a,b],f] is Morphism of C; end; hereby let m be Morphism of C; m in M; hence ex a,b being Element of A(), f being Element of B() st m = [[a,b],f] & P[a,b,f]; end; let m1,m2 be (Morphism of C), a1,a2,a3 be Element of A(), f1,f2 be Element of B(); assume that A98: m1 = [[a1,a2],f1] and A99: m2 = [[a2,a3],f2]; A100: m1`11 = a1 by A98,MCART_1:85; A101: m1`12 = a2 by A98,MCART_1:85; A102: m2`11 = a2 by A99,MCART_1:85; A103: m2`12 = a3 by A99,MCART_1:85; thus m2(*)m1 = CC.(m2,m1) by CAT_1:def 1,A25,A101,A102 .= [[a1,a3],F(m2`2,m1`2)] by A26,A100,A103,A25,A101,A102 .= [[a1,a3],F(f2,m1`2)] by A99,MCART_1:7 .= [[a1,a3], F(f2,f1)] by A98,MCART_1:7; end; scheme CatUniq { A, B() -> non empty set, P[set, set, set], F(set,set) -> set }: for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = A() & (for a,b being Element of A(), f being Element of B() st P[a,b,f] holds [[a,b],f] is Morphism of C1) & (for m being Morphism of C1 ex a,b being Element of A(), f being Element of B() st m = [[a,b],f] & P[a,b,f]) & (for m1,m2 being (Morphism of C1), a1,a2,a3 being Element of A(), f1,f2 being Element of B() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], F(f2,f1)]) & the carrier of C2 = A() & (for a,b being Element of A(), f being Element of B() st P[a,b,f] holds [[a,b],f] is Morphism of C2) & (for m being Morphism of C2 ex a,b being Element of A(), f being Element of B() st m = [[a,b],f] & P[a,b,f]) & for m1,m2 being (Morphism of C2), a1,a2,a3 being Element of A(), f1,f2 being Element of B() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], F(f2,f1)] holds C1 = C2 provided for a being Element of A() ex f being Element of B() st P[a,a,f] & for b being Element of A(), g being Element of B() holds (P[a,b,g] implies F(g,f) = g) & (P[b,a,g] implies F(f,g) = g) proof let C1, C2 be strict with_triple-like_morphisms Category such that A1: the carrier of C1 = A() and A2: for a,b being Element of A(), f being Element of B() st P[a,b,f] holds [[a,b],f] is Morphism of C1 and A3: for m being Morphism of C1 ex a,b being Element of A(), f being Element of B() st m = [[a,b],f] & P[a,b,f] and A4: for m1,m2 being (Morphism of C1), a1,a2,a3 being Element of A(), f1,f2 being Element of B() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], F(f2,f1)] and A5: the carrier of C2 = A() and A6: for a,b being Element of A(), f being Element of B() st P[a,b,f] holds [[a,b],f] is Morphism of C2 and A7: for m being Morphism of C2 ex a,b being Element of A(), f being Element of B() st m = [[a,b],f] & P[a,b,f] and A8: for m1,m2 being (Morphism of C2), a1,a2,a3 being Element of A(), f1,f2 being Element of B() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], F(f2,f1)]; A9: the carrier' of C1 = the carrier' of C2 proof hereby let x be set; assume x in the carrier' of C1; then ex a,b being Element of A(), f being Element of B() st x = [[a,b],f] & P[a,b,f] by A3; then x is Morphism of C2 by A6; hence x in the carrier' of C2; end; let x be set; assume x in the carrier' of C2; then ex a,b being Element of A(), f being Element of B() st x = [[a,b],f] & P[a,b,f] by A7; then x is Morphism of C1 by A2; hence thesis; end; A10: dom the Source of C1 = the carrier' of C1 by FUNCT_2:def 1; A11: dom the Source of C2 = the carrier' of C2 by FUNCT_2:def 1; A12: dom the Target of C1 = the carrier' of C1 by FUNCT_2:def 1; A13: dom the Target of C2 = the carrier' of C2 by FUNCT_2:def 1; A14: now let x be set; assume x in the carrier' of C1; then reconsider m1 = x as Morphism of C1; reconsider m2 = m1 as Morphism of C2 by A9; thus (the Source of C1).x = dom m1 .= m1`11 by Th2 .= dom m2 by Th2 .= (the Source of C2).x; end; then A15: the Source of C1 = the Source of C2 by A9,A10,A11,FUNCT_1:2; now let x be set; assume x in the carrier' of C1; then reconsider m1 = x as Morphism of C1; reconsider m2 = m1 as Morphism of C2 by A9; thus (the Target of C1).x = cod m1 .= m1`12 by Th2 .= cod m2 by Th2 .= (the Target of C2).x; end; then A16: the Target of C1 = the Target of C2 by A9,A12,A13,FUNCT_1:2; A17: dom the Comp of C1 = dom the Comp of C2 proof hereby let x be set; assume A18: x in dom the Comp of C1; then reconsider xx = x as Element of [:the carrier' of C1, the carrier' of C1:]; reconsider y = xx as Element of [:the carrier' of C2, the carrier' of C2:] by A9; A19: y = [xx`1,xx`2] by MCART_1:21; then dom(xx`1) = cod(xx`2) by A18,CAT_1:def 6; then dom(y`1) = cod(y`2) by A14,A16; hence x in dom the Comp of C2 by A19,CAT_1:def 6; end; let x be set; assume A20: x in dom the Comp of C2; then reconsider xx = x as Element of [:the carrier' of C1, the carrier' of C1:] by A9; reconsider y = xx as Element of [:the carrier' of C2, the carrier' of C2:] by A9; A21: xx = [y`1,y`2] by MCART_1:21; then dom(y`1) = cod(y`2) by A20,CAT_1:def 6; then dom(xx`1) = cod(xx`2) by A14,A16; hence thesis by A21,CAT_1:def 6; end; now let x,y be set; assume A22: [x,y] in dom the Comp of C1; then reconsider g1 = x, h1 = y as Morphism of C1 by ZFMISC_1:87; reconsider g2 = g1, h2 = h1 as Morphism of C2 by A9; consider a1,b1 being Element of A(), f1 being Element of B() such that A23: g1 = [[a1,b1],f1] and P[a1,b1,f1] by A3; consider c1,d1 being Element of A(), i1 being Element of B() such that A24: h1 = [[c1,d1],i1] and P[c1,d1,i1] by A3; A25: a1 = g1`11 by A23,MCART_1:85 .= dom g1 by Th2 .= cod h1 by A22,CAT_1:15 .= h1`12 by Th2 .= d1 by A24,MCART_1:85; thus (the Comp of C1).(x,y) = g1(*)h1 by A22,CAT_1:def 1 .= [[c1,b1],F(f1,i1)] by A4,A23,A24,A25 .= g2(*)h2 by A8,A23,A24,A25 .= (the Comp of C2).(x,y) by A17,A22,CAT_1:def 1; end; hence thesis by A1,A5,A9,A15,A16,A17,BINOP_1:20; end; scheme FunctorEx { A,B() -> Category, O(set) -> Object of B(), F(set) -> set }: ex F being Functor of A(),B() st for f being Morphism of A() holds F.f = F(f) provided A1: for f being Morphism of A() holds F(f) is Morphism of B() & for g being Morphism of B() st g = F(f) holds dom g = O(dom f) & cod g = O(cod f) and A2: for a being Object of A() holds F(id a) = id O(a) and A3: for f1,f2 being Morphism of A() for g1,g2 being Morphism of B() st g1 = F(f1) & g2 = F(f2) & dom f2 = cod f1 holds F(f2(*)f1) = g2(*)g1 proof consider F being Function such that A4: dom F = the carrier' of A() and A5: for x being set st x in the carrier' of A() holds F.x = F(x) from FUNCT_1:sch 3; rng F c= the carrier' of B() proof let x be set; assume x in rng F; then consider y being set such that A6: y in dom F and A7: x = F.y by FUNCT_1:def 3; x = F(y) by A4,A5,A6,A7; then x is Morphism of B() by A1,A4,A6; hence thesis; end; then reconsider F as Function of the carrier' of A(), the carrier' of B() by A4,FUNCT_2:def 1,RELSET_1:4; A8: now let c be Object of A(); take d = O(c); thus F.(id c) = F(id c) by A5 .= id d by A2; end; A9: now let f be Morphism of A(); reconsider g = F(f) as Morphism of B() by A1; thus F.(id dom f) = F(id dom f) by A5 .= id O(dom f) by A2 .= id dom g by A1 .= id dom (F.f) by A5; thus F.(id cod f) = F(id cod f) by A5 .= id O(cod f) by A2 .= id cod g by A1 .= id cod (F.f) by A5; end; now let f,g be Morphism of A(); assume A10: dom g = cod f; A11: F.g = F(g) by A5; A12: F.f = F(f) by A5; F.(g(*)f) = F(g(*)f) by A5; hence F.(g(*)f) = (F.g)(*)(F.f) by A3,A10,A11,A12; end; then reconsider F as Functor of A(), B() by A8,A9,CAT_1:61; take F; thus thesis by A5; end; theorem Th3: for C1 being Category, C2 being Subcategory of C1 st C1 is Subcategory of C2 holds the CatStr of C1 = the CatStr of C2 proof let C1 be Category, C2 be Subcategory of C1; assume A1: C1 is Subcategory of C2; then A2: the carrier of C1 c= the carrier of C2 by CAT_2:def 4; the carrier of C2 c= the carrier of C1 by CAT_2:def 4; then A3: the carrier of C1 = the carrier of C2 by A2,XBOOLE_0:def 10; A4: the carrier' of C1 c= the carrier' of C2 by A1,CAT_2:7; A5: the carrier' of C2 c= the carrier' of C1 by CAT_2:7; then A6: the carrier' of C1 = the carrier' of C2 by A4,XBOOLE_0:def 10; A7: the Comp of C1 c= the Comp of C2 by A1,CAT_2:def 4; the Comp of C2 c= the Comp of C1 by CAT_2:def 4; then A8: the Comp of C1 = the Comp of C2 by A7,XBOOLE_0:def 10; now let m1 be Morphism of C1; reconsider m2 = m1 as Morphism of C2 by A4,A5,XBOOLE_0:def 10; thus (the Source of C1).m1 = dom m1 .= dom m2 by CAT_2:9 .= (the Source of C2).m1; end; then A9: the Source of C1 = the Source of C2 by A3,A6,FUNCT_2:63; now let m1 be Morphism of C1; reconsider m2 = m1 as Morphism of C2 by A4,A5,XBOOLE_0:def 10; thus (the Target of C1).m1 = cod m1 .= cod m2 by CAT_2:9 .= (the Target of C2).m1; end; then the Target of C1 = the Target of C2 by A3,A6,FUNCT_2:63; hence thesis by A3,A6,A8,A9; end; theorem Th4: for C being Category, D being Subcategory of C, E being Subcategory of D holds E is Subcategory of C proof let C be Category, D be Subcategory of C, E be Subcategory of D; A1: the carrier of D c= the carrier of C by CAT_2:def 4; A2: the Comp of D c= the Comp of C by CAT_2:def 4; A3: the carrier of E c= the carrier of D by CAT_2:def 4; A4: the Comp of E c= the Comp of D by CAT_2:def 4; thus the carrier of E c= the carrier of C by A1,A3,XBOOLE_1:1; hereby let a,b be Object of E, a9,b9 be Object of C; reconsider a1 = a, b1 = b as Object of D by CAT_2:6; assume that A5: a = a9 and A6: b = b9; A7: Hom(a,b) c= Hom(a1,b1) by CAT_2:def 4; Hom(a1,b1) c= Hom(a9,b9) by A5,A6,CAT_2:def 4; hence Hom(a,b) c= Hom(a9,b9) by A7,XBOOLE_1:1; end; thus the Comp of E c= the Comp of C by A2,A4,XBOOLE_1:1; let a be Object of E, a9 be Object of C; reconsider a1 = a as Object of D by CAT_2:6; assume A8: a = a9; id a = id a1 by CAT_2:def 4; hence thesis by A8,CAT_2:def 4; end; definition let C1,C2 be Category; given C being Category such that A1: C1 is Subcategory of C and A2: C2 is Subcategory of C; given o1 being Object of C1 such that A3: o1 is Object of C2; func C1 /\ C2 -> strict Category means : Def2: the carrier of it = (the carrier of C1) /\ the carrier of C2 & the carrier' of it = (the carrier' of C1) /\ the carrier' of C2 & the Source of it = (the Source of C1)|the carrier' of C2 & the Target of it = (the Target of C1)|the carrier' of C2 & the Comp of it = (the Comp of C1)||the carrier' of C2; existence proof set DD = (the Source of C1)|the carrier' of C2; set CC = (the Target of C1)|the carrier' of C2; set Cm = (the Comp of C1)||the carrier' of C2; reconsider O = (the carrier of C1) /\ the carrier of C2 as non empty set by A3,XBOOLE_0:def 4; reconsider o2 = o1 as Object of C2 by A3; reconsider o = o1 as Object of C by A1,CAT_2:6; A4: id o1 = id o by A1,CAT_2:def 4; id o2 = id o by A2,CAT_2:def 4; then reconsider M = (the carrier' of C1) /\ the carrier' of C2 as non empty set by A4,XBOOLE_0:def 4; A5: dom the Source of C1 = the carrier' of C1 by FUNCT_2:def 1; A6: dom the Target of C1 = the carrier' of C1 by FUNCT_2:def 1; A7: dom DD = M by A5,RELAT_1:61; A8: dom CC = M by A6,RELAT_1:61; rng DD c= O proof let x be set; assume x in rng DD; then consider m being set such that A9: m in dom DD and A10: x = DD.m by FUNCT_1:def 3; reconsider m1 = m as Morphism of C1 by A9; reconsider m2 = m as Morphism of C2 by A7,A9,XBOOLE_0:def 4; reconsider m = m1 as Morphism of C by A1,CAT_2:8; A11: x = dom m1 by A9,A10,FUNCT_1:47; A12: dom m1 = dom m by A1,CAT_2:9; dom m = dom m2 by A2,CAT_2:9; hence thesis by A11,A12,XBOOLE_0:def 4; end; then reconsider DD as Function of M,O by A7,FUNCT_2:def 1,RELSET_1:4; rng CC c= O proof let x be set; assume x in rng CC; then consider m being set such that A13: m in dom CC and A14: x = CC.m by FUNCT_1:def 3; reconsider m1 = m as Morphism of C1 by A13; reconsider m2 = m as Morphism of C2 by A8,A13,XBOOLE_0:def 4; reconsider m = m1 as Morphism of C by A1,CAT_2:8; A15: x = cod m1 by A13,A14,FUNCT_1:47; A16: cod m1 = cod m by A1,CAT_2:9; cod m = cod m2 by A2,CAT_2:9; hence thesis by A15,A16,XBOOLE_0:def 4; end; then reconsider CC as Function of M,O by A8,FUNCT_2:def 1,RELSET_1:4; A17: dom Cm = (dom the Comp of C1) /\ [:the carrier' of C2,the carrier' of C2:] by RELAT_1:61; then dom Cm c= [:the carrier' of C1,the carrier' of C1:] /\ [:the carrier' of C2,the carrier' of C2:] by XBOOLE_1:26; then A18: dom Cm c= [:M,M:] by ZFMISC_1:100; rng Cm c= M proof let x be set; assume x in rng Cm; then consider m being set such that A19: m in dom Cm and A20: x = Cm.m by FUNCT_1:def 3; A21: m`1 in M by A18,A19,MCART_1:10; A22: m`2 in M by A18,A19,MCART_1:10; A23: m = [m`1,m`2] by A17,A19,MCART_1:21; reconsider m1 = m`1, m2 = m`2 as Morphism of C1 by A21,A22,XBOOLE_0:def 4; reconsider n1 = m`1, n2 = m`2 as Morphism of C2 by A21,A22,XBOOLE_0:def 4; reconsider mm = m1, n = m2 as Morphism of C by A1,CAT_2:8; A24: m in dom the Comp of C1 by A17,A19,XBOOLE_0:def 4; then A25: dom m1 = cod m2 by A23,CAT_1:15; A26: x = (the Comp of C1).(m1,m2) by A19,A20,A23,FUNCT_1:47; A27: dom m1 = dom mm by A1,CAT_2:9; A28: dom n1 = dom mm by A2,CAT_2:9; A29: cod m2 = cod n by A1,CAT_2:9; A30: cod n2 = cod n by A2,CAT_2:9; A31: x = m1(*)m2 by A23,A24,A26,CAT_1:def 1; A32: m1(*)m2 = mm(*)n by A1,A25,CAT_2:11; mm(*)n = n1(*)n2 by A2,A25,A27,A28,A29,A30,CAT_2:11; hence thesis by A31,A32,XBOOLE_0:def 4; end; then reconsider Cm as PartFunc of [:M,M:], M by A18,RELSET_1:4; set CAT = CatStr(#O,M,DD,CC,Cm#); A33: CAT is Category-like proof let f,g be Morphism of CAT; reconsider g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def 4; A34: g in the carrier' of C2 by XBOOLE_0:def 4; A35: f in the carrier' of C2 by XBOOLE_0:def 4; hereby assume [g,f] in dom the Comp of CAT; then A36: [g,f] in dom the Comp of C1 by A17,XBOOLE_0:def 4; thus dom g = dom g9 by A34,FUNCT_1:49 .= cod f9 by A36,CAT_1:def 6 .= cod f by A35,FUNCT_1:49; end; assume A37: dom g = cod f; A38: dom g = dom g9 by A7,FUNCT_1:47; A39: dom g = cod f9 by A8,A37,FUNCT_1:47; A40: [g,f] in [:the carrier' of C2,the carrier' of C2:] by A34,A35, ZFMISC_1:87; [g,f] in dom the Comp of C1 by A38,A39,CAT_1:def 6; hence [g,f] in dom(the Comp of CAT) by A17,A40,XBOOLE_0:def 4; end; A41: for f,g being Morphism of CAT holds [g,f] in dom the Comp of CAT iff dom g = cod f by A33,CAT_1:def 6; A42: CAT is transitive proof let f,g be Morphism of CAT; reconsider g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def 4; assume A43: dom g=cod f; then A44: [g,f] in dom the Comp of CAT by A41; A45: dom the Comp of CAT c= dom the Comp of C1 by RELAT_1:60; reconsider h = g(*)f as Morphism of CAT; reconsider h9 = h as Morphism of C1 by XBOOLE_0:def 4; A46: h = (the Comp of CAT).(g,f) by A44,CAT_1:def 1 .= (the Comp of C1).(g9,f9) by A44,FUNCT_1:47 .= g9(*)f9 by A45,A44,CAT_1:def 1; A47: dom f = dom f9 by A7,FUNCT_1:47; A48: dom g = dom g9 by A7,FUNCT_1:47; A49: dom h = dom h9 by A7,FUNCT_1:47; A50: cod f = cod f9 by A8,FUNCT_1:47; A51: cod g = cod g9 by A8,FUNCT_1:47; A52: cod h = cod h9 by A8,FUNCT_1:47; thus dom(g(*)f) = dom f by A43,A47,A48,A49,A50,A46,CAT_1:def 7; thus cod(g(*)f) = cod g by A43,A46,A48,A50,A51,A52,CAT_1:def 7; end; A53: for f,g being Morphism of CAT st dom g = cod f holds dom(g(*)f) = dom f & cod(g(*)f) = cod g by A42,CAT_1:def 7; A54: CAT is associative proof let f,g,h be Morphism of CAT; reconsider h9 = h, g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def 4; assume that A55: dom h = cod g and A56: dom g = cod f; A57: [h,g] in dom the Comp of CAT by A41,A55; A58: [g,f] in dom the Comp of CAT by A41,A56; then reconsider hg = (the Comp of CAT).(h,g), gf = (the Comp of CAT).(g,f) as Morphism of CAT by A57,PARTFUN1:4; reconsider hg9 = hg, gf9 = gf as Morphism of C1 by XBOOLE_0:def 4; A59: dom hg = dom(h(*)g) by A57,CAT_1:def 1 .= dom g by A53,A55; A60: cod gf = cod(g(*)f) by A58,CAT_1:def 1 .= cod g by A53,A56; A61: [hg,f] in dom the Comp of CAT by A41,A56,A59; A62: [h,gf] in dom the Comp of CAT by A41,A55,A60; A63: dom h9 = dom h by A7,FUNCT_1:47; A64: cod g9 = cod g by A8,FUNCT_1:47; then A65: h9(*)g9 =(the Comp of C1).(h9,g9) by A63,A55,CAT_1:16; A66: dom g9 = dom g by A7,FUNCT_1:47; A67: cod f9 = cod f by A8,FUNCT_1:47; then A68: g9(*)f9 =(the Comp of C1).(g9,f9) by A66,A56,CAT_1:16; A69: cod(g9(*)f9) = cod g9 by A56,A66,A67,CAT_1:def 7; A70: dom(h9(*)g9) = dom g9 by A55,A63,A64,CAT_1:def 7; A71: hg = h(*)g by A57,CAT_1:def 1; gf = g(*)f by A58,CAT_1:def 1; hence h(*)(g(*)f) =(the Comp of CAT).(h,(the Comp of CAT).(g,f)) by A62,CAT_1:def 1 .= (the Comp of C1).[h9,gf9] by A62,FUNCT_1:47 .= (the Comp of C1).(h9,(the Comp of C1).(g9,f9)) by A58,FUNCT_1:47 .= h9(*)(g9(*)f9) by A69,A68,A55,A63,A64,CAT_1:16 .= h9(*)g9(*)f9 by A55,A56,A63,A64,A66,A67,CAT_1:def 8 .= (the Comp of C1).((the Comp of C1).(h9,g9),f9) by A70,A65,A56,A66,A67,CAT_1:16 .= (the Comp of C1).[hg9,f9] by A57,FUNCT_1:47 .= (the Comp of CAT).((the Comp of CAT).(h,g),f) by A61,FUNCT_1:47 .= h(*)g(*)f by A71,A61,CAT_1:def 1; end; A72: CAT is reflexive proof let b be Object of CAT; reconsider b1 = b as Object of C1 by XBOOLE_0:def 4; reconsider b2 = b as Object of C2 by XBOOLE_0:def 4; A73: the carrier of C1 c= the carrier of C by A1,CAT_2:def 4; b1 in the carrier of C1; then reconsider bb = b1 as Object of C by A73; A74: id b1 = id bb by A1,CAT_2:def 4 .= id b2 by A2,CAT_2:def 4; id b2 in (the carrier' of C1) /\ the carrier' of C2 by A74,XBOOLE_0:def 4; then id b2 in M; then reconsider ii = id b2 as Morphism of CAT; A75: dom ii = dom id b1 by A74,FUNCT_1:49 .= b; cod ii = cod id b1 by A74,FUNCT_1:49 .= b; then ii in Hom(b,b) by A75; hence Hom(b,b)<>{}; end; CAT is with_identities proof let a be Element of CAT; reconsider a1 = a as Object of C1 by XBOOLE_0:def 4; reconsider a2 = a as Object of C2 by XBOOLE_0:def 4; A76: the carrier of C1 c= the carrier of C by A1,CAT_2:def 4; a1 in the carrier of C1; then reconsider aa = a1 as Object of C by A76; A77: id a1 = id aa by A1,CAT_2:def 4 .= id a2 by A2,CAT_2:def 4; id a2 in (the carrier' of C1) /\ the carrier' of C2 by A77,XBOOLE_0:def 4; then id a2 in M; then reconsider ii = id a2 as Morphism of CAT; A78: dom ii = dom id a1 by A77,FUNCT_1:49 .= a; cod ii = cod id a1 by A77,FUNCT_1:49 .= a; then ii in Hom(a,a) by A78; then reconsider ii as Morphism of a,a by CAT_1:def 5; take ii; let b be Element of CAT; thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g proof assume A79: Hom(a,b)<>{}; let g be Morphism of a,b; g in the carrier' of C1 by XBOOLE_0:def 4; then reconsider gg = g as Morphism of C1; A80: g in the carrier' of C2 by XBOOLE_0:def 4; A81: dom gg = (the Source of C1).g .= ((the Source of C1)|the carrier' of C2).g by FUNCT_1:49,A80 .= dom g .= a1 by A79,CAT_1:5; A82: cod id a1 = a1; cod ii = cod id a1 by A77,FUNCT_1:49 .= dom g by A79,CAT_1:5; then A83: [g,ii] in dom the Comp of CAT by A33,CAT_1:def 6; hence g(*)ii = Cm.(g,ii) by CAT_1:def 1 .= ((the Comp of C1)||the carrier' of C2).(g,ii) .= ((the Comp of C1)).(gg,id a1) by A77,A83,FUNCT_1:47 .= gg(*)id a1 by A82,A81,CAT_1:16 .= g by A81,CAT_1:22; end; assume A84: Hom(b,a)<>{}; let g be Morphism of b,a; g in the carrier' of C1 by XBOOLE_0:def 4; then reconsider gg = g as Morphism of C1; A85: g in the carrier' of C2 by XBOOLE_0:def 4; A86: cod gg = (the Target of C1).g .= ((the Target of C1)|the carrier' of C2).g by FUNCT_1:49,A85 .= cod g .= a1 by A84,CAT_1:5; A87: dom id a1 = a1; dom ii = dom id a1 by A77,FUNCT_1:49 .= cod g by A84,CAT_1:5; then A88: [ii,g] in dom the Comp of CAT by A33,CAT_1:def 6; hence ii(*)g = Cm.(ii,g) by CAT_1:def 1 .= ((the Comp of C1)||the carrier' of C2).(ii,g) .= ((the Comp of C1)).(id a1,gg) by A77,A88,FUNCT_1:47 .= (id a1)(*)gg by A87,A86,CAT_1:16 .= g by A86,CAT_1:21; end; hence thesis by A33,A42,A54,A72; end; uniqueness; end; reserve C for Category, C1,C2 for Subcategory of C; theorem Th5: the carrier of C1 meets the carrier of C2 implies C1 /\ C2 = C2 /\ C1 proof assume (the carrier of C1) /\ the carrier of C2 <> {}; then reconsider O = (the carrier of C1) /\ the carrier of C2 as non empty set; set o = the Element of O; set C12 = C1 /\ C2, C21 = C2 /\ C1; set M1 = the carrier' of C1, M2 = the carrier' of C2; set O1 = the carrier of C1, O2 = the carrier of C2; A1: o is Object of C1 by XBOOLE_0:def 4; A2: o is Object of C2 by XBOOLE_0:def 4; then A3: the carrier of C12 = O by A1,Def2; A4: the carrier of C21 = O by A1,A2,Def2; A5: the carrier' of C12 = (the carrier' of C1) /\ the carrier' of C2 by A1,A2 ,Def2; A6: the Source of C21 = (the Source of C2)|M1 by A1,A2,Def2; A7: the Source of C12 = (the Source of C1)|M2 by A1,A2,Def2; A8: the Target of C21 = (the Target of C2)|M1 by A1,A2,Def2; A9: the Target of C12 = (the Target of C1)|M2 by A1,A2,Def2; A10: the Comp of C21 = (the Comp of C2)||M1 by A1,A2,Def2; A11: the Comp of C12 = (the Comp of C1)||M2 by A1,A2,Def2; A12: the Source of C1 = (the Source of C)|M1 by NATTRA_1:8; A13: the Target of C1 = (the Target of C)|M1 by NATTRA_1:8; A14: the Source of C2 = (the Source of C)|M2 by NATTRA_1:8; A15: the Target of C2 = (the Target of C)|M2 by NATTRA_1:8; A16: the Source of C12 = (the Source of C)|(M1 /\ M2) by A7,A12,RELAT_1:71 .= the Source of C21 by A6,A14,RELAT_1:71; A17: the Target of C12 = (the Target of C)|(M1 /\ M2) by A9,A13,RELAT_1:71 .= the Target of C21 by A8,A15,RELAT_1:71; the Comp of C12 = (the Comp of C)||M1||M2 by A11,NATTRA_1:8 .= (the Comp of C)|([:M1,M1:] /\ [:M2,M2:]) by RELAT_1:71 .= (the Comp of C)||M2||M1 by RELAT_1:71 .= the Comp of C21 by A10,NATTRA_1:8; hence thesis by A1,A2,A3,A4,A5,A16,A17,Def2; end; theorem Th6: the carrier of C1 meets the carrier of C2 implies C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 proof assume A1: (the carrier of C1) meets the carrier of C2; then A2: (the carrier of C1) /\ the carrier of C2 <> {} by XBOOLE_0:def 7; A3: C1 /\ C2 = C2 /\ C1 by A1,Th5; now let C1,C2 be Subcategory of C; assume A4: (the carrier of C1) /\ the carrier of C2 <> {}; A5: (the carrier of C1) /\ the carrier of C2 c= the carrier of C1 by XBOOLE_1:17; A6: (the carrier' of C1) /\ the carrier' of C2 c= the carrier' of C1 by XBOOLE_1:17; reconsider O = (the carrier of C1) /\ the carrier of C2 as non empty set by A4; set o = the Element of O; A7: o is Object of C1 by XBOOLE_0:def 4; A8: o is Object of C2 by XBOOLE_0:def 4; then A9: the carrier of C1/\C2 = (the carrier of C1) /\ the carrier of C2 by A7,Def2 ; A10: the carrier' of C1/\C2 = (the carrier' of C1) /\ the carrier' of C2 by A7 ,A8,Def2; A11: the Source of C1/\C2 = (the Source of C1)|the carrier' of C2 by A7,A8,Def2 ; A12: the Target of C1/\C2 = (the Target of C1)|the carrier' of C2 by A7,A8,Def2 ; A13: the Comp of C1/\C2 = (the Comp of C1)||the carrier' of C2 by A7,A8,Def2; A14: the Source of C1 = (the Source of C1)|dom the Source of C1; dom the Source of C1 = the carrier' of C1 by FUNCT_2:def 1; then A15: the Source of C1/\C2 = (the Source of C1)|the carrier' of C1/\C2 by A10,A11,A14,RELAT_1:71; A16: the Target of C1 = (the Target of C1)|dom the Target of C1; dom the Target of C1 = the carrier' of C1 by FUNCT_2:def 1; then A17: the Target of C1/\C2 = (the Target of C1)|the carrier' of C1/\C2 by A10,A12,A16,RELAT_1:71; A18: for o being Element of C1 st o in O holds id o in (the carrier' of C1) /\ the carrier' of C2 proof let o1 be Element of C1; assume o1 in O; then reconsider o2 = o1 as Element of C2 by XBOOLE_0:def 4; A19: the carrier of C1 c= the carrier of C by CAT_2:def 4; o1 in the carrier of C1; then reconsider o = o1 as Element of C by A19; A20: id o1 = id o by CAT_2:def 4; id o2 = id o by CAT_2:def 4; hence id o1 in (the carrier' of C1) /\ the carrier' of C2 by A20,XBOOLE_0:def 4; end; the Comp of C1 = (the Comp of C1)||the carrier' of C1; then the Comp of C1/\C2 = (the Comp of C1)| ([:the carrier' of C1,the carrier' of C1:] /\ [:the carrier' of C2,the carrier' of C2:]) by A13,RELAT_1:71; then the Comp of C1/\C2 = (the Comp of C1)||the carrier' of C1/\C2 by A10,ZFMISC_1:100; hence C1/\C2 is Subcategory of C1 by A5,A6,A9,A10,A15,A17,NATTRA_1:9,A18; end; hence thesis by A2,A3; end; definition let C,D be Category; let F be Functor of C,D; func Image F -> strict Subcategory of D means :Def3: the carrier of it = rng Obj F & rng F c= the carrier' of it & for E being Subcategory of D st the carrier of E = rng Obj F & rng F c= the carrier' of E holds it is Subcategory of E; existence proof set a = the Object of C; A1: dom Obj F = the carrier of C by FUNCT_2:def 1; then (Obj F).a in rng Obj F by FUNCT_1:def 3; then reconsider O = rng Obj F as non empty set; reconsider O as non empty Subset of the carrier of D; set f = the Morphism of C; A2: dom F = the carrier' of C by FUNCT_2:def 1; A3: dom the Source of D = the carrier' of D by FUNCT_2:def 1; A4: dom the Target of D = the carrier' of D by FUNCT_2:def 1; defpred P[set] means rng F c= $1 & ex E being Subcategory of D st the carrier of E = O & the carrier' of E = $1; consider MM being set such that A5: for x being set holds x in MM iff x in bool the carrier' of D & P[x] from XBOOLE_0:sch 1; set HH = {Hom(a0,b) where a0 is Object of D, b is Object of D: a0 in O & b in O}; reconsider M0 = union HH as non empty Subset of the carrier' of D by CAT_2:19; reconsider D0 = (the Source of D)|M0, C0 = (the Target of D)|M0 as Function of M0,O by CAT_2:20; reconsider CC = (the Comp of D)||M0 as PartFunc of [:M0,M0:],M0 by CAT_2:20; CatStr(#O,M0,D0,C0,CC#) is full Subcategory of D by CAT_2:21; then A6: CatStr(#O,M0,D0,C0,CC#) is Subcategory of D; rng F c= M0 proof let y be set; assume y in rng F; then consider x being set such that A7: x in dom F and A8: y = F.x by FUNCT_1:def 3; reconsider x as Morphism of C by A7; A9: (Obj F).dom x in O by A1,FUNCT_1:def 3; A10: (Obj F).cod x in O by A1,FUNCT_1:def 3; A11: dom (F.x) in O by A9,CAT_1:69; A12: cod (F.x) in O by A10,CAT_1:69; A13: y in Hom(dom (F.x), cod (F.x)) by A8; Hom(dom (F.x), cod (F.x)) in HH by A11,A12; hence thesis by A13,TARSKI:def 4; end; then A14: M0 in MM by A5,A6; set M = meet MM; A15: for Z being set st Z in MM holds rng F c= Z by A5; now let X be set; assume X in MM; then A16: rng F c= X by A5; F.f in rng F by A2,FUNCT_1:def 3; hence F.f in X by A16; end; then reconsider M as non empty set by A14,SETFAM_1:def 1; M c= the carrier' of D proof let x be set; assume x in M; then x in M0 by A14,SETFAM_1:def 1; hence thesis; end; then reconsider M as non empty Subset of the carrier' of D; set DOM = (the Source of D)|M; set COD = (the Target of D)|M; set COMP = (the Comp of D)||M; A17: dom DOM = M by A3,RELAT_1:62; rng DOM c= O proof let y be set; assume y in rng DOM; then consider x being set such that A18: x in M and A19: y = DOM.x by A17,FUNCT_1:def 3; reconsider x as Morphism of D by A18; x in M0 by A14,A18,SETFAM_1:def 1; then consider X being set such that A20: x in X and A21: X in HH by TARSKI:def 4; consider a,b being Object of D such that A22: X = Hom(a,b) and A23: a in O and b in O by A21; dom x = a by A20,A22,CAT_1:1; hence thesis by A17,A18,A19,A23,FUNCT_1:47; end; then reconsider DOM as Function of M,O by A17,FUNCT_2:def 1,RELSET_1:4; A24: dom COD = M by A4,RELAT_1:62; rng COD c= O proof let y be set; assume y in rng COD; then consider x being set such that A25: x in M and A26: y = COD.x by A24,FUNCT_1:def 3; reconsider x as Morphism of D by A25; x in M0 by A14,A25,SETFAM_1:def 1; then consider X being set such that A27: x in X and A28: X in HH by TARSKI:def 4; consider a,b being Object of D such that A29: X = Hom(a,b) and a in O and A30: b in O by A28; cod x = b by A27,A29,CAT_1:1; hence thesis by A24,A25,A26,A30,FUNCT_1:47; end; then reconsider COD as Function of M,O by A24,FUNCT_2:def 1,RELSET_1:4; A31: dom COMP c= [:M,M:] by RELAT_1:58; rng COMP c= M proof let y be set; assume y in rng COMP; then consider x being set such that A32: x in dom COMP and A33: y = COMP.x by FUNCT_1:def 3; reconsider x1 = x`1, x2 = x`2 as Element of M by A31,A32,MCART_1:10; A34: x = [x1,x2] by A31,A32,MCART_1:21; now let X be set; assume A35: X in MM; then consider E being Subcategory of D such that the carrier of E = O and A36: the carrier' of E = X by A5; reconsider y1 = x1, y2 = x2 as Morphism of E by A35,A36,SETFAM_1:def 1; dom COMP = (dom the Comp of D) /\ [:M,M:] by RELAT_1:61; then x in dom the Comp of D by A32,XBOOLE_0:def 4; then A37: dom x1 = cod x2 by A34,CAT_1:15; A38: dom y1 = dom x1 by CAT_2:9; cod y2 = cod x2 by CAT_2:9; then A39: x in dom the Comp of E by A34,A37,A38,CAT_1:15; the Comp of E c= the Comp of D by CAT_2:def 4; then (the Comp of E).x = (the Comp of D).x by A39,GRFUNC_1:2 .= y by A32,A33,FUNCT_1:47; then y in rng the Comp of E by A39,FUNCT_1:def 3; hence y in X by A36; end; hence thesis by A14,SETFAM_1:def 1; end; then reconsider COMP as PartFunc of [:M,M:], M by A31,RELSET_1:4; for o being Element of D st o in O holds id o in M proof let o be Element of D; assume A40: o in O; for X being set st X in MM holds id o in X proof let X be set; assume X in MM; then P[X] by A5; then consider E being Subcategory of D such that A41: the carrier of E = O and A42: the carrier' of E = X; o in the carrier of E by A40,A41; then reconsider oo=o as Element of E; id oo = id o by CAT_2:def 4; hence id o in X by A42; end; hence id o in M by SETFAM_1:def 1,A14; end; then reconsider T = CatStr(#O,M, DOM, COD, COMP#) as strict Subcategory of D by NATTRA_1:9; take T; thus the carrier of T = rng Obj F & rng F c= the carrier' of T by A14,A15, SETFAM_1:5; let E be Subcategory of D; assume that A43: the carrier of E = rng Obj F and A44: rng F c= the carrier' of E; thus the carrier of T c= the carrier of E by A43; the carrier' of E c= the carrier' of D by CAT_2:7; then the carrier' of E in MM by A5,A43,A44; then A45: M c= the carrier' of E by SETFAM_1:3; hereby let a,b be Object of T, a9,b9 be Object of E; assume that A46: a = a9 and A47: b = b9; thus Hom(a,b) c= Hom(a9,b9) proof let x be set; assume x in Hom(a,b); then consider f being Morphism of T such that A48: x = f and A49: dom f = a and A50: cod f = b; reconsider g = f as Morphism of D by TARSKI:def 3; reconsider f as Morphism of E by A45,TARSKI:def 3; A51: dom g = a by A49,CAT_2:9; A52: cod g = b by A50,CAT_2:9; A53: a9 = dom f by A46,A51,CAT_2:9; b9 = cod f by A47,A52,CAT_2:9; hence thesis by A48,A53; end; end; A54: dom the Comp of T c= dom the Comp of E proof let x be set; assume A55: x in dom the Comp of T; then reconsider x1 = x`1, x2 = x`2 as Element of M by MCART_1:10; reconsider y1 = x1, y2 = x2 as Morphism of T; reconsider z1 = x1, z2 = x2 as Morphism of E by A45,TARSKI:def 3; A56: x = [x1,x2] by A55,MCART_1:21; then A57: dom y1 = cod y2 by A55,CAT_1:15; A58: dom y1 = dom x1 by CAT_2:9; A59: dom z1 = dom x1 by CAT_2:9; A60: cod y2 = cod x2 by CAT_2:9; cod z2 = cod x2 by CAT_2:9; hence thesis by A56,A57,A58,A59,A60,CAT_1:15; end; now let x be set; assume A61: x in dom the Comp of T; A62: the Comp of T c= the Comp of D by CAT_2:def 4; A63: the Comp of E c= the Comp of D by CAT_2:def 4; thus (the Comp of T).x = (the Comp of D).x by A61,A62,GRFUNC_1:2 .= (the Comp of E).x by A54,A61,A63,GRFUNC_1:2; end; hence the Comp of T c= the Comp of E by A54,GRFUNC_1:2; let a be Object of T, a9 be Object of E; reconsider b = a as Object of D by TARSKI:def 3; assume A64: a = a9; id a = id b by CAT_2:def 4; hence thesis by A64,CAT_2:def 4; end; uniqueness proof let C1,C2 be strict Subcategory of D such that A65: the carrier of C1 = rng Obj F and A66: rng F c= the carrier' of C1 and A67: for E being Subcategory of D st the carrier of E = rng Obj F & rng F c= the carrier' of E holds C1 is Subcategory of E and A68: the carrier of C2 = rng Obj F and A69: rng F c= the carrier' of C2 and A70: for E being Subcategory of D st the carrier of E = rng Obj F & rng F c= the carrier' of E holds C2 is Subcategory of E; A71: C1 is Subcategory of C2 by A67,A68,A69; C2 is Subcategory of C1 by A65,A66,A70; hence thesis by A71,Th3; end; end; theorem Th7: for C,D being Category, E be Subcategory of D, F being Functor of C,D st rng F c= the carrier' of E holds F is Functor of C, E proof let C,D be Category, E be Subcategory of D, F be Functor of C,D; assume A1: rng F c= the carrier' of E; A2: dom F = the carrier' of C by FUNCT_2:def 1; A3: dom Obj F = the carrier of C by FUNCT_2:def 1; reconsider G = F as Function of the carrier' of C, the carrier' of E by A1,A2,FUNCT_2:def 1,RELSET_1:4; A4: rng Obj F c= the carrier of E proof let y be set; assume y in rng Obj F; then consider x being set such that A5: x in dom Obj F and A6: y = (Obj F).x by FUNCT_1:def 3; reconsider x as Object of C by A5; F.id x = id ((Obj F).x) by CAT_1:68; then id ((Obj F).x) in rng F by A2,FUNCT_1:def 3; then reconsider f = id ((Obj F).x) as Morphism of E by A1; A7: dom id ((Obj F).x) = y by A6; dom id ((Obj F).x) = dom f by CAT_2:9; hence thesis by A7; end; A8: now let c be Object of C; (Obj F).c in rng Obj F by A3,FUNCT_1:def 3; then reconsider d = (Obj F).c as Object of E by A4; take d; thus G.id c = id ((Obj F).c) by CAT_1:68 .= id d by CAT_2:def 4; end; A9: now let f be Morphism of C; A10: dom (F.f) = dom (G.f) by CAT_2:9; A11: cod (F.f) = cod (G.f) by CAT_2:9; thus G.id dom f = id (F.dom f) by CAT_1:71 .= id dom (F.f) by CAT_1:72 .= id dom (G.f) by A10,CAT_2:def 4; thus G.id cod f = id (F.cod f) by CAT_1:71 .= id cod (F.f) by CAT_1:72 .= id cod (G.f) by A11,CAT_2:def 4; end; now let f,g be Morphism of C; assume A12: dom g = cod f; then A13: F.(g(*)f) = (F.g)(*)(F.f) by CAT_1:64; A14: dom (F.g) = cod (F.f) by A12,CAT_1:64; A15: dom (F.g) = dom (G. g) by CAT_2:9; cod (F.f) = cod (G.f) by CAT_2:9; hence G.(g(*)f) = (G.g)(*)(G.f) by A13,A14,A15,CAT_2:11; end; hence thesis by A8,A9,CAT_1:61; end; theorem for C,D being Category, F being Functor of C,D holds F is Functor of C, Image F proof let C,D be Category, F be Functor of C,D; rng F c= the carrier' of Image F by Def3; hence thesis by Th7; end; theorem Th9: for C,D being Category, E being Subcategory of D, F being Functor of C,E for G being Functor of C,D st F = G holds Image F = Image G proof let C,D be Category, E be Subcategory of D; let F be Functor of C,E, G be Functor of C,D such that A1: F = G; reconsider S = Image F as strict Subcategory of D by Th4; A2: now thus dom Obj F = the carrier of C & dom Obj G = the carrier of C by FUNCT_2:def 1; let x be set; assume x in the carrier of C; then reconsider a = x as Object of C; reconsider b = (Obj F).a as Object of D by CAT_2:6; G.id a = id ((Obj F).a) by A1,CAT_1:68 .= id b by CAT_2:def 4; hence (Obj G).x = (Obj F).x by CAT_1:67; end; then A3: Obj F = Obj G by FUNCT_1:2; then A4: the carrier of S = rng Obj G by Def3; A5: rng G c= the carrier' of S by A1,Def3; now let T be Subcategory of D; assume that A6: the carrier of T = rng Obj G and A7: rng G c= the carrier' of T; set x = the Object of C; A8: (Obj G).x in rng Obj G by A2,FUNCT_1:def 3; A9: (Obj G).x = (Obj F).x by A2; then (Obj G).x in (the carrier of T) /\ the carrier of E by A6,A8,XBOOLE_0:def 4; then A10: (the carrier of T) meets the carrier of E by XBOOLE_0:def 7; then reconsider E1 = T /\ E as Subcategory of E by Th6; the carrier of E1 = (the carrier of T) /\ the carrier of E by A6,A8,A9,Def2 ; then A11: the carrier of E1 = rng Obj F by A3,A6,XBOOLE_1:28; the carrier' of E1 = (the carrier' of T) /\ the carrier' of E by A6,A8,A9 ,Def2; then rng F c= the carrier' of E1 by A1,A7,XBOOLE_1:19; then A12: Image F is Subcategory of E1 by A11,Def3; E1 is Subcategory of T by A10,Th6; hence S is Subcategory of T by A12,Th4; end; hence thesis by A4,A5,Def3; end; begin :: Categorial Categories definition let IT be set; attr IT is categorial means :Def4: for x being set st x in IT holds x is Category; end; definition let X be non empty set; redefine attr X is categorial means : Def5: for x being Element of X holds x is Category; compatibility proof thus X is categorial implies for x being Element of X holds x is Category by Def4; assume A1: for x being Element of X holds x is Category; let x be set; thus thesis by A1; end; end; registration cluster categorial for non empty set; existence proof take X = {1Cat(0,1)}; let x be Element of X; thus thesis by TARSKI:def 1; end; end; definition let X be non empty categorial set; redefine mode Element of X -> Category; coherence by Def4; end; definition let C be Category; attr C is Categorial means :Def6: the carrier of C is categorial & (for a being Object of C, A being Category st a = A holds id a = [[A,A], id A]) & (for m being Morphism of C for A,B being Category st A = dom m & B = cod m ex F being Functor of A,B st m = [[A,B], F]) & for m1,m2 being Morphism of C for A,B,C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2(*)m1 = [[A,C],G*F]; end; registration cluster Categorial -> with_triple-like_morphisms for Category; coherence proof let C be Category; assume A1: C is Categorial; then A2: the carrier of C is categorial by Def6; let f be Morphism of C; reconsider A = dom f, B = cod f as Category by A2,Def5; ex F being Functor of A,B st f = [[A,B], F] by A1,Def6; hence thesis; end; end; theorem Th10: for C,D being Category st the CatStr of C = the CatStr of D holds C is Categorial implies D is Categorial proof let C,D be Category; assume A1: the CatStr of C = the CatStr of D; assume that A2: the carrier of C is categorial and A3: for a being Object of C, A being Category st a = A holds id a = [[A,A], id A] and A4: for m being Morphism of C for A,B being Category st A = dom m & B = cod m ex F being Functor of A,B st m = [[A,B], F] and A5: for m1,m2 being Morphism of C for A,B,C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2(*)m1 = [[A,C],G*F]; thus the carrier of D is categorial by A1,A2; thus for a being Object of D, A being Category st a = A holds id a = [[A,A], id A] proof let a be Object of D, A be Category; reconsider b = a as Object of C by A1; assume a = A; then [[A,A], id A] = id b by A3; hence id a = [[A,A], id A] by A1,Lm1; end; hereby let m be Morphism of D; reconsider m9 = m as Morphism of C by A1; let A,B be Category; assume that A6: A = dom m and A7: B = cod m; A8: A = dom m9 by A1,A6; B = cod m9 by A1,A7; hence ex F being Functor of A,B st m = [[A,B], F] by A4,A8; end; let m1,m2 be Morphism of D; reconsider f1 = m1, f2 = m2 as Morphism of C by A1; let a,b,c be Category; let F be Functor of a,b, G be Functor of b,c; assume that A9: m1 = [[a,b],F] and A10: m2 = [[b,c],G]; reconsider a1 = dom f1, b1 = cod f1, a2 = dom f2, b2 = cod f2 as Category by A2,Def5; A11: ex F1 being Functor of a1,b1 st ( f1 = [[a1,b1], F1]) by A4; ex F2 being Functor of a2,b2 st ( f2 = [[a2,b2], F2]) by A4; then A12: dom f2 = m2`11 by MCART_1:85; A13: m2`11 = b by A10,MCART_1:85; A14: cod f1 = m1`12 by A11,MCART_1:85; m1`12 = b by A9,MCART_1:85; then A15: [f2,f1] in dom the Comp of C by A12,A13,A14,CAT_1:15; hence m2(*)m1 = (the Comp of D).(m2,m1) by A1,CAT_1:def 1 .= f2(*)f1 by A1,A15,CAT_1:def 1 .= [[a,c],G*F] by A5,A9,A10; end; theorem Th11: for C being Category holds 1Cat(C, [[C,C], id C]) is Categorial proof let A be Category; set F = [[A,A], id A]; set C = 1Cat(A, F); thus for x be Object of C holds x is Category by TARSKI:def 1; hereby let a be Object of C, D be Category; assume a = D; then D = A by TARSKI:def 1; hence id a = [[D,D], id D] by TARSKI:def 1; end; hereby let m be Morphism of C; let C1,C2 be Category; assume that A1: C1 = dom m and A2: C2 = cod m; A3: C1 = A by A1,TARSKI:def 1; A4: C2 = A by A2,TARSKI:def 1; reconsider G = id A as Functor of C1,C2 by A2,A3,TARSKI:def 1; take G; thus m = [[C1,C2],G] by A3,A4,TARSKI:def 1; end; let m1,m2 be Morphism of C; let A1,B,C be Category, F1 be Functor of A1,B, F2 be Functor of B,C; assume that A5: m1 = [[A1,B],F1] and A6: m2 = [[B,C],F2]; A7: [[A1,B],F1] = F by A5,TARSKI:def 1; A8: [[B,C],F2] = F by A6,TARSKI:def 1; A9: [A1,B] = [A,A] by A7,XTUPLE_0:1; A10: [A,A] = [B,C] by A8,XTUPLE_0:1; A11: F1 = id A by A7,XTUPLE_0:1; A12: F2 = id A by A8,XTUPLE_0:1; A13: A1 = A by A9,XTUPLE_0:1; A14: C = A by A10,XTUPLE_0:1; F2*F1 = id A by A11,A12,FUNCT_2:17; hence thesis by A13,A14,TARSKI:def 1; end; registration cluster Categorial for strict Category; existence proof set A = 1Cat(0,1); take 1Cat(A, [[A,A], id A]); thus thesis by Th11; end; end; theorem Th12: for C being Categorial Category, a being Object of C holds a is Category proof let C be Categorial Category; the carrier of C is categorial by Def6; hence thesis by Def5; end; theorem Th13: for C being Categorial Category, f being Morphism of C holds dom f = f`11 & cod f = f`12 proof let C be Categorial Category; let f be Morphism of C; reconsider A = dom f, B = cod f as Category by Th12; ex F being Functor of A,B st f = [[A,B], F] by Def6; hence thesis by MCART_1:85; end; definition let C be Categorial Category; let m be Morphism of C; redefine func m`11 -> Category; coherence proof dom m = m`11 by Th13; hence thesis by Th12; end; redefine func m`12 -> Category; coherence proof cod m = m`12 by Th13; hence thesis by Th12; end; end; theorem Th14: for C1, C2 being Categorial Category st the carrier of C1 = the carrier of C2 & the carrier' of C1 = the carrier' of C2 holds the CatStr of C1 = the CatStr of C2 proof let C1, C2 be Categorial Category; assume that A1: the carrier of C1 = the carrier of C2 and A2: the carrier' of C1 = the carrier' of C2; A3: dom the Source of C1 = the carrier' of C1 by FUNCT_2:def 1; A4: dom the Source of C2 = the carrier' of C2 by FUNCT_2:def 1; A5: dom the Target of C1 = the carrier' of C1 by FUNCT_2:def 1; A6: dom the Target of C2 = the carrier' of C2 by FUNCT_2:def 1; now let x be set; assume x in the carrier' of C1; then reconsider m1 = x as Morphism of C1; reconsider m2 = m1 as Morphism of C2 by A2; thus (the Source of C1).x = dom m1 .= m1`11 by Th13 .= dom m2 by Th13 .= (the Source of C2).x; end; then A7: the Source of C1 = the Source of C2 by A2,A3,A4,FUNCT_1:2; A8: now let x be set; assume x in the carrier' of C1; then reconsider m1 = x as Morphism of C1; reconsider m2 = m1 as Morphism of C2 by A2; thus (the Target of C1).x = cod m1 .= m1`12 by Th13 .= cod m2 by Th13 .= (the Target of C2).x; end; then A9: the Target of C1 = the Target of C2 by A2,A5,A6,FUNCT_1:2; A10: dom the Comp of C1 = dom the Comp of C2 proof hereby let x be set; assume A11: x in dom the Comp of C1; then reconsider xx = x as Element of [:the carrier' of C1, the carrier' of C1:]; reconsider y = xx as Element of [:the carrier' of C2, the carrier' of C2:] by A2; A12: y = [xx`1,xx`2] by MCART_1:21; then dom(xx`1) = cod(xx`2) by A11,CAT_1:def 6; then dom(y`1) = cod(y`2) by A8,A7; hence x in dom the Comp of C2 by A12,CAT_1:def 6; end; let x be set; assume A13: x in dom the Comp of C2; then reconsider xx = x as Element of [:the carrier' of C1, the carrier' of C1:] by A2; reconsider y = xx as Element of [:the carrier' of C2, the carrier' of C2:] by A2; A14: xx = [y`1,y`2] by MCART_1:21; then dom(y`1) = cod(y`2) by A13,CAT_1:def 6; then dom(xx`1) = cod(xx`2) by A8,A7; hence thesis by A14,CAT_1:def 6; end; now let x,y be set; assume A15: [x,y] in dom the Comp of C1; then reconsider g1 = x, h1 = y as Morphism of C1 by ZFMISC_1:87; reconsider g2 = g1, h2 = h1 as Morphism of C2 by A2; reconsider a1 = dom g1, b1 = cod g1 as Category by Th12; consider f1 being Functor of a1,b1 such that A16: g1 = [[a1,b1],f1] by Def6; reconsider c1 = dom h1, d1 = cod h1 as Category by Th12; consider i1 being Functor of c1,d1 such that A17: h1 = [[c1,d1],i1] by Def6; A18: a1 = d1 by A15,CAT_1:15; thus (the Comp of C1).(x,y) = g1(*)h1 by A15,CAT_1:def 1 .= [[c1,b1],f1*i1] by A16,A17,A18,Def6 .= g2(*)h2 by A16,A17,A18,Def6 .= (the Comp of C2).(x,y) by A10,A15,CAT_1:def 1; end; then the Comp of C1 = the Comp of C2 by A2,A10,BINOP_1:20; hence thesis by A1,A2,A7,A9; end; registration let C be Categorial Category; cluster -> Categorial for Subcategory of C; coherence proof let D be Subcategory of C; A1: the carrier of C is categorial by Def6; thus the carrier of D is categorial proof let x be Object of D; x is Object of C by CAT_2:6; hence thesis by A1,Def4; end; hereby let a be Object of D, A be Category; reconsider b = a as Object of C by CAT_2:6; assume a = A; then [[A,A], id A] = id b by Def6; hence id a = [[A,A], id A] by CAT_2:def 4; end; hereby let m be Morphism of D; reconsider m9 = m as Morphism of C by CAT_2:8; let a,b be Category; assume that A2: a = dom m and A3: b = cod m; A4: dom m9 = a by A2,CAT_2:9; cod m9 = b by A3,CAT_2:9; hence ex F being Functor of a,b st m = [[a,b], F] by A4,Def6; end; let m1,m2 be Morphism of D; let a,b,c be Category; reconsider m19 = m1, m29 = m2 as Morphism of C by CAT_2:8; let f be Functor of a,b; let g be Functor of b,c; assume that A5: m1 = [[a,b],f] and A6: m2 = [[b,c],g]; A7: dom m2 = dom m29 by CAT_2:9; A8: cod m1 = cod m19 by CAT_2:9; A9: dom m29 = m2`11 by Th13; A10: cod m19 = m1 `12 by Th13; A11: dom m2 = b by A6,A7,A9,MCART_1:85; cod m1 = b by A5,A8,A10,MCART_1:85; hence m2(*)m1 = m29(*)m19 by A11,CAT_2:11 .= [[a,c],g*f] by A5,A6,Def6; end; end; theorem Th15: for C,D being Categorial Category st the carrier' of C c= the carrier' of D holds C is Subcategory of D proof let C,D be Categorial Category; assume A1: the carrier' of C c= the carrier' of D; thus the carrier of C c= the carrier of D proof let x be set; assume x in the carrier of C; then reconsider a = x as Object of C; reconsider i = id a as Morphism of D by A1,TARSKI:def 3; A2: dom i = i`11 by Th13; dom id a = i`11 by Th13; hence thesis by A2; end; hereby let a,b be Object of C, a9,b9 be Object of D; assume that A3: a = a9 and A4: b = b9; thus Hom(a,b) c= Hom(a9,b9) proof let x be set; assume x in Hom(a,b); then consider f being Morphism of C such that A5: x = f and A6: dom f = a and A7: cod f = b; reconsider A = a, B = b as Category by Th12; A8: ex F being Functor of A,B st ( f = [[A,B], F]) by A6,A7,Def6; reconsider f as Morphism of D by A1,TARSKI:def 3; A9: dom f = f`11 by Th13; A10: cod f = f`12 by Th13; A11: f`11 = A by A8,MCART_1:85; f`12 = B by A8,MCART_1:85; hence thesis by A3,A4,A5,A9,A10,A11; end; end; A12: dom the Comp of C c= dom the Comp of D proof let x be set; assume A13: x in dom the Comp of C; then reconsider g = x`1, f = x`2 as Morphism of C by MCART_1:10; reconsider g9 = g, f9 = f as Morphism of D by A1,TARSKI:def 3; A14: x = [g,f] by A13,MCART_1:21; then A15: dom g = cod f by A13,CAT_1:15; A16: dom g = g`11 by Th13; A17: dom g9 = g `11 by Th13; A18: cod f = f`12 by Th13; cod f9 = f`12 by Th13; hence thesis by A14,A15,A16,A17,A18,CAT_1:15; end; now let x be set; assume A19: x in dom the Comp of C; then reconsider g = x`1, f = x`2 as Morphism of C by MCART_1:10; reconsider g9 = g, f9 = f as Morphism of D by A1,TARSKI:def 3; A20: x = [g,f] by A19,MCART_1:21; A21: dom g = g`11 by Th13; cod g = g`12 by Th13; then consider G being Functor of g`11, g`12 such that A22: g = [[g`11,g`12],G] by A21,Def6; A23: dom f = f`11 by Th13; cod f = dom g by A19,A20,CAT_1:15; then consider F being Functor of f`11, g`11 such that A24: f = [[f`11,g`11],F] by A21,A23,Def6; thus (the Comp of C).x = (the Comp of C).(g,f) by A19,MCART_1:21 .= g(*)f by A19,A20,CAT_1:def 1 .= [[f`11,g`12],G*F] by A22,A24,Def6 .= g9(*)f9 by A22,A24,Def6 .= (the Comp of D).(g,f) by A12,A19,A20,CAT_1:def 1 .= (the Comp of D).x by A19,MCART_1:21; end; hence the Comp of C c= the Comp of D by A12,GRFUNC_1:2; let a be Object of C, a9 be Object of D; assume A25: a = a9; reconsider A = a as Category by Th12; thus id a = [[A,A], id A] by Def6 .= id a9 by A25,Def6; end; definition let a be set such that A1: a is Category; func cat a -> Category equals : Def7: a; correctness by A1; end; theorem Th16: for C being Categorial Category, c being Object of C holds cat c = c proof let C be Categorial Category, c be Object of C; the carrier of C is categorial by Def6; then c is Category by Def4; hence thesis by Def7; end; definition let C be Categorial Category; let m be Morphism of C; redefine func m`2 -> Functor of cat dom m, cat cod m; coherence proof the carrier of C is categorial by Def6; then reconsider A = dom m, B = cod m as Category by Def4; consider F being Functor of A, B such that A1: m = [[A,B], F] by Def6; A2: m`2 = F by A1,MCART_1:7; cat A = A by Def7; hence thesis by A2,Def7; end; end; theorem Th17: for X being categorial non empty set, Y being non empty set st (for A,B,C being Element of X for F being Functor of A,B, G being Functor of B,C st F in Y & G in Y holds G*F in Y) & (for A being Element of X holds id A in Y) ex C being strict Categorial Category st the carrier of C = X & for A,B being Element of X, F being Functor of A,B holds [[A,B],F] is Morphism of C iff F in Y proof let X be categorial non empty set, Y be non empty set such that A1: for A,B,C being Element of X for F being Functor of A,B, G being Functor of B,C st F in Y & G in Y holds G*F in Y and A2: for A being Element of X holds id A in Y; set B = {b where b is Element of Y: b is Function}; set a = the Element of X; id a in Y by A2; then id a in B; then reconsider B as non empty set; B is functional proof let x be set; assume x in B; then ex b being Element of Y st x = b & b is Function; hence thesis; end; then reconsider B as non empty functional set; reconsider A = X as non empty categorial set; defpred P[Element of A, Element of A, set] means $3 is Functor of $1, $2; deffunc F(Function,Function) = $1 * $2; A3: for a,b,c being Element of A, f,g being Element of B st P[a,b,f] & P[b,c,g] holds F(g,f) in B & P[a,c,F(g,f)] proof let a,b,c be Element of A, f,g be Element of B; assume that A4: P[a,b,f] and A5: P[b,c,g]; reconsider f as Functor of a,b by A4; reconsider g as Functor of b,c by A5; A6: f in B; A7: g in B; A8: ex b being Element of Y st f = b & b is Function by A6; ex b being Element of Y st g = b & b is Function by A7; then g*f in Y by A1,A8; hence thesis; end; A9: for a being Element of A ex f being Element of B st P[a,a,f] & for b being Element of A, g being Element of B holds (P[a,b,g] implies F(g,f) = g) & (P[b,a,g] implies F(f,g) = g) proof let a be Element of A; reconsider f = id a as Element of Y by A2; f in B; then reconsider f as Element of B; take f; thus P[a,a,f]; let b be Element of A, g be Element of B; thus P[a,b,g] implies g*f = g by FUNCT_2:17; assume P[b,a,g]; then reconsider G = g as Functor of b,a; (id a)*G = G by FUNCT_2:17; hence thesis; end; A10: for a,b,c,d being Element of A, f,g,h being Element of B st P[a,b,f] & P[b,c,g] & P[c,d,h] holds F(h, F(g,f)) = F(F(h,g), f) by RELAT_1:36; consider C being strict with_triple-like_morphisms Category such that A11: the carrier of C = A & (for a,b being Element of A, f being Element of B st P[a,b,f] holds [[a,b],f] is Morphism of C) & (for m being Morphism of C ex a,b being Element of A, f being Element of B st m = [[a,b],f] & P[a,b,f]) & for m1,m2 being (Morphism of C), a1,a2,a3 being Element of A, f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], F(f2,f1)] from CatEx(A3,A9,A10); C is Categorial proof thus the carrier of C is categorial by A11; hereby let a be Object of C, D be Category; assume A12: a = D; then id D in Y by A2,A11; then id D in B; then reconsider f = id D as Element of B; reconsider x = a as Element of A by A11; reconsider F = [[x,x], f] as Morphism of C by A11,A12; consider b,c being Element of A, g being Element of B such that A13: id a = [[b,c],g] and A14: P[b,c,g] by A11; A15: dom id a = (id a)`11 by Th2; A16: (id a)`11 = b by A13,MCART_1:85; cod F = F`12 by Th2 .= x by MCART_1:85; then F = (id a)(*)F by CAT_1:21 .= [[x,c], g*id the carrier' of D] by A11,A13,A15,A16 .= [[x,c], g] by A12,A14,A15,A16,FUNCT_2:17; hence id a = [[D,D], id D] by A12,A13,A15,MCART_1:85; end; hereby let m be Morphism of C; consider a,b being Element of A, f being Element of B such that A17: m = [[a,b],f] and A18: P[a,b,f] by A11; A19: dom m = m`11 by Th2; A20: cod m = m`12 by Th2; A21: dom m = a by A17,A19,MCART_1:85; cod m = b by A17,A20,MCART_1:85; hence for A,B being Category st A = dom m & B = cod m ex F being Functor of A,B st m = [[A,B], F] by A17,A18,A21; end; let m1,m2 be Morphism of C; consider a1,b1 being Element of A, f1 being Element of B such that A22: m1 = [[a1,b1],f1] and P[a1,b1,f1] by A11; consider a2,b2 being Element of A, f2 being Element of B such that A23: m2 = [[a2,b2],f2] and P[a2,b2,f2] by A11; let A,B,C be Category; let F be Functor of A,B; let G be Functor of B,C; assume that A24: m1 = [[A,B],F] and A25: m2 = [[B,C],G]; A26: [A,B] = [a1,b1] by A22,A24,XTUPLE_0:1; A27: [B,C] = [a2,b2] by A23,A25,XTUPLE_0:1; A28: f1 = F by A22,A24,XTUPLE_0:1; A29: f2 = G by A23,A25,XTUPLE_0:1; A30: A = a1 by A26,XTUPLE_0:1; A31: B = b1 by A26,XTUPLE_0:1; C = b2 by A27,XTUPLE_0:1; hence thesis by A11,A22,A25,A28,A29,A30,A31; end; then reconsider C as Categorial strict Category; take C; thus the carrier of C = X by A11; let A9,B9 be Element of X, F be Functor of A9,B9; hereby assume [[A9,B9],F] is Morphism of C; then reconsider m = [[A9,B9],F] as Morphism of C; consider a,b being Element of A, f being Element of B such that A32: m = [[a,b],f] and P[a,b,f] by A11; A33: m`2 = F by MCART_1:7; m`2 = f by A32,MCART_1:7; then F in B by A33; then ex b being Element of Y st F = b & b is Function; hence F in Y; end; assume F in Y; then F in B; hence thesis by A11; end; theorem Th18: for X being categorial non empty set, Y being non empty set for C1, C2 being strict Categorial Category st the carrier of C1 = X & (for A,B being Element of X, F being Functor of A,B holds [[A,B],F] is Morphism of C1 iff F in Y) & the carrier of C2 = X & (for A,B being Element of X, F being Functor of A,B holds [[A,B],F] is Morphism of C2 iff F in Y) holds C1 = C2 proof let X be categorial non empty set, Y be non empty set; let C1, C2 be strict Categorial Category such that A1: the carrier of C1 = X and A2: for A,B being Element of X, F being Functor of A,B holds [[A,B],F] is Morphism of C1 iff F in Y and A3: the carrier of C2 = X and A4: for A,B being Element of X, F being Functor of A,B holds [[A,B],F] is Morphism of C2 iff F in Y; the carrier' of C1 = the carrier' of C2 proof hereby let x be set; assume x in the carrier' of C1; then reconsider m = x as Morphism of C1; reconsider a = dom m, b = cod m as Category by Th12; consider f being Functor of a,b such that A5: m = [[a,b],f] by Def6; f in Y by A1,A2,A5; then x is Morphism of C2 by A1,A4,A5; hence x in the carrier' of C2; end; let x be set; assume x in the carrier' of C2; then reconsider m = x as Morphism of C2; reconsider a = dom m, b = cod m as Category by Th12; consider f being Functor of a,b such that A6: m = [[a,b],f] by Def6; f in Y by A3,A4,A6; then x is Morphism of C1 by A2,A3,A6; hence thesis; end; hence thesis by A1,A3,Th14; end; definition let IT be Categorial Category; attr IT is full means :Def8: for a,b being Category st a is Object of IT & b is Object of IT for F being Functor of a, b holds [[a,b],F] is Morphism of IT; end; registration cluster full for Categorial strict Category; existence proof set A = 1Cat(0,1); reconsider C = 1Cat(A, [[A,A], id A]) as Categorial strict Category by Th11; take C; let a,b be Category; assume that A1: a is Object of C and A2: b is Object of C; let F be Functor of a, b; A3: a = A by A1,TARSKI:def 1; A4: b = A by A2,TARSKI:def 1; then id A = F by A3,FUNCT_2:51; hence thesis by A3,A4,TARSKI:def 1; end; end; theorem for C1,C2 being full Categorial Category st the carrier of C1 = the carrier of C2 holds the CatStr of C1 = the CatStr of C2 proof let C1, C2 be full Categorial Category; assume A1: the carrier of C1 = the carrier of C2; reconsider A = the carrier of C1 as categorial non empty set by Def6; set B = {m`2 where m is Morphism of C1: not contradiction}; set m = the Morphism of C1; m`2 in B; then reconsider B as non empty set; reconsider D1 = the CatStr of C1, D2 = the CatStr of C2 as strict Category by Th1; A2: D1 is Categorial by Th10; A3: D2 is Categorial by Th10; A4: now let a,b be Element of A, F be Functor of a,b; reconsider m = [[a,b], F] as Morphism of C1 by Def8; m`2 = F by MCART_1:7; hence [[a,b],F] is Morphism of the CatStr of C1 iff F in B; end; now let a,b be Element of A, F be Functor of a,b; reconsider a9 = a, b9 = b as Object of C2 by A1; A5: cat a9 = a by Th16; cat b9 = b by Th16; then reconsider m2 = [[a,b], F] as Morphism of C2 by A5,Def8; reconsider m = [[a,b], F] as Morphism of C1 by Def8; A6: m`2 = F by MCART_1:7; m2 = m2; hence [[a,b],F] is Morphism of the CatStr of C2 iff F in B by A6; end; hence thesis by A1,A2,A3,A4,Th18; end; theorem Th20: for A being categorial non empty set ex C being full Categorial strict Category st the carrier of C = A proof let AA be categorial non empty set; set dFF = {Funct(a,b) where a is Element of AA, b is Element of AA: not contradiction}; set a = the Element of AA,f = the Functor of a,a; A1: f in Funct(a,a) by CAT_2:def 2; Funct(a,a) in dFF; then reconsider FF = union dFF as non empty set by A1,TARSKI:def 4; A2: now let A,B,C be Element of AA; let F be Functor of A,B, G be Functor of B,C; assume that F in FF and G in FF; A3: G*F in Funct(A,C) by CAT_2:def 2; Funct(A,C) in dFF; hence G*F in FF by A3,TARSKI:def 4; end; now let A be Element of AA; A4: id A in Funct(A,A) by CAT_2:def 2; Funct(A,A) in dFF; hence id A in FF by A4,TARSKI:def 4; end; then consider C being strict Categorial Category such that A5: the carrier of C = AA and A6: for A,B being Element of AA, F being Functor of A,B holds [[A,B],F] is Morphism of C iff F in FF by A2,Th17; C is full proof let a,b be Category; assume that A7: a is Object of C and A8: b is Object of C; reconsider A = a, B = b as Element of AA by A5,A7,A8; let F be Functor of a, b; A9: F in Funct(A,B) by CAT_2:def 2; Funct(A,B) in dFF; then F in FF by A9,TARSKI:def 4; then [[A,B], F] is Morphism of C by A6; hence thesis; end; hence thesis by A5; end; theorem Th21: for C being Categorial Category, D being full Categorial Category st the carrier of C c= the carrier of D holds C is Subcategory of D proof let C be Categorial Category; let D be full Categorial Category; assume A1: the carrier of C c= the carrier of D; the carrier' of C c= the carrier' of D proof let x be set; assume x in the carrier' of C; then reconsider x as Morphism of C; reconsider y1 = dom x, y2 = cod x as Category by Th12; consider F being Functor of y1,y2 such that A2: x = [[y1,y2], F] by Def6; A3: y1 is Object of D by A1,TARSKI:def 3; y2 is Object of D by A1,TARSKI:def 3; then [[y1,y2], F] is Morphism of D by A3,Def8; hence thesis by A2; end; hence thesis by Th15; end; theorem for C being Category, D1,D2 being Categorial Category for F1 being Functor of C,D1 for F2 being Functor of C,D2 st F1 = F2 holds Image F1 = Image F2 proof let C be Category, D1,D2 be Categorial Category; let F1 be Functor of C,D1; let F2 be Functor of C,D2; assume A1: F1 = F2; reconsider DD = (the carrier of D1) \/ the carrier of D2 as non empty set; DD is categorial proof let d be Element of DD; d is Object of D1 or d is Object of D2 by XBOOLE_0:def 3; hence thesis by Th12; end; then reconsider DD = (the carrier of D1) \/ the carrier of D2 as non empty categorial set; consider D being full Categorial strict Category such that A2: the carrier of D = DD by Th20; reconsider D1, D2 as Subcategory of D by A2,Th21,XBOOLE_1:7; reconsider F1 as Functor of C,D1; reconsider F2 as Functor of C,D2; rng F1 c= the carrier' of D1; then F1 = (incl D1)*F1 by RELAT_1:53; then reconsider G1 = F1 as Functor of C,D; Image F1 = Image G1 by Th9 .= Image F2 by A1,Th9; hence thesis; end; begin :: Slice category definition let C be Category; let o be Object of C; func Hom o -> Subset of the carrier' of C equals (the Target of C)"{o}; coherence; func o Hom -> Subset of the carrier' of C equals (the Source of C)"{o}; coherence; end; registration let C be Category; let o be Object of C; cluster Hom o -> non empty; coherence proof A1: (the Target of C).id o = cod id o .= o; A2: o in {o} by TARSKI:def 1; dom the Target of C = the carrier' of C by FUNCT_2:def 1; hence thesis by A1,A2,FUNCT_1:def 7; end; cluster o Hom -> non empty; coherence proof A3: (the Source of C).id o = dom id o .= o; A4: o in {o} by TARSKI:def 1; dom the Source of C = the carrier' of C by FUNCT_2:def 1; hence thesis by A3,A4,FUNCT_1:def 7; end; end; theorem Th23: for C being Category, a being Object of C, f being Morphism of C holds f in Hom a iff cod f = a proof let C be Category, a be Object of C, f be Morphism of C; cod f in {a} iff cod f = a by TARSKI:def 1; hence thesis by FUNCT_2:38; end; theorem Th24: for C being Category, a being Object of C, f being Morphism of C holds f in a Hom iff dom f = a proof let C be Category, a be Object of C, f be Morphism of C; dom f in {a} iff dom f = a by TARSKI:def 1; hence thesis by FUNCT_2:38; end; theorem for C being Category, a,b being Object of C holds Hom(a,b) = (a Hom) /\ (Hom b) proof let C be Category, a,b be Object of C; hereby let x be set; assume A1: x in Hom(a,b); then reconsider f = x as Morphism of C; A2: dom f = a by A1,CAT_1:1; A3: cod f = b by A1,CAT_1:1; A4: f in a Hom by A2,Th24; f in Hom b by A3,Th23; hence x in (a Hom) /\ (Hom b) by A4,XBOOLE_0:def 4; end; let x be set; assume A5: x in (a Hom) /\ (Hom b); then A6: x in a Hom by XBOOLE_0:def 4; A7: x in Hom b by A5,XBOOLE_0:def 4; reconsider f = x as Morphism of C by A5; A8: dom f = a by A6,Th24; cod f = b by A7,Th23; hence thesis by A8; end; theorem for C being Category, f being Morphism of C holds f in (dom f) Hom & f in Hom (cod f) by Th23,Th24; theorem Th27: for C being Category, f being (Morphism of C), g being Element of Hom dom f holds f(*)g in Hom cod f proof let C be Category, f be (Morphism of C), g be Element of Hom dom f; cod g = dom f by Th23; then cod (f(*)g) = cod f by CAT_1:17; hence thesis by Th23; end; theorem Th28: for C being Category, f being (Morphism of C), g being Element of (cod f) Hom holds g(*)f in (dom f) Hom proof let C be Category, f be (Morphism of C), g be Element of (cod f) Hom; cod f = dom g by Th24; then dom (g(*)f) = dom f by CAT_1:17; hence thesis by Th24; end; definition let C be Category, o be Object of C; set A = Hom o; set B = the carrier' of C; defpred P[Element of A,Element of A,Element of B] means dom $2 = cod $3 & $1 = $2(*)$3; deffunc F((Morphism of C),Morphism of C) = $1(*)$2; A1: for a,b,c being Element of A, f,g being Element of B st P[a,b,f] & P[b,c,g] holds F(g,f) in B & P[a,c,F(g,f)] proof let a,b,c be Element of Hom o, f,g be Morphism of C; assume that A2: dom b = cod f and A3: a = b(*)f and A4: dom c = cod g and A5: b = c(*)g; dom g = cod f by A2,A4,A5,CAT_1:17; hence thesis by A3,A4,A5,CAT_1:17,18; end; A6: for a being Element of A ex f being Element of B st P[a,a,f] & for b being Element of A, g being Element of B holds (P[a,b,g] implies F(g,f) = g) & (P[b,a,g] implies F(f,g) = g) proof let a be Element of Hom o; take f = id dom a; thus dom a = cod f & a = a(*)f by CAT_1:58,22; let b be Element of Hom o, g be Morphism of C; hereby assume that A7: dom b = cod g and A8: a = b(*)g; dom a = dom g by A7,A8,CAT_1:17; hence g(*)f = g by CAT_1:22; end; thus thesis by CAT_1:21; end; A9: for a,b,c,d being Element of A, f,g,h being Element of B st P[a,b,f] & P[b,c,g] & P[c,d,h] holds F(h, F(g,f)) = F(F(h,g), f) proof let a,b,c,d be Element of Hom o, f,g,h be Morphism of C; assume that A10: dom b = cod f and a = b(*)f and A11: dom c = cod g and A12: b = c(*)g and A13: dom d = cod h and A14: c = d(*)h; A15: dom g = cod f by A10,A11,A12,CAT_1:17; dom h = cod g by A11,A13,A14,CAT_1:17; hence thesis by A15,CAT_1:18; end; func C-SliceCat(o) -> strict with_triple-like_morphisms Category means :Def11: the carrier of it = Hom o & (for a,b being Element of Hom o, f being Morphism of C st dom b = cod f & a = b(*)f holds [[a,b],f] is Morphism of it) & (for m being Morphism of it ex a,b being Element of Hom o, f being Morphism of C st m = [[a,b],f] & dom b = cod f & a = b(*)f) & for m1,m2 being (Morphism of it), a1,a2,a3 being Element of Hom o, f1,f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], f2(*)f1]; existence proof thus ex F being with_triple-like_morphisms strict Category st the carrier of F = A & (for a,b being Element of A, f being Element of B st P[a,b,f] holds [[a,b],f] is Morphism of F) & (for m being Morphism of F ex a,b being Element of A, f being Element of B st m = [[a,b],f] & P[a,b,f]) & for m1,m2 being (Morphism of F), a1,a2,a3 being Element of A, f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], F(f2,f1)] from CatEx(A1,A6,A9); end; uniqueness proof thus for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = A & (for a,b being Element of A, f being Element of B st P[a,b,f] holds [[a,b],f] is Morphism of C1) & (for m being Morphism of C1 ex a,b being Element of A, f being Element of B st m = [[a,b],f] & P[a,b,f]) & (for m1,m2 being (Morphism of C1), a1,a2,a3 being Element of A, f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], F(f2,f1)]) & the carrier of C2 = A & (for a,b being Element of A, f being Element of B st P[a,b,f] holds [[a,b],f] is Morphism of C2) & (for m being Morphism of C2 ex a,b being Element of A, f being Element of B st m = [[a,b],f] & P[a,b,f]) & for m1,m2 being (Morphism of C2), a1,a2,a3 being Element of A, f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], F(f2,f1)] holds C1 = C2 from CatUniq(A6); end; set X = o Hom; defpred R[Element of X,Element of X,Element of B] means dom $3 = cod $1 & $2 = $3(*)$1; A16: for a,b,c being Element of X, f,g being Element of B st R[a,b,f] & R[b,c,g] holds F(g,f) in B & R[a,c,F(g,f)] proof let a,b,c be Element of o Hom, f,g be Morphism of C; assume that A17: dom f = cod a and A18: f(*)a = b and A19: dom g = cod b and A20: g(*)b = c; dom g = cod f by A17,A18,A19,CAT_1:17; hence thesis by A17,A18,A20,CAT_1:17,18; end; A21: for a being Element of X ex f being Element of B st R[a,a,f] & for b being Element of X, g being Element of B holds (R[a,b,g] implies F(g,f) = g) & (R[b,a,g] implies F(f,g) = g) proof let a be Element of o Hom; take f = id cod a; thus dom f = cod a & f(*)a = a by CAT_1:58,21; let b be Element of o Hom, g be Morphism of C; thus dom g = cod a & g(*)a = b implies g(*)f = g by CAT_1:22; assume that A22: dom g = cod b and A23: g(*)b = a; cod g = cod a by A22,A23,CAT_1:17; hence thesis by CAT_1:21; end; A24: for a,b,c,d being Element of X, f,g,h being Element of B st R[a,b,f] & R[b,c,g] & R[c,d,h] holds F(h, F(g,f)) = F(F(h,g), f) proof let a,b,c,d be Element of o Hom, f,g,h be Morphism of C; assume that A25: dom f = cod a and A26: f(*)a = b and A27: dom g = cod b and A28: g(*)b = c and A29: dom h = cod c and h(*)c = d; A30: dom g = cod f by A25,A26,A27,CAT_1:17; dom h = cod g by A27,A28,A29,CAT_1:17; hence thesis by A30,CAT_1:18; end; func o-SliceCat(C) -> strict with_triple-like_morphisms Category means : Def12: the carrier of it = o Hom & (for a,b being Element of o Hom, f being Morphism of C st dom f = cod a & f(*)a = b holds [[a,b],f] is Morphism of it) & (for m being Morphism of it ex a,b being Element of o Hom, f being Morphism of C st m = [[a,b],f] & dom f = cod a & f(*)a = b) & for m1,m2 being (Morphism of it), a1,a2,a3 being Element of o Hom, f1,f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], f2(*)f1]; existence proof thus ex F being with_triple-like_morphisms strict Category st the carrier of F = X & (for a,b being Element of X, f being Element of B st R[a,b,f] holds [[a,b],f] is Morphism of F) & (for m being Morphism of F ex a,b being Element of X, f being Element of B st m = [[a,b],f] & R[a,b,f]) & for m1,m2 being (Morphism of F), a1,a2,a3 being Element of X, f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], F(f2,f1)] from CatEx(A16,A21,A24); end; uniqueness proof thus for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = X & (for a,b being Element of X, f being Element of B st R[a,b,f] holds [[a,b],f] is Morphism of C1) & (for m being Morphism of C1 ex a,b being Element of X, f being Element of B st m = [[a,b],f] & R[a,b,f]) & (for m1,m2 being (Morphism of C1), a1,a2,a3 being Element of X, f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], F(f2,f1)]) & the carrier of C2 = X & (for a,b being Element of X, f being Element of B st R[a,b,f] holds [[a,b],f] is Morphism of C2) & (for m being Morphism of C2 ex a,b being Element of X, f being Element of B st m = [[a,b],f] & R[a,b,f]) & for m1,m2 being (Morphism of C2), a1,a2,a3 being Element of X, f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], F(f2,f1)] holds C1 = C2 from CatUniq(A21); end; end; definition let C be Category; let o be Object of C; let m be Morphism of C-SliceCat(o); redefine func m`2 -> Morphism of C; coherence proof ex a,b being Element of Hom o, f being Morphism of C st ( m = [[a,b],f])&( dom b = cod f)&( a = b(*)f) by Def11; hence thesis by MCART_1:7; end; redefine func m`11 -> Element of Hom o; coherence proof ex a,b being Element of Hom o, f being Morphism of C st ( m = [[a,b],f])&( dom b = cod f)&( a = b(*)f) by Def11; hence thesis by MCART_1:85; end; redefine func m`12 -> Element of Hom o; coherence proof ex a,b being Element of Hom o, f being Morphism of C st ( m = [[a,b],f])&( dom b = cod f)&( a = b(*)f) by Def11; hence thesis by MCART_1:85; end; end; theorem Th29: for C being Category, a being Object of C, m being Morphism of C-SliceCat a holds m = [[m`11,m`12],m`2] & dom m`12 = cod m`2 & m`11 = m`12(*)m`2 & dom m = m`11 & cod m = m`12 proof let C be Category, o be Object of C, m be Morphism of C-SliceCat o; consider a,b being Element of Hom o, f being Morphism of C such that A1: m = [[a,b],f] and A2: dom b = cod f and A3: a = b(*)f by Def11; A4: m`11 = a by A1,MCART_1:85; m`12 = b by A1,MCART_1:85; hence thesis by A1,A2,A3,A4,Th2,MCART_1:7; end; theorem Th30: for C being Category, o being Object of C, f being Element of Hom o for a being Object of C-SliceCat o st a = f holds id a = [[a,a], id dom f] proof let C be Category, o be Object of C, f be Element of Hom o; let a be Object of C-SliceCat o; assume A1: a = f; consider b,c being Element of Hom o, g being Morphism of C such that A2: id a = [[b,c], g] and A3: dom c = cod g and b = c(*)g by Def11; A4: cod id dom f = dom f; f = f(*)id dom f by CAT_1:22; then reconsider h = [[f,f], id dom f] as Morphism of C-SliceCat o by A4,Def11 ; A5: (id a)`11 = b by A2,MCART_1:85; A6: (id a)`12 = c by A2,MCART_1:85; A7: dom id a = b by A5,Th2; A8: cod id a = c by A6,Th2; A9: b = a by A7; A10: c = a by A8; dom h = h`11 by Th2 .= a by A1,MCART_1:85; then h = h(*)id a by CAT_1:22 .= [[f,f], (id dom f)(*)g] by A1,A2,A9,A10,Def11 .= [[f,f], g] by A1,A3,A10,CAT_1:21; hence thesis by A1,A2,A7,A10; end; definition let C be Category; let o be Object of C; let m be Morphism of o-SliceCat(C); redefine func m`2 -> Morphism of C; coherence proof ex a,b being Element of o Hom, f being Morphism of C st ( m = [[a,b],f])&( dom f = cod a)&( f(*)a = b) by Def12; hence thesis by MCART_1:7; end; redefine func m`11 -> Element of o Hom; coherence proof ex a,b being Element of o Hom, f being Morphism of C st ( m = [[a,b],f])&( dom f = cod a)&( f(*)a = b) by Def12; hence thesis by MCART_1:85; end; redefine func m`12 -> Element of o Hom; coherence proof ex a,b being Element of o Hom, f being Morphism of C st ( m = [[a,b],f])&( dom f = cod a)&( f(*)a = b) by Def12; hence thesis by MCART_1:85; end; end; theorem Th31: for C being Category, a being Object of C, m being Morphism of a-SliceCat C holds m = [[m`11,m`12],m`2] & dom m`2 = cod m`11 & m`2(*)m`11 = m`12 & dom m = m`11 & cod m = m`12 proof let C be Category, o be Object of C, m be Morphism of o-SliceCat C; consider a,b being Element of o Hom, f being Morphism of C such that A1: m = [[a,b],f] and A2: dom f = cod a and A3: f(*)a = b by Def12; A4: m`11 = a by A1,MCART_1:85; m`12 = b by A1,MCART_1:85; hence thesis by A1,A2,A3,A4,Th2,MCART_1:7; end; theorem Th32: for C being Category, o being Object of C, f being Element of o Hom for a being Object of o-SliceCat C st a = f holds id a = [[a,a], id cod f] proof let C be Category, o be Object of C, f be Element of o Hom; let a be Object of o-SliceCat C; assume A1: a = f; consider b,c being Element of o Hom, g being Morphism of C such that A2: id a = [[b,c], g] and A3: dom g = cod b and g(*)b = c by Def12; A4: dom id cod f = cod f; f = (id cod f)(*)f by CAT_1:21; then reconsider h = [[f,f], id cod f] as Morphism of o-SliceCat C by A4,Def12 ; A5: (id a)`11 = b by A2,MCART_1:85; A6: (id a)`12 = c by A2,MCART_1:85; A7: dom id a = b by A5,Th2; A8: cod id a = c by A6,Th2; A9: b = a by A7; A10: c = a by A8; cod h = h`12 by Th2 .= a by A1,MCART_1:85; then h = (id a)(*)h by CAT_1:21 .= [[f,f], g(*)id cod f] by A1,A2,A9,A10,Def12 .= [[f,f], g] by A1,A3,A9,CAT_1:22; hence thesis by A1,A2,A8,A9; end; begin :: Functors Between Slice Categories definition let C be Category, f be Morphism of C; func SliceFunctor f -> Functor of C-SliceCat dom f, C-SliceCat cod f means : Def13: for m being Morphism of C-SliceCat dom f holds it.m = [[f(*)m`11, f(*)m`12], m`2]; existence proof set C1 = C-SliceCat dom f, C2 = C-SliceCat cod f; deffunc f(Morphism of C1) = [[f(*)$1`11, f(*)$1`12], $1`2]; consider F being Function of the carrier' of C1, the carrier' of [:[:C,C:],C:] such that A1: for m being Morphism of C1 holds F.m = f(m) from FUNCT_2:sch 4; A2: dom F = the carrier' of C1 by FUNCT_2:def 1; rng F c= the carrier' of C2 proof let x be set; assume x in rng F; then consider m being set such that A3: m in dom F and A4: x = F.m by FUNCT_1:def 3; reconsider m as Morphism of C1 by A3; A5: x = [[f(*)m`11, f(*)m`12], m`2] by A1,A4; A6: dom m`12 = cod m`2 by Th29; A7: m`11 = m`12(*)m`2 by Th29; A8: cod m`12 = dom f by Th23; A9: f(*)m`11 in Hom cod f by Th27; A10: f(*)m`12 in Hom cod f by Th27; A11: dom (f(*)m`12) = cod m`2 by A6,A8,CAT_1:17; f(*)m`11 = f(*)m`12(*)m`2 by A6,A7,A8,CAT_1:18; then x is Morphism of C2 by A5,A9,A10,A11,Def11; hence thesis; end; then reconsider F as Function of the carrier' of C1, the carrier' of C2 by A2,FUNCT_2:def 1,RELSET_1:4; A12: now let c be Object of C1; reconsider g = c as Element of Hom dom f by Def11; reconsider h = f(*)g as Element of Hom cod f by Th27; reconsider d = h as Object of C2 by Def11; take d; A13: id c = [[c,c], id dom g] by Th30; A14: id d = [[d,d], id dom h] by Th30; A15: (id c)`11 = c by A13,MCART_1:85; A16: (id c)`12 = c by A13,MCART_1:85; A17: (id c)`2 = id dom g by A13,MCART_1:7; A18: cod g = dom f by Th23; thus F.(id c) = [[h, h], (id c)`2] by A1,A15,A16 .= id d by A14,A17,A18,CAT_1:17; end; A19: now let m be Morphism of C1; reconsider g1 = f(*)m`11, g2 = f(*)m`12 as Element of Hom cod f by Th27; A20: dom f = cod m`11 by Th23; A21: dom f = cod m`12 by Th23; F.m = [[g1,g2], m`2] by A1; then dom (F.m) = [[g1,g2], m`2]`11 by Th29 .= g1 by MCART_1:85; then A22: id dom (F.m) = [[g1,g1], id dom g1] by Th30; dom m = m`11 by Th29; then A23: id dom m = [[m`11,m`11], id dom m`11] by Th30; then A24: (id dom m)`11 = m`11 by MCART_1:85; A25: (id dom m)`12 = m`11 by A23,MCART_1:85; (id dom m)`2 = id dom m`11 by A23,MCART_1:7; hence F.(id dom m) = [[g1,g1], id dom m`11] by A1,A24,A25 .= id dom (F.m) by A20,A22,CAT_1:17; F.m = [[g1,g2], m`2] by A1; then cod (F.m) = [[g1,g2], m`2]`12 by Th29 .= g2 by MCART_1:85; then A26: id cod (F.m) = [[g2,g2], id dom g2] by Th30; cod m = m`12 by Th29; then A27: id cod m = [[m`12,m`12], id dom m`12] by Th30; then A28: (id cod m)`11 = m`12 by MCART_1:85; A29: (id cod m)`12 = m`12 by A27,MCART_1:85; (id cod m)`2 = id dom m`12 by A27,MCART_1:7; hence F.(id cod m) = [[g2,g2], id dom m`12] by A1,A28,A29 .= id cod (F.m) by A21,A26,CAT_1:17; end; now let f1,f2 be Morphism of C1; consider a1,b1 being Element of Hom dom f, g1 being Morphism of C such that A30: f1 = [[a1,b1], g1] and dom b1 = cod g1 and a1 = b1(*)g1 by Def11; consider a2,b2 being Element of Hom dom f, g2 being Morphism of C such that A31: f2 = [[a2,b2], g2] and dom b2 = cod g2 and a2 = b2(*)g2 by Def11; A32: dom f2 = f2`11 by Th2; A33: cod f1 = f1`12 by Th2; A34: dom f2 = a2 by A31,A32,MCART_1:85; A35: cod f1 = b1 by A30,A33,MCART_1:85; reconsider ha1 = f(*)a1, ha2 = f(*)a2, hb1 = f(*)b1, hb2 = f(*)b2 as Element of Hom cod f by Th27; A36: f1`11 = a1 by A30,MCART_1:85; A37: f1`12 = b1 by A30,MCART_1:85; A38: f1`2 = g1 by A30,MCART_1:7; A39: f2`11 = a2 by A31,MCART_1:85; A40: f2`12 = b2 by A31,MCART_1:85; A41: f2`2 = g2 by A31,MCART_1:7; A42: F.f1 = [[ha1, hb1], g1] by A1,A36,A37,A38; A43: F.f2 = [[ha2, hb2], g2] by A1,A39,A40,A41; assume A44: dom f2 = cod f1; then A45: f2(*)f1 = [[a1,b2], g2(*)g1] by A30,A31,A34,A35,Def11; A46: (F.f2)(*)(F.f1) = [[ha1,hb2], g2(*)g1] by A34,A35,A42,A43,A44,Def11; A47: (f2(*)f1)`11 = a1 by A45,MCART_1:85; A48: (f2(*)f1)`12 = b2 by A45,MCART_1:85; (f2(*)f1)`2 = g2(*)g1 by A45,MCART_1:7; hence F.(f2(*)f1) = (F.f2)(*)(F.f1) by A1,A46,A47,A48; end; then reconsider F as Functor of C1, C2 by A12,A19,CAT_1:61; take F; thus thesis by A1; end; uniqueness proof let F1,F2 be Functor of C-SliceCat dom f, C-SliceCat cod f such that A49: for m being Morphism of C-SliceCat dom f holds F1.m = [[f(*)m`11, f(*)m`12], m`2] and A50: for m being Morphism of C-SliceCat dom f holds F2.m = [[f(*)m`11, f(*)m`12], m`2]; now let m be Morphism of C-SliceCat dom f; thus F1.m = [[f(*)m`11, f(*)m`12], m`2] by A49 .= F2.m by A50; end; hence thesis by FUNCT_2:63; end; func SliceContraFunctor f -> Functor of (cod f)-SliceCat C, (dom f)-SliceCat C means : Def14: for m being Morphism of (cod f)-SliceCat C holds it.m = [[m`11(*)f, m`12(*)f], m`2]; existence proof set C1 = (cod f)-SliceCat C, C2 = (dom f)-SliceCat C; deffunc f(Morphism of C1) = [[$1`11(*)f, $1`12(*)f], $1`2]; consider F being Function of the carrier' of C1, the carrier' of [:[:C,C:],C:] such that A51: for m being Morphism of C1 holds F.m = f(m) from FUNCT_2:sch 4; A52: dom F = the carrier' of C1 by FUNCT_2:def 1; rng F c= the carrier' of C2 proof let x be set; assume x in rng F; then consider m being set such that A53: m in dom F and A54: x = F.m by FUNCT_1:def 3; reconsider m as Morphism of C1 by A53; A55: x = [[m`11(*)f, m`12(*)f], m`2] by A51,A54; A56: dom m`2 = cod m`11 by Th31; A57: m`12 = m`2(*)m`11 by Th31; A58: dom m`11 = cod f by Th24; A59: m`11(*)f in (dom f)Hom by Th28; A60: m`12(*)f in (dom f)Hom by Th28; A61: cod (m`11(*)f) = dom m`2 by A56,A58,CAT_1:17; m`12(*)f = m`2(*)(m`11(*)f) by A56,A57,A58,CAT_1:18; then x is Morphism of C2 by A55,A59,A60,A61,Def12; hence thesis; end; then reconsider F as Function of the carrier' of C1, the carrier' of C2 by A52,FUNCT_2:def 1,RELSET_1:4; A62: now let c be Object of C1; reconsider g = c as Element of (cod f) Hom by Def12; reconsider h = g(*)f as Element of (dom f) Hom by Th28; reconsider d = h as Object of C2 by Def12; take d; A63: id c = [[c,c], id cod g] by Th32; A64: id d = [[d,d], id cod h] by Th32; A65: (id c)`11 = c by A63,MCART_1:85; A66: (id c)`12 = c by A63,MCART_1:85; A67: (id c)`2 = id cod g by A63,MCART_1:7; A68: dom g = cod f by Th24; thus F.(id c) = [[h, h], (id c)`2] by A51,A65,A66 .= id d by A64,A67,A68,CAT_1:17; end; A69: now let m be Morphism of C1; reconsider g1 = m`11(*)f, g2 = m`12(*)f as Element of (dom f) Hom by Th28; A70: cod f = dom m`11 by Th24; A71: cod f = dom m`12 by Th24; F.m = [[g1,g2], m`2] by A51; then dom (F.m) = [[g1,g2], m`2]`11 by Th31 .= g1 by MCART_1:85; then A72: id dom (F.m) = [[g1,g1], id cod g1] by Th32; dom m = m`11 by Th31; then A73: id dom m = [[m`11,m`11], id cod m`11] by Th32; then A74: (id dom m)`11 = m`11 by MCART_1:85; A75: (id dom m)`12 = m`11 by A73,MCART_1:85; (id dom m)`2 = id cod m`11 by A73,MCART_1:7; hence F.(id dom m) = [[g1,g1], id cod m`11] by A51,A74,A75 .= id dom (F.m) by A70,A72,CAT_1:17; F.m = [[g1,g2], m`2] by A51; then cod (F.m) = [[g1,g2], m`2]`12 by Th31 .= g2 by MCART_1:85; then A76: id cod (F.m) = [[g2,g2], id cod g2] by Th32; cod m = m`12 by Th31; then A77: id cod m = [[m`12,m`12], id cod m`12] by Th32; then A78: (id cod m)`11 = m`12 by MCART_1:85; A79: (id cod m)`12 = m`12 by A77,MCART_1:85; (id cod m)`2 = id cod m`12 by A77,MCART_1:7; hence F.(id cod m) = [[g2,g2], id cod m`12] by A51,A78,A79 .= id cod (F.m) by A71,A76,CAT_1:17; end; now let f1,f2 be Morphism of C1; consider a1,b1 being Element of (cod f) Hom, g1 being Morphism of C such that A80: f1 = [[a1,b1], g1] and dom g1 = cod a1 and g1(*)a1 = b1 by Def12; consider a2,b2 being Element of (cod f) Hom, g2 being Morphism of C such that A81: f2 = [[a2,b2], g2] and dom g2 = cod a2 and g2(*)a2 = b2 by Def12; A82: dom f2 = f2`11 by Th2; A83: cod f1 = f1`12 by Th2; A84: dom f2 = a2 by A81,A82,MCART_1:85; A85: cod f1 = b1 by A80,A83,MCART_1:85; reconsider ha1 = a1(*)f, ha2 = a2(*)f, hb1 = b1(*)f, hb2 = b2(*)f as Element of (dom f) Hom by Th28; A86: f1`11 = a1 by A80,MCART_1:85; A87: f1`12 = b1 by A80,MCART_1:85; A88: f1`2 = g1 by A80,MCART_1:7; A89: f2`11 = a2 by A81,MCART_1:85; A90: f2`12 = b2 by A81,MCART_1:85; A91: f2`2 = g2 by A81,MCART_1:7; A92: F.f1 = [[ha1, hb1], g1] by A51,A86,A87,A88; A93: F.f2 = [[ha2, hb2], g2] by A51,A89,A90,A91; assume A94: dom f2 = cod f1; then A95: f2(*)f1 = [[a1,b2], g2(*)g1] by A80,A81,A84,A85,Def12; A96: (F.f2)(*)(F.f1) = [[ha1,hb2], g2(*)g1] by A84,A85,A92,A93,A94,Def12; A97: (f2(*)f1)`11 = a1 by A95,MCART_1:85; A98: (f2(*)f1)`12 = b2 by A95,MCART_1:85; (f2(*)f1)`2 = g2(*)g1 by A95,MCART_1:7; hence F.(f2(*)f1) = (F.f2)(*)(F.f1) by A51,A96,A97,A98; end; then reconsider F as Functor of C1, C2 by A62,A69,CAT_1:61; take F; thus thesis by A51; end; uniqueness proof let F1,F2 be Functor of (cod f)-SliceCat C, (dom f)-SliceCat C such that A99: for m being Morphism of (cod f)-SliceCat C holds F1.m = [[m`11(*)f, m`12(*)f], m`2] and A100: for m being Morphism of (cod f)-SliceCat C holds F2.m = [[m`11(*)f, m`12(*)f], m`2]; now let m be Morphism of (cod f)-SliceCat C; thus F1.m = [[m`11(*)f, m`12(*)f], m`2] by A99 .= F2.m by A100; end; hence thesis by FUNCT_2:63; end; end; theorem for C being Category, f,g being Morphism of C st dom g = cod f holds SliceFunctor (g(*)f) = (SliceFunctor g)*(SliceFunctor f) proof let C be Category, f,g be Morphism of C; assume A1: dom g = cod f; then A2: dom (g(*)f) = dom f by CAT_1:17; set A1 = C-SliceCat dom f, A3 = C-SliceCat cod g; set F = SliceFunctor f; reconsider G = SliceFunctor g as Functor of C-SliceCat cod f,A3 by A1; reconsider GF = SliceFunctor (g(*)f) as Functor of A1,A3 by A1,A2,CAT_1:17; now let m be Morphism of A1; A3: F.m = [[f(*)m`11, f(*)m`12], m`2] by Def13; then A4: (F.m)`11 = f(*)m`11 by MCART_1:85; A5: (F.m)`12 = f(*)m`12 by A3,MCART_1:85; A6: (F.m)`2 = m`2 by A3,MCART_1:7; A7: dom f = cod m`11 by Th23; A8: dom f = cod m`12 by Th23; A9: g(*)(f(*)m`11) = g(*)f(*)m`11 by A1,A7,CAT_1:18; A10: g(*)(f(*)m`12) = g(*)f(*)m`12 by A1,A8,CAT_1:18; thus (G*F).m = G.(F.m) by FUNCT_2:15 .= [[g(*)(f(*)m`11), g(*)(f(*)m`12)], m`2] by A1,A4,A5,A6,Def13 .= GF.m by A2,A9,A10,Def13; end; hence thesis by FUNCT_2:63; end; theorem for C being Category, f,g being Morphism of C st dom g = cod f holds SliceContraFunctor (g(*)f) = (SliceContraFunctor f)*(SliceContraFunctor g) proof let C be Category, f,g be Morphism of C; assume A1: dom g = cod f; then A2: cod (g(*)f) = cod g by CAT_1:17; set A1 = (dom f)-SliceCat C, A2 = (cod f)-SliceCat C; set A3 = (cod g)-SliceCat C; reconsider F=SliceContraFunctor f as Functor of A2,A1; reconsider G = SliceContraFunctor g as Functor of A3,A2 by A1; reconsider FG = SliceContraFunctor (g(*)f) as Functor of A3,A1 by A1,A2, CAT_1:17; now let m be Morphism of A3; A3: G.m = [[m`11(*)g, m`12(*)g], m`2] by Def14; then A4: (G.m)`11 = m`11(*)g by MCART_1:85; A5: (G.m)`12 = m`12(*)g by A3,MCART_1:85; A6: (G.m)`2 = m`2 by A3,MCART_1:7; A7: cod g = dom m`11 by Th24; A8: cod g = dom m`12 by Th24; A9: m`11(*)(g(*)f) = m`11(*)g(*)f by A1,A7,CAT_1:18; A10: m`12(*)(g(*)f) = m`12(*)g(*)f by A1,A8,CAT_1:18; thus (F*G).m = F.(G.m) by FUNCT_2:15 .= [[m`11(*)g(*)f, m`12(*)g(*)f], m`2] by A4,A5,A6,Def14 .= FG.m by A2,A9,A10,Def14; end; hence thesis by FUNCT_2:63; end;