:: Subcategories and Products of Categories :: by Czes{\l}aw Byli\'nski :: :: Received May 31, 1990 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, SUBSET_1, FUNCT_2, FUNCT_1, ZFMISC_1, FUNCT_5, RELAT_1, TARSKI, CAT_1, FUNCOP_1, STRUCT_0, GRAPH_1, FUNCT_3, REALSET1, PARTFUN1, FUNCT_4, MCART_1, CAT_2, MONOID_0, RELAT_2, BINOP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, PARTFUN1, FUNCT_3, FUNCT_4, FUNCT_5, REALSET1, FUNCOP_1, STRUCT_0, GRAPH_1, CAT_1; constructors PARTFUN1, BINOP_1, FUNCT_3, FUNCT_4, FUNCT_5, REALSET1, CAT_1, FUNCOP_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, CAT_1, STRUCT_0, RELAT_1, XTUPLE_0; requirements SUBSET, BOOLE; definitions TARSKI, CAT_1; equalities CAT_1, REALSET1, FUNCOP_1, BINOP_1, GRAPH_1; expansions CAT_1; theorems TARSKI, ZFMISC_1, MCART_1, DOMAIN_1, FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_4, FUNCT_5, PARTFUN1, FUNCOP_1, CAT_1, GRFUNC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XTUPLE_0; schemes XBOOLE_0, BINOP_1; begin ::$CT 4 reserve B,C,D,C9,D9 for Category; :: Auxiliary theorems on Functors definition let B,C; let c be Object of C; func B --> c -> Functor of B,C equals (the carrier' of B) --> (id c); coherence proof reconsider T = (the carrier' of B) --> id c as Function of the carrier' of B,the carrier' of C; now thus for b being Object of B ex d being Object of C st T.(id b) = id d by FUNCOP_1:7; thus for f being Morphism of B holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f) proof let f be Morphism of B; T.(id cod f) = id c by FUNCOP_1:7; then A1: T.(id cod f) = id cod id c; T.(id dom f) = id c by FUNCOP_1:7; then T.(id dom f) = id dom id c; hence thesis by A1,FUNCOP_1:7; end; let f,g be Morphism of B such that dom g = cod f; Hom(c,c) <> {}; then A2: T.f = id c & (id c)*(id c) = (id c)(*)((id c)) by CAT_1:def 13,FUNCOP_1:7 ; T.(g(*)f) = id c & T.g = id c by FUNCOP_1:7; hence T.(g(*)f) = (T.g)(*)(T.f) by A2; end; hence thesis by CAT_1:61; end; end; theorem for c being Object of C, b being Object of B holds (Obj (B --> c)).b = c proof let c be Object of C, b be Object of B; (B --> c).(id b) = id c by FUNCOP_1:7; hence thesis by CAT_1:67; end; definition let C,D; func Funct(C,D) -> set means :Def2: for x being set holds x in it iff x is Functor of C,D; existence proof defpred P[object] means $1 is Functor of C,D; consider F being set such that A1: for x being object holds x in F iff x in Funcs(the carrier' of C,the carrier' of D) & P[x] from XBOOLE_0:sch 1; take F; let x be set; thus x in F implies x is Functor of C,D by A1; assume A2: x is Functor of C,D; then x in Funcs(the carrier' of C,the carrier' of D) by FUNCT_2:8; hence thesis by A1,A2; end; uniqueness proof let F1,F2 be set such that A3: for x being set holds x in F1 iff x is Functor of C,D and A4: for x being set holds x in F2 iff x is Functor of C,D; now let x be object; x in F1 iff x is Functor of C,D by A3; hence x in F1 iff x in F2 by A4; end; hence thesis by TARSKI:2; end; end; registration let C,D; cluster Funct(C,D) -> non empty; coherence proof set x = the Functor of C,D; x in Funct(C,D) by Def2; hence thesis; end; end; definition let C,D; mode FUNCTOR-DOMAIN of C,D -> non empty set means :Def3: for x being Element of it holds x is Functor of C,D; existence proof take Funct(C,D); thus thesis by Def2; end; end; definition let C,D; let F be FUNCTOR-DOMAIN of C,D; redefine mode Element of F -> Functor of C,D; coherence by Def3; end; definition let A be non empty set; let C,D; let F be FUNCTOR-DOMAIN of C,D, T be Function of A,F, x be Element of A; redefine func T.x -> Element of F; coherence proof thus T.x is Element of F; end; end; definition let C,D; redefine func Funct(C,D) -> FUNCTOR-DOMAIN of C,D; coherence proof let x be Element of Funct(C,D); thus thesis by Def2; end; end; :: Subcategory definition let C; mode Subcategory of C -> Category means :Def4: the carrier of it c= the carrier of C & (for a,b being Object of it, a9,b9 being Object of C st a = a9 & b = b9 holds Hom(a,b) c= Hom(a9,b9)) & the Comp of it c= the Comp of C & for a being Object of it, a9 being Object of C st a = a9 holds id a = id a9; existence proof take C; thus thesis; end; end; registration let C; cluster strict for Subcategory of C; existence proof set c = the Object of C; set E = 1Cat(c,id c); now thus the carrier of E c= the carrier of C proof let a be object; assume a in the carrier of E; then a = c by TARSKI:def 1; hence thesis; end; thus for a,b being Object of E, a9,b9 being Object of C st a = a9 & b = b9 holds Hom(a,b) c= Hom(a9,b9) proof let a,b be Object of E, a9,b9 be Object of C; assume a = a9 & b = b9; then A1: a9 = c & b9 = c by TARSKI:def 1; let x be object; assume x in Hom(a,b); then x = id c by TARSKI:def 1; hence thesis by A1,CAT_1:27; end; thus the Comp of E c= the Comp of C proof reconsider i = id c as Morphism of C; A2: Hom(c,c) <> {}; A3: dom id c = c & cod id c = c; then A4: [id c,id c] in dom the Comp of C by CAT_1:15; the Comp of E = (id c,id c).-->((id c)*(id c)) .= (id c,id c).-->((id c)(*)i) by A2,CAT_1:def 13 .= [id c,id c].-->(the Comp of C).(id c,id c) by A3,CAT_1:16; hence thesis by A4,FUNCT_4:7; end; let a be Object of E, a9 be Object of C; assume a = a9; then a9 = c by TARSKI:def 1; hence id a = id a9 by TARSKI:def 1; end; then E is Subcategory of C by Def4; hence thesis; end; end; reserve E for Subcategory of C; theorem Th2: for e being Object of E holds e is Object of C proof let e be Object of E; e in the carrier of E & the carrier of E c= the carrier of C by Def4; hence thesis; end; theorem Th3: the carrier' of E c= the carrier' of C proof let x be object; assume x in the carrier' of E; then reconsider f = x as Morphism of E; set a = dom f, b = cod f; reconsider a9 = a, b9 = b as Object of C by Th2; f in Hom(a,b) & Hom(a,b) c= Hom(a9,b9) by Def4; then f in Hom(a9,b9) & Hom(a9,b9) <> {}; hence thesis; end; theorem Th4: for f being Morphism of E holds f is Morphism of C proof let f be Morphism of E; f in the carrier' of E & the carrier' of E c= the carrier' of C by Th3; hence thesis; end; theorem Th5: for f being (Morphism of E), f9 being Morphism of C st f = f9 holds dom f = dom f9 & cod f = cod f9 proof let f be (Morphism of E), f9 be Morphism of C such that A1: f = f9; set a = dom f, b = cod f; reconsider a9 = a, b9 = b as Object of C by Th2; f in Hom(a,b) & Hom(a,b) c= Hom(a9,b9) by Def4; hence thesis by A1,CAT_1:1; end; theorem for a,b being Object of E, a9,b9 being Object of C,f being Morphism of a, b st a = a9 & b = b9 & Hom(a,b)<>{} holds f is Morphism of a9,b9 proof let a,b be Object of E, a9,b9 be Object of C, f be Morphism of a,b; assume a = a9 & b = b9 & Hom(a,b)<>{}; then f in Hom(a,b) & Hom(a,b) c= Hom(a9,b9) by Def4,CAT_1:def 5; then f in Hom(a9,b9) & Hom(a9,b9) <> {}; hence thesis by CAT_1:def 5; end; theorem Th7: for f,g being (Morphism of E), f9,g9 being Morphism of C st f = f9 & g = g9 & dom g = cod f holds g(*)f = g9(*)f9 proof let f,g be (Morphism of E), f9,g9 be Morphism of C such that A1: f = f9 & g = g9 and A2: dom g = cod f; dom g = dom g9 & cod f = cod f9 by A1,Th5; then A3: g9(*)f9 = (the Comp of C).(g9,f9) by A2,CAT_1:16; A4: the Comp of E c= the Comp of C by Def4; g(*)f = (the Comp of E).(g,f) & [g,f] in dom(the Comp of E) by A2,CAT_1:15,16; hence thesis by A1,A3,A4,GRFUNC_1:2; end; theorem Th8: C is Subcategory of C proof thus the carrier of C c= the carrier of C; thus thesis; end; theorem Th9: id E is Functor of E,C proof rng id E c= the carrier' of C by Th3; then reconsider T = id E as Function of the carrier' of E,the carrier' of C by FUNCT_2:6; now thus for e being Object of E ex c being Object of C st T.(id e) = id c proof let e be Object of E; reconsider c = e as Object of C by Th2; T.(id e) = id e by FUNCT_1:18 .= id c by Def4; hence thesis; end; thus for f being Morphism of E holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f) proof let f be Morphism of E; A1: T.(id dom f) = id dom f by FUNCT_1:18 .= id dom ((id E).f) by FUNCT_1:18; A2: T.(id cod f) = id cod f by FUNCT_1:18 .= id cod ((id E).f) by FUNCT_1:18; dom (T.f) = dom((id E).f) & cod (T.f) = cod((id E).f) by Th5; hence thesis by A1,A2,Def4; end; let f,g be Morphism of E; A3: T.f = f & T.g = g by FUNCT_1:18; assume A4: dom g = cod f; then T.(g(*)f) = ((id E).g)(*)((id E).f) by CAT_1:64; hence T.(g(*)f) = (T.g)(*)(T.f) by A4,A3,Th7; end; hence thesis by CAT_1:61; end; definition let C,E; func incl(E) -> Functor of E,C equals id E; coherence by Th9; end; theorem Th10: for a being Object of E holds (Obj incl E).a = a proof let a be Object of E; reconsider a9 = a as Object of C by Th2; id a9 = id a by Def4 .= (incl E).(id a) by FUNCT_1:18 .= id((Obj incl E).a) by CAT_1:68; hence thesis by CAT_1:59; end; theorem for a being Object of E holds (incl E).a = a by Th10; theorem incl E is faithful proof let a,b be Object of E such that Hom(a,b) <> {}; let f1,f2 be Morphism of a,b; (incl E).f1 = f1 by FUNCT_1:18; hence thesis by FUNCT_1:18; end; theorem Th13: incl E is full iff for a,b being Object of E, a9,b9 being Object of C st a = a9 & b = b9 holds Hom(a,b) = Hom(a9,b9) proof set T = incl E; thus T is full implies for a,b being Object of E, a9,b9 being Object of C st a = a9 & b = b9 holds Hom(a,b) = Hom(a9,b9) proof assume A1: for a,b being Object of E st Hom(T.a,T.b) <> {} for g being Morphism of T.a,T.b holds Hom(a,b) <> {} & ex f being Morphism of a,b st g = T. f; let a,b be Object of E, a9,b9 be Object of C such that A2: a = a9 & b = b9; now let x be object; Hom(a,b) c= Hom(a9,b9) by A2,Def4; hence x in Hom(a,b) implies x in Hom(a9,b9); assume A3: x in Hom(a9,b9); A4: T.a = a9 & T.b = b9 by A2,Th10; then reconsider g = x as Morphism of T.a,T.b by A3,CAT_1:def 5; consider f being Morphism of a,b such that A5: g = T.f by A1,A4,A3; A6: g = f by A5,FUNCT_1:18; Hom(a,b) <> {} by A1,A4,A3; hence x in Hom(a,b) by A6,CAT_1:def 5; end; hence thesis by TARSKI:2; end; assume A7: for a,b being Object of E, a9,b9 being Object of C st a = a9 & b = b9 holds Hom(a,b) = Hom(a9,b9); let a,b be Object of E such that A8: Hom(T.a,T.b) <> {}; let g be Morphism of T.a,T.b; A9: g in Hom(T.a,T.b) by A8,CAT_1:def 5; A10: a = T.a & b = T.b by Th10; hence Hom(a,b) <> {} by A7,A8; Hom(a,b) = Hom(T.a,T.b) by A7,A10; then reconsider f = g as Morphism of a,b by A9,CAT_1:def 5; take f; thus thesis by FUNCT_1:18; end; definition let D; let C be Subcategory of D; attr C is full means :Def6: for c1,c2 being Object of C, d1,d2 being Object of D st c1 = d1 & c2 = d2 holds Hom(c1,c2) = Hom(d1,d2); end; registration let D; cluster full for Subcategory of D; existence proof reconsider C = D as Subcategory of D by Th8; take C; let c1,c2 be Object of C, d1,d2 being Object of D; assume c1 = d1 & c2 = d2; hence Hom(c1,c2) = Hom(d1,d2); end; end; theorem E is full iff incl(E) is full by Th13; theorem Th15: for O being non empty Subset of the carrier of C holds union{Hom (a,b) where a is Object of C,b is Object of C: a in O & b in O} is non empty Subset of the carrier' of C proof let O be non empty Subset of the carrier of C; set H = {Hom(a,b) where a is Object of C, b is Object of C: a in O & b in O}; set M = union H; A1: M c= the carrier' of C proof let x be object; assume x in M; then consider X being set such that A2: x in X and A3: X in H by TARSKI:def 4; ex a,b being Object of C st X = Hom(a,b) & a in O & b in O by A3; hence thesis by A2; end; now set a = the Element of O; reconsider a as Object of C; id a in Hom(a,a) & Hom(a,a) in H by CAT_1:27; then id a in M by TARSKI:def 4; hence ex f being set st f in M; end; hence thesis by A1; end; theorem Th16: for O being non empty Subset of the carrier of C, M being non empty set st M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} holds (the Source of C)|M is Function of M,O & (the Target of C)|M is Function of M,O & (the Comp of C)||M is PartFunc of [:M,M:],M proof let O be non empty Subset of the carrier of C; set H = {Hom(a,b) where a is Object of C, b is Object of C: a in O & b in O}; A1: dom the Source of C = the carrier' of C by FUNCT_2:def 1; let M be non empty set such that A2: M = union H; A3: now let f be Morphism of C; assume f in M; then consider X being set such that A4: f in X and A5: X in H by A2,TARSKI:def 4; ex a,b being Object of C st X = Hom(a,b) & a in O & b in O by A5; hence dom f in O & cod f in O by A4,CAT_1:1; end; set d = (the Source of C)|M, c = (the Target of C)|M, p = (the Comp of C)||M; A6: dom the Target of C = the carrier' of C by FUNCT_2:def 1; A7: dom d = (dom the Source of C) /\ M by RELAT_1:61; A8: rng d c= O proof let y be object; assume y in rng d; then consider x being object such that A9: x in dom d and A10: y = d.x by FUNCT_1:def 3; reconsider f = x as Morphism of C by A1,A7,A9,XBOOLE_0:def 4; d.f = dom f & f in M by A7,A9,FUNCT_1:47,XBOOLE_0:def 4; hence thesis by A3,A10; end; A11: M is non empty Subset of the carrier' of C by A2,Th15; then A12: dom c = M by A6,RELAT_1:62; A13: dom c = (dom the Target of C) /\ M by RELAT_1:61; A14: rng c c= O proof let y be object; assume y in rng c; then consider x being object such that A15: x in dom c and A16: y = c.x by FUNCT_1:def 3; reconsider f = x as Morphism of C by A6,A13,A15,XBOOLE_0:def 4; c.f = cod f & f in M by A13,A15,FUNCT_1:47,XBOOLE_0:def 4; hence thesis by A3,A16; end; dom d = M by A1,A11,RELAT_1:62; hence d is Function of M,O & c is Function of M,O by A8,A14,A12,FUNCT_2:def 1 ,RELSET_1:4; A17: dom p = (dom the Comp of C) /\ [:M,M:] by RELAT_1:61; A18: dom the Comp of C c= [:the carrier' of C,the carrier' of C:] by RELAT_1:def 18; rng p c= M proof let y be object; assume y in rng p; then consider x being object such that A19: x in dom p and A20: y = p.x by FUNCT_1:def 3; A21: x in dom the Comp of C by A17,A19,XBOOLE_0:def 4; then consider g,f being Morphism of C such that A22: x = [g,f] by A18,DOMAIN_1:1; A23: [g,f] in [:M,M:] by A17,A19,A22,XBOOLE_0:def 4; then g in M by ZFMISC_1:87; then A24: cod g in O by A3; dom g = cod f by A21,A22,CAT_1:15; then A25: dom(g(*)f) = dom f & cod(g(*)f) = cod g by CAT_1:17; f in M by A23,ZFMISC_1:87; then dom f in O by A3; then A26: Hom(dom(g(*)f),cod(g(*)f)) in H by A24,A25; A27: g(*)f in Hom(dom(g(*)f),cod(g(*)f )); p.x = (the Comp of C).(g,f) by A19,A22,FUNCT_1:47 .= g(*)f by A21,A22,CAT_1:def 1; hence thesis by A2,A20,A26,A27,TARSKI:def 4; end; hence p is PartFunc of [:M,M:],M by A17,RELSET_1:4,XBOOLE_1:17; thus thesis; end; registration let O, M be non empty set, d,c being Function of M,O, p being PartFunc of [: M,M:],M; cluster CatStr(#O,M,d,c,p#) -> non void non empty; coherence; end; Lm1: for O being non empty Subset of the carrier of C, M being non empty set, d,c being Function of M,O, p being PartFunc of [:M,M:],M, i being Function of O,M st M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} & d = (the Source of C)|M & c = (the Target of C)|M & p = (the Comp of C)||M holds CatStr(#O,M,d,c,p#) is Category proof let O be non empty Subset of the carrier of C, M be non empty set, d,c be Function of M,O, p be PartFunc of [:M,M:],M, i be Function of O,M; set H = {Hom(a,b) where a is Object of C, b is Object of C: a in O & b in O}; assume that A1: M = union H and A2: d = (the Source of C)|M and A3: c = (the Target of C)|M and A4: p = (the Comp of C)||M; set B = CatStr(#O,M,d,c,p#); A5: now let f be Morphism of B; consider X being set such that A6: f in X and A7: X in H by A1,TARSKI:def 4; ex a,b being Object of C st X = Hom(a,b) & a in O & b in O by A7; hence f is Morphism of C by A6; end; A8: for f,g being Morphism of B holds [g,f] in dom(p) iff d.g=c.f proof let f,g be Morphism of B; reconsider gg=g, ff=f as Morphism of C by A5; A9: d.g = dom gg & c.f = cod ff by A2,A3,FUNCT_1:49; thus [g,f] in dom(p) implies d.g = c.f proof assume [g,f] in dom(p); then [g,f] in (dom the Comp of C) /\ [:M,M:] by A4,RELAT_1:61; then [gg,ff] in (dom the Comp of C) by XBOOLE_0:def 4; hence thesis by A9,CAT_1:def 6; end; assume d.g=c.f; then [g,f] in dom the Comp of C by A9,CAT_1:def 6; then [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def 4; hence thesis by A4,RELAT_1:61; end; A10: B is Category-like by A8; A11: B is transitive proof thus for f,g being Morphism of B st dom g = cod f holds dom(g(*)f) = dom f & cod(g(*)f) = cod g proof let f,g be Morphism of B; reconsider ff=f, gg=g as Morphism of C by A5; A12: d.g = dom gg & c.f = cod ff by A2,A3,FUNCT_1:49; assume A13: dom g = cod f; A14: [g,f] in dom the Comp of B by A13,A8; A15: p.(g,f) = g(*)f by A13,A8,CAT_1:def 1; A16: dom p c= dom the Comp of C by A4,RELAT_1:60; A17: p.[g,f] = (the Comp of C).(g,f) by A4,A8,A13,FUNCT_1:47 .= gg(*)ff by A16,A14,CAT_1:def 1; thus dom(g(*)f) = dom(gg(*)ff) by A17,A2,A15,FUNCT_1:49 .= dom ff by A13,A12,CAT_1:def 7 .= dom f by A2,FUNCT_1:49; thus cod(g(*)f) = cod(gg(*)ff) by A17,A3,A15,FUNCT_1:49 .= cod gg by A13,A12,CAT_1:def 7 .= cod g by A3,FUNCT_1:49; end; end; A18: B is associative proof thus for f,g,h being Morphism of B st dom h = cod g & dom g = cod f holds h(*)(g(*)f) = (h(*)g)(*)f proof let f,g,h be Morphism of B; reconsider ff=f, gg=g, hh=h as Morphism of C by A5; assume that A19: dom h = cod g and A20: dom g = cod f; A21: h(*)g = (the Comp of B).(h,g) by A19,A8,CAT_1:def 1; A22: g(*)f = (the Comp of B).(g,f) by A20,A8,CAT_1:def 1; A23: dom(h(*)g) = dom g by A11,A19; A24: c.g = cod gg & d.g = dom gg by A2,A3,FUNCT_1:49; A25: c.f = cod ff by A3,FUNCT_1:49; A26: f is Morphism of C & d.h = dom hh by A2,A5,FUNCT_1:49; A27: dom gg = d.g by A2,FUNCT_1:49 .= cod ff by A3,A20,FUNCT_1:49; then A28: gg(*)ff = (the Comp of C).(gg,ff) by CAT_1:16; A29: dom hh = d.h by A2,FUNCT_1:49 .= cod gg by A3,A19,FUNCT_1:49; then A30: cod(gg(*)ff) = dom hh by A27,CAT_1:def 7; A31: hh(*)gg = (the Comp of C).(hh,gg) by A29,CAT_1:16; A32: cod ff= dom(hh(*)gg) by A27,A29,CAT_1:def 7; A33: cod(g(*)f) = cod g by A11,A20; hence h(*)(g(*)f) = (the Comp of B).(h,(the Comp of B).(g,f)) by A22,A19,A8 ,CAT_1:def 1 .= (the Comp of C).[h,p.[g,f]] by A4,A8,A19,A33,A22,FUNCT_1:47 .= (the Comp of C).(hh,gg(*)ff) by A4,A8,A20,A28,FUNCT_1:47 .= hh(*)(gg(*)ff) by A30,CAT_1:16 .= (hh(*)gg)(*)ff by A19,A20,A26,A24,A25,CAT_1:def 8 .= (the Comp of C).((the Comp of C).(hh,gg),ff) by A31,A32,CAT_1:16 .= (the Comp of C).[p.[h,g],f] by A4,A8,A19,FUNCT_1:47 .= (the Comp of B).((the Comp of B).(h,g),f) by A4,A8,A20,A23,A21,FUNCT_1:47 .= h(*)g(*)f by A21,A20,A8,A23,CAT_1:def 1; end; end; A34: B is reflexive proof let b be Object of B; b in O; then reconsider bb = b as Object of C; A35: Hom(bb,bb) in H; id bb in Hom(bb,bb) by CAT_1:27; then reconsider ii = id bb as Morphism of B by A35,A1,TARSKI:def 4; A36: dom ii = dom id bb by A2,FUNCT_1:49 .= bb; cod ii = cod id bb by A3,FUNCT_1:49 .= bb; then ii in Hom(b,b) by A36; hence Hom(b,b)<>{}; end; B is with_identities proof let a be Element of B; a in O; then reconsider aa = a as Object of C; A37: Hom(aa,aa) in H; id aa in Hom(aa,aa) by CAT_1:27; then reconsider ii = id aa as Morphism of B by A37,A1,TARSKI:def 4; A38: dom ii = dom id aa by A2,FUNCT_1:49 .= aa; A39: cod ii = cod id aa by A3,FUNCT_1:49 .= aa; then reconsider ii as Morphism of a,a by A38,CAT_1:4; take ii; let b be Element of B; b in O; then reconsider bb = b as Object of C; thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g proof assume A40: Hom(a,b)<>{}; let g be Morphism of a,b; reconsider gg = g as Morphism of C by A5; A41: dom gg = dom g by A2,FUNCT_1:49 .= aa by A40,CAT_1:5; A42: cod id aa = aa; cod gg = cod g by A3,FUNCT_1:49 .= bb by A40,CAT_1:5; then reconsider gg as Morphism of aa,bb by A41,CAT_1:4; A43: dom g = a by A40,CAT_1:5; hence g(*)ii = p.(g,ii) by A39,A8,CAT_1:def 1 .= (the Comp of C).(gg,id aa) by A43,A4,A39,A8,FUNCT_1:47 .= gg(*)id aa by A41,A42,CAT_1:16 .= g by A41,CAT_1:22; end; thus Hom(b,a)<>{} implies for f being Morphism of b,a holds ii(*)f = f proof assume A44: Hom(b,a)<>{}; let g be Morphism of b,a; reconsider gg = g as Morphism of C by A5; A45: cod gg = cod g by A3,FUNCT_1:49 .= aa by A44,CAT_1:5; A46: dom id aa = aa; dom gg = dom g by A2,FUNCT_1:49 .= bb by A44,CAT_1:5; then reconsider gg as Morphism of bb,aa by A45,CAT_1:4; A47: cod g = a by A44,CAT_1:5; hence ii(*)g = p.(ii,g) by A38,A8,CAT_1:def 1 .= (the Comp of C).(id aa,gg) by A4,A47,A38,A8,FUNCT_1:47 .= (id aa)(*)gg by A45,A46,CAT_1:16 .= g by A45,CAT_1:21; end; end; hence B is Category by A10,A11,A18,A34; end; Lm2: for O being non empty Subset of the carrier of C, M being non empty set, d,c being Function of M,O, p being PartFunc of [:M,M:],M, i being Function of O,M st M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} & d = (the Source of C)|M & c = (the Target of C)|M & p = (the Comp of C)||M holds CatStr(#O,M,d,c,p#) is Subcategory of C proof let O be non empty Subset of the carrier of C, M be non empty set, d,c be Function of M,O, p be PartFunc of [:M,M:],M, i be Function of O,M; set H = {Hom(a,b) where a is Object of C, b is Object of C: a in O & b in O}; assume that A1: M = union H and A2: d = (the Source of C)|M and A3: c = (the Target of C)|M and A4: p = (the Comp of C)||M; set B = CatStr(#O,M,d,c,p#); A5: now let f be Morphism of B; consider X being set such that A6: f in X and A7: X in H by A1,TARSKI:def 4; ex a,b being Object of C st X = Hom(a,b) & a in O & b in O by A7; hence f is Morphism of C by A6; end; A8: for a,b being Object of B, a9,b9 being Object of C st a = a9 & b = b9 holds Hom(a,b) = Hom(a9,b9) proof let a,b be Object of B, a9,b9 be Object of C such that A9: a = a9 & b = b9; now let x be object; thus x in Hom(a,b) implies x in Hom(a9,b9) proof assume A10: x in Hom(a,b); then reconsider f = x as Morphism of B; reconsider f9 = f as Morphism of C by A5; cod f = cod f9 by A3,FUNCT_1:49; then A11: b = cod f9 by A10,CAT_1:1; dom f = dom f9 by A2,FUNCT_1:49; then a = dom f9 by A10,CAT_1:1; hence thesis by A9,A11; end; assume A12: x in Hom(a9,b9); then reconsider f9 = x as Morphism of C; Hom(a9,b9) in H by A9; then reconsider f = f9 as Morphism of B by A1,A12,TARSKI:def 4; cod f = cod f9 by A3,FUNCT_1:49; then A13: cod f = b9 by A12,CAT_1:1; dom f = dom f9 by A2,FUNCT_1:49; then dom f = a9 by A12,CAT_1:1; hence x in Hom(a,b) by A9,A13; end; hence thesis by TARSKI:2; end; reconsider B as Category by Lm1,A1,A2,A3,A4; A14: for a be Object of B, a9 be Object of C st a = a9 holds id a = id a9 proof let a be Object of B, a9 be Object of C such that A15: a = a9; A16: Hom(a9,a9) in H by A15; A17: id a9 in Hom(a9,a9) by CAT_1:27; then reconsider ii = id a9 as Morphism of B by A16,A1,TARSKI:def 4; A18: dom ii = dom id a9 by A2,FUNCT_1:49 .= a9; A19: cod ii = cod id a9 by A3,FUNCT_1:49 .= a9; ii in Hom(a,a) by A17,A8,A15; then reconsider ii as Morphism of a,a by CAT_1:def 5; A20: for f,g being Morphism of B holds [g,f] in dom(p) iff d.g=c.f proof let f,g be Morphism of B; reconsider gg=g, ff=f as Morphism of C by A5; A21: d.g = dom gg & c.f = cod ff by A2,A3,FUNCT_1:49; thus [g,f] in dom(p) implies d.g = c.f proof assume [g,f] in dom(p); then [g,f] in (dom the Comp of C) /\ [:M,M:] by A4,RELAT_1:61; then [gg,ff] in (dom the Comp of C) by XBOOLE_0:def 4; hence thesis by A21,CAT_1:def 6; end; assume d.g=c.f; then [g,f] in dom the Comp of C by A21,CAT_1:def 6; then [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def 4; hence thesis by A4,RELAT_1:61; end; for b being Object of B holds (Hom(a,b) <> {} implies for f being Morphism of a,b holds f(*)ii = f) & (Hom(b,a) <> {} implies for f being Morphism of b,a holds ii(*)f = f) proof let b be Object of B; b in O; then reconsider bb = b as Element of C; thus Hom(a,b) <> {} implies for f being Morphism of a,b holds f(*)ii = f proof assume A22: Hom(a,b)<>{}; let g be Morphism of a,b; reconsider gg = g as Morphism of C by A5; A23: dom gg = dom g by A2,FUNCT_1:49 .= a9 by A15,A22,CAT_1:5; A24: cod id a9 = a9; cod gg = cod g by A3,FUNCT_1:49 .= bb by A22,CAT_1:5; then reconsider gg as Morphism of a9,bb by A23,CAT_1:4; A25: dom g = a by A22,CAT_1:5; hence g(*)ii = p.(g,ii) by A19,A20,A15,CAT_1:def 1 .= (the Comp of C).(gg,id a9) by A19,A20,A15,A4,A25,FUNCT_1:47 .= gg(*)id a9 by A23,A24,CAT_1:16 .= g by A23,CAT_1:22; end; assume A26: Hom(b,a)<>{}; let g be Morphism of b,a; reconsider gg = g as Morphism of C by A5; A27: cod gg = cod g by A3,FUNCT_1:49 .= a9 by A15,A26,CAT_1:5; A28: dom id a9 = a9; dom gg = dom g by A2,FUNCT_1:49 .= bb by A26,CAT_1:5; then reconsider gg as Morphism of bb,a9 by A27,CAT_1:4; A29: cod g = a by A26,CAT_1:5; hence ii(*)g = p.(ii,g) by A18,A20,A15,CAT_1:def 1 .= (the Comp of C).(id a9,gg) by A18,A20,A15,A4,A29,FUNCT_1:47 .= (id a9)(*)gg by A27,A28,CAT_1:16 .= g by A27,CAT_1:21; end; hence id a = id a9 by CAT_1:def 12; end; ( for a,b being Object of B, a9,b9 being Object of C st a = a9 & b = b9 holds Hom(a,b) c= Hom(a9,b9))& the Comp of B c= the Comp of C by A4,A8,RELAT_1:59; hence thesis by A14,Def4; end; theorem for O being non empty Subset of the carrier of C, M being non empty set, d,c being Function of M,O, p being PartFunc of [:M,M:],M, i being Function of O,M st M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} & d = (the Source of C)|M & c = (the Target of C)|M & p = (the Comp of C)||M holds CatStr(#O,M,d,c,p#) is full Subcategory of C proof let O be non empty Subset of the carrier of C, M be non empty set, d,c be Function of M,O, p be PartFunc of [:M,M:],M, i be Function of O,M; set H = {Hom(a,b) where a is Object of C, b is Object of C: a in O & b in O}; assume that A1: M = union H and A2: d = (the Source of C)|M and A3: c = (the Target of C)|M and A4: p = (the Comp of C)||M; set B = CatStr(#O,M,d,c,p#); A5: now let f be Morphism of B; consider X being set such that A6: f in X and A7: X in H by A1,TARSKI:def 4; ex a,b being Object of C st X = Hom(a,b) & a in O & b in O by A7; hence f is Morphism of C by A6; end; A8: for a,b being Object of B, a9,b9 being Object of C st a = a9 & b = b9 holds Hom(a,b) = Hom(a9,b9) proof let a,b be Object of B, a9,b9 be Object of C such that A9: a = a9 & b = b9; now let x be object; thus x in Hom(a,b) implies x in Hom(a9,b9) proof assume A10: x in Hom(a,b); then reconsider f = x as Morphism of B; reconsider f9 = f as Morphism of C by A5; cod f = cod f9 by A3,FUNCT_1:49; then A11: b = cod f9 by A10,CAT_1:1; dom f = dom f9 by A2,FUNCT_1:49; then a = dom f9 by A10,CAT_1:1; hence thesis by A9,A11; end; assume A12: x in Hom(a9,b9); then reconsider f9 = x as Morphism of C; Hom(a9,b9) in H by A9; then reconsider f = f9 as Morphism of B by A1,A12,TARSKI:def 4; cod f = cod f9 by A3,FUNCT_1:49; then A13: cod f = b9 by A12,CAT_1:1; dom f = dom f9 by A2,FUNCT_1:49; then dom f = a9 by A12,CAT_1:1; hence x in Hom(a,b) by A9,A13; end; hence thesis by TARSKI:2; end; reconsider B as Subcategory of C by Lm2,A1,A2,A3,A4; B is full by A8; hence thesis; end; theorem for O being non empty Subset of the carrier of C, M being non empty set , d,c being Function of M,O, p being PartFunc of [:M,M:],M st CatStr(#O,M,d,c,p#) is full Subcategory of C holds M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} & d = (the Source of C)|M & c = (the Target of C)|M & p = (the Comp of C)||M proof let O be non empty Subset of the carrier of C, M be non empty set, d,c be Function of M,O, p be PartFunc of [:M,M:],M; set H = {Hom(a,b) where a is Object of C, b is Object of C: a in O & b in O}; set B = CatStr(#O,M,d,c,p#); assume A1: B is full Subcategory of C; A2: for f being Morphism of B holds d.f = (the Source of C).f & c.f = (the Target of C).f proof let f be Morphism of B; reconsider f9 = f as Morphism of C by A1,Th4; dom f = dom f9 & cod f = cod f9 by A1,Th5; hence thesis; end; now let x be object; thus x in M implies x in union H proof assume x in M; then reconsider f = x as Morphism of B; reconsider f9 = f as Morphism of C by A1,Th4; set a9 = dom f9, b9 = cod f9; (the Source of B).f = (the Source of C).f9 & (the Target of B).f = ( the Target of C).f9 by A2; then f in Hom(a9,b9) & Hom(a9,b9) in H; hence thesis by TARSKI:def 4; end; assume x in union H; then consider X being set such that A3: x in X and A4: X in H by TARSKI:def 4; consider a9,b9 being Object of C such that A5: X = Hom(a9,b9) and A6: a9 in O & b9 in O by A4; reconsider a = a9, b = b9 as Object of B by A6; Hom(a,b) = Hom(a9,b9) by A1,Def6; hence x in M by A3,A5; end; hence M = union H by TARSKI:2; then reconsider d9 = (the Source of C)|M, c9 = (the Target of C)|M as Function of M,O by Th16; set p9 = (the Comp of C)||M; now let f be Element of M; d.f = (the Source of C).f by A2; hence d.f = d9.f by FUNCT_1:49; end; hence d = (the Source of C)|M by FUNCT_2:63; now let f be Element of M; c.f = (the Target of C).f by A2; hence c.f = c9.f by FUNCT_1:49; end; hence c = (the Target of C)|M by FUNCT_2:63; now A7: dom p c= [:M,M:] by RELAT_1:def 18; A8: dom p9 = (dom the Comp of C) /\ [:M,M:] by RELAT_1:61; the Comp of B c= the Comp of C by A1,Def4; then dom p c= dom the Comp of C by GRFUNC_1:2; then A9: dom p c= dom p9 by A7,A8,XBOOLE_1:19; dom p9 c= dom p proof let x be object; assume A10: x in dom p9; then x in [:M,M:] by A8,XBOOLE_0:def 4; then consider g,f being Element of M such that A11: x = [g,f] by DOMAIN_1:1; reconsider f,g as Morphism of B; reconsider f9 = f,g9 = g as Morphism of C by A1,Th4; [g,f] in dom the Comp of C by A8,A10,A11,XBOOLE_0:def 4; then A12: dom g9 = cod f9 by CAT_1:15; cod f = cod f9 & dom g = dom g9 by A1,Th5; hence thesis by A1,A11,A12,CAT_1:15; end; hence dom p = dom p9 by A9,XBOOLE_0:def 10; let x be object; assume A13: x in dom p; then consider g,f being Element of M such that A14: x = [g,f] by A7,DOMAIN_1:1; reconsider f,g as Morphism of B; A15: dom g = cod f by A1,A13,A14,CAT_1:15; reconsider f9 = f,g9 = g as Morphism of C by A1,Th4; A16: cod f = cod f9 & dom g = dom g9 by A1,Th5; p.x = p.(g,f) by A14; hence p.x = g(*)f by A1,A15,CAT_1:16 .= g9(*)f9 by A1,A15,Th7 .= (the Comp of C).(g9,f9) by A16,A1,A13,A14,CAT_1:15,16 .= p9.x by A9,A13,A14,FUNCT_1:47; end; hence p = (the Comp of C)||M by FUNCT_1:2; end; :: Product of Categories definition let C,D; func [:C,D:] -> Category equals CatStr (# [:the carrier of C,the carrier of D:], [:the carrier' of C,the carrier' of D:], [:the Source of C,the Source of D:], [:the Target of C,the Target of D:], |:the Comp of C, the Comp of D:| #); coherence proof set O = [:the carrier of C,the carrier of D:], M = [:the carrier' of C,the carrier' of D:], d = [:the Source of C,the Source of D:], c = [:the Target of C,the Target of D:], p = |:the Comp of C, the Comp of D:|; A1: for f,g being Element of M st d.g = c.f holds [g`1,f`1] in dom(the Comp of C) & [g`2,f`2] in dom(the Comp of D) proof let f,g be Element of M; A2: d.(g`1,g`2) = [(the Source of C).g`1,(the Source of D).g`2] & c.(f`1 ,f`2) = [(the Target of C).f`1,(the Target of D).f`2] by FUNCT_3:75; assume A3: d.g = c.f; g = [g`1,g`2] & f = [f`1,f`2] by MCART_1:21; then dom(g`1) = cod(f`1) & dom(g`2) = cod(f`2) by A2,A3,XTUPLE_0:1; hence thesis by CAT_1:def 6; end; A4: for f,g being Element of M st [g,f] in dom(p) holds dom(g`1) = cod(f`1) & dom(g`2) = cod(f`2) proof let f,g be Element of M; assume A5: [g,f] in dom(p); g = [g`1,g`2] & f = [f`1,f`2] by MCART_1:21; then [g`1,f`1] in dom(the Comp of C) & [g`2,f`2] in dom(the Comp of D) by A5,FUNCT_4:54; hence thesis by CAT_1:def 6; end; set B = CatStr(#O,M,d,c,p#); A6: B is Category-like proof let ff,gg be Morphism of B; reconsider f = ff, g=gg as Element of M; A7: g = [g`1,g`2] & f = [f`1,f`2] by MCART_1:21; thus [gg,ff] in dom(the Comp of B) implies dom gg = cod ff proof A8: d.(g`1,g`2) = [dom(g`1),dom(g`2)] & c.( f`1,f`2) = [cod(f`1),cod(f`2)] by FUNCT_3:75; assume A9: [gg,ff] in dom(the Comp of B); then dom(g`1) = cod(f`1) by A4; hence thesis by A4,A7,A9,A8; end; assume dom gg = cod ff; then [g`1,f`1] in dom(the Comp of C) & [g`2,f`2] in dom(the Comp of D) by A1; hence thesis by A7,FUNCT_4:54; end; A10: for f,g being Morphism of B holds [g,f] in dom(the Comp of B) iff dom g = cod f by A6; A11: for f,g being Element of M st d.g = c.f holds p.(g,f) = [(the Comp of C).(g`1,f`1),(the Comp of D).(g`2,f`2)] proof let f,g be Element of M; reconsider ff=f, gg=g as Morphism of B; assume d.g = c.f; then A12: dom gg = cod ff; g = [g`1,g`2] & f = [f`1,f`2] by MCART_1:21; hence thesis by A12,A10,FUNCT_4:55; end; A13: for f,g being Element of M st d.g = c.f holds d.(p.(g,f)) = d.f & c.(p.(g,f)) = c.g proof let f,g be Element of M; reconsider ff=f, gg=g as Morphism of B; A14: f = [f`1,f`2] & d.(f`1,f`2) = [dom(f`1),dom(f`2)] by FUNCT_3:75,MCART_1:21; assume A15: d.g = c.f; then A16: (the Comp of C).[g`1,f`1] in the carrier' of C by A1,PARTFUN1:4; then A17: (the Comp of C).(g`1,f`1) in dom(the Source of C) by FUNCT_2:def 1; dom gg = cod ff by A15; then A18: [gg,ff] in dom(p) by A6; then A19: dom(g`1) = cod(f`1) by A4; then [g`1,f`1] in dom the Comp of C by CAT_1:def 6; then A20: (the Comp of C).(g`1,f`1) = (g`1)(*)(f`1) by CAT_1:def 1; A21: dom((g`1)(*)(f`1)) = dom(f`1) by A19,CAT_1:def 7; A22: (the Comp of D).[g`2,f`2] in the carrier' of D by A1,A15,PARTFUN1:4; then A23: (the Comp of D).(g`2,f`2) in dom(the Source of D) by FUNCT_2:def 1; A24: dom(g`2) = cod(f`2) by A4,A18; then [g`2,f`2] in dom the Comp of D by CAT_1:def 6; then A25: (the Comp of D).(g`2,f`2) = (g`2)(*)(f`2) by CAT_1:def 1; A26: dom((g`2)(*)(f`2)) = dom(f`2) by A24,CAT_1:def 7; thus d.(p.(g,f)) = d.((the Comp of C).(g`1,f`1),(the Comp of D).(g`2,f`2 )) by A11,A15 .= d.f by A14,A21,A26,A17,A23,A20,A25,FUNCT_3:def 8; A27: g = [g`1,g`2] & c.(g`1,g`2) = [(the Target of C).g`1,(the Target of D).g`2] by FUNCT_3:75,MCART_1:21; A28: cod((g`2)(*)(f`2)) = cod(g`2) by A24,CAT_1:def 7; A29: cod((g`1)(*)(f`1)) = cod(g`1) by A19,CAT_1:def 7; A30: (the Comp of D).(g`2,f`2) in dom(the Target of D) by A22,FUNCT_2:def 1; A31: (the Comp of C).(g`1,f`1) in dom(the Target of C) by A16,FUNCT_2:def 1; thus c.(p.(g,f)) = c.((the Comp of C).(g`1,f`1),(the Comp of D).(g`2,f`2)) by A11,A15 .= c.g by A27,A29,A28,A31,A30,A20,A25,FUNCT_3:def 8; end; A32: B is transitive proof let ff,gg be Morphism of B; reconsider f=ff, g=gg as Element of M; assume A33: dom gg = cod ff; then A34: (the Comp of B).(gg,ff) = gg(*)ff by A10,CAT_1:def 1; thus dom(gg(*)ff) = dom ff by A13,A33,A34; thus cod(gg(*)ff) = cod gg by A13,A33,A34; end; A35: B is associative proof let ff,gg,hh be Morphism of B; reconsider f=ff, g=gg, h=hh as Element of M; assume that A36: dom hh = cod gg and A37: dom gg = cod ff; A38: (the Comp of C).[h`1,g`1] in the carrier' of C & (the Comp of D).[h `2,g`2] in the carrier' of D by A1,A36,PARTFUN1:4; (the Comp of C).[g`1,f`1] in the carrier' of C & (the Comp of D).[g `2,f`2] in the carrier' of D by A1,A37,PARTFUN1:4; then reconsider pgf = [(the Comp of C).[g`1,f`1],(the Comp of D).[g`2,f`2]], phg = [(the Comp of C).[h`1,g`1],(the Comp of D).[h`2,g`2]] as Element of M by A38,ZFMISC_1:87; set pgf2 = pgf`2, phg2 = phg`2; set pgf1 = pgf`1, phg1 = phg`1; A39: p.(g,f) = [(the Comp of C).(g`1,f`1),(the Comp of D).(g`2,f`2)] by A11,A37; A40: d.h = c.(p.(g,f)) by A13,A36,A37; A41: p.(h,g) = [(the Comp of C).(h`1,g`1),(the Comp of D).(h`2,g`2)] by A11,A36; [h`2,g`2] in dom(the Comp of D) by A1,A36; then A42: dom(h`2) = cod(g`2) by CAT_1:def 6; [h`1,g`1] in dom(the Comp of C) by A1,A36; then A43: dom(h`1) = cod(g`1) by CAT_1:def 6; [g`2,f`2] in dom(the Comp of D) by A1,A37; then A44: dom(g`2) = cod(f`2) by CAT_1:def 6; [g`1,f`1] in dom(the Comp of C) by A1,A37; then A45: dom(g`1) = cod(f`1) by CAT_1:def 6; A46: d.(p.(h,g)) = c.f by A13,A36,A37; A47: pgf`1 = (the Comp of C).(g`1,f`1) & phg`1 = (the Comp of C).(h`1,g`1); A48: pgf`2 = (the Comp of D).(g`2,f`2) & phg`2 = (the Comp of D).(h`2,g`2); A49: h`2(*)(g`2(*)f`2) = h`2(*)g`2(*)f`2 by A42,A44,CAT_1:def 8; A50: gg(*)ff = p.(g,f) by A37,A10,CAT_1:def 1; then A51: cod(gg(*)ff) = dom hh by A13,A36,A37; A52: hh(*)gg = p.(h,g) by A36,A10,CAT_1:def 1; then A53: dom(hh(*)gg) = cod ff by A13,A36,A37; A54: cod(g`1(*)f`1) = cod g`1 by A45,CAT_1:def 7; A55: pgf1 = g`1(*)f`1 by A47,A45,CAT_1:16; A56: cod(g`2(*)f`2) = cod g`2 by A44,CAT_1:def 7; pgf2 = g`2(*)f`2 by A48,A44,CAT_1:16; then A57: (the Comp of D).(h`2, pgf2) = h`2(*)(g`2(*)f`2) by A42,A56,CAT_1:16; A58: dom(h`1(*)g`1) = dom g`1 by A43,CAT_1:def 7; A59: phg1 = h`1(*)g`1 by A47,A43,CAT_1:16; A60: dom(h`2(*)g`2) = dom g`2 by A42,CAT_1:def 7; phg2 = h`2(*)g`2 by A48,A42,CAT_1:16; then A61: (the Comp of D).(phg2,f`2) = h`2(*)g`2(*)f`2 by A44,A60,CAT_1:16; thus hh(*)(gg(*)ff) = p.(h,p.(g,f)) by A51,A50,A10,CAT_1:def 1 .= [(the Comp of C).(h`1,pgf1), (the Comp of D).(h`2, pgf2)] by A40,A11,A39 .= [h`1(*)(g`1(*)f`1),h`2(*)(g`2(*)f`2)] by A55,A57,A43,A54,CAT_1:16 .= [h`1(*)g`1(*)f`1,h`2(*)g`2(*)f`2] by A43,A45,A49,CAT_1:def 8 .= [(the Comp of C).(phg1,f`1), (the Comp of D).(phg2,f`2)] by A59,A61,A45,A58,CAT_1:16 .= p.(p.(h,g),f) by A46,A11,A41 .= (hh(*)gg)(*)ff by A53,A10,A52,CAT_1:def 1; end; A62: B is reflexive proof let b be Element of B; reconsider bb=b as Element of O; reconsider ii = [id bb`1, id bb`2] as Morphism of B; A63: cod ii = c.(id bb`1, id bb`2) .= [cod id bb`1,cod id bb`2] by FUNCT_3:75 .= [bb`1,cod id bb`2] .= [bb`1,bb`2] .= bb by MCART_1:21; dom ii = d.(id bb`1, id bb`2) .= [dom id bb`1,dom id bb`2] by FUNCT_3:75 .= [bb`1,dom id bb`2] .= [bb`1,bb`2] .= bb by MCART_1:21; then [id bb`1,id bb`2] in Hom(b,b) by A63; hence Hom(b,b)<>{}; end; B is with_identities proof let a be Element of B; reconsider aa=a as Element of O; reconsider ii = [id aa`1, id aa`2] as Morphism of B; A64: cod ii = c.(id aa`1, id aa`2) .= [cod id aa`1,cod id aa`2] by FUNCT_3:75 .= [aa`1,cod id aa`2] .= [aa`1,aa`2] .= aa by MCART_1:21; A65: dom ii = d.(id aa`1, id aa`2) .= [dom id aa`1,dom id aa`2] by FUNCT_3:75 .= [aa`1,dom id aa`2] .= [aa`1,aa`2] .= aa by MCART_1:21; then reconsider ii = [id aa`1, id aa`2] as Morphism of a,a by A64,CAT_1:4; take ii; let b be Element of B; thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g proof assume A66: Hom(a,b)<>{}; let g be Morphism of a,b; reconsider gg = g as Element of M; cod ii = dom g by A66,A64,CAT_1:5; then A67: [g,ii] in dom p by A6; then A68: dom gg`1 = cod [id aa`1, id aa`2]`1 by A4 .= cod id aa`1; A69: (the Comp of C).(gg`1,id aa`1) = (gg`1)(*)id aa`1 by A68,CAT_1:16 .= gg`1 by A68,CAT_1:22; A70: dom gg`2 = cod [id aa`1, id aa`2]`2 by A4,A67 .= cod id aa`2; A71: (the Comp of D).(gg`2,id aa`2) = (gg`2)(*)id aa`2 by A70,CAT_1:16 .= gg`2 by A70,CAT_1:22; A72: cod ii = dom g by A64,A66,CAT_1:5; then [g,ii] in dom the Comp of B by A6; hence g(*)ii = p.(g,ii) by CAT_1:def 1 .= [(the Comp of C).(gg`1,[id aa`1, id aa`2]`1), (the Comp of D).(gg`2,[id aa`1, id aa`2]`2)] by A11,A72 .= g by A69,A71,MCART_1:21; end; assume A73: Hom(b,a)<>{}; let g be Morphism of b,a; reconsider gg = g as Element of M; dom ii = cod g by A73,A65,CAT_1:5; then A74: [ii,g] in dom p by A6; then A75: cod gg`1 = dom [id aa`1, id aa`2]`1 by A4 .= dom id aa`1; A76: (the Comp of C).(id aa`1,gg`1) = (id aa`1)(*)gg`1 by A75,CAT_1:16 .= gg`1 by A75,CAT_1:21; A77: cod gg`2 = dom [id aa`1, id aa`2]`2 by A4,A74 .= dom id aa`2; A78: (the Comp of D).(id aa`2,gg`2) = (id aa`2)(*)gg`2 by A77,CAT_1:16 .= gg`2 by A77,CAT_1:21; A79: dom ii = cod g by A65,A73,CAT_1:5; then [ii,g] in dom the Comp of B by A6; hence ii(*)g = p.(ii,g) by CAT_1:def 1 .= [(the Comp of C).([id aa`1, id aa`2]`1,gg`1), (the Comp of D).([id aa`1, id aa`2]`2,gg`2)] by A11,A79 .= g by A76,A78,MCART_1:21; end; hence thesis by A6,A32,A35,A62; end; end; theorem the carrier of [:C,D:] = [:the carrier of C,the carrier of D:] & the carrier' of [:C,D:] = [:the carrier' of C,the carrier' of D:] & the Source of [:C,D:] = [:the Source of C,the Source of D:] & the Target of [:C,D:] = [:the Target of C,the Target of D:] & the Comp of [:C,D:] = |:the Comp of C, the Comp of D:|; definition let C,D; let c be Object of C; let d be Object of D; redefine func [c,d] -> Object of [:C,D:]; coherence proof thus [c,d] is Object of [:C,D:]; end; end; ::$CT theorem for cd being Object of [:C,D:] ex c being Object of C, d being Object of D st cd = [c,d] by DOMAIN_1:1; definition let C,D; let f be Morphism of C; let g be Morphism of D; redefine func [f,g] -> Morphism of [:C,D:]; coherence proof thus [f,g] is Morphism of [:C,D:]; end; end; ::$CT theorem for fg being Morphism of [:C,D:] ex f being (Morphism of C), g being Morphism of D st fg = [f,g] by DOMAIN_1:1; theorem Th22: for f being Morphism of C for g being Morphism of D holds dom [f,g] = [dom f,dom g] & cod [f,g] = [cod f,cod g] proof let f be Morphism of C; let g be Morphism of D; thus dom [f,g] = [:the Source of C,the Source of D:].(f,g) .= [dom f,dom g] by FUNCT_3:75; thus cod [f,g] = [:the Target of C,the Target of D:].(f,g) .= [cod f,cod g] by FUNCT_3:75; end; theorem Th23: for f,f9 being Morphism of C for g,g9 being Morphism of D st dom f9 = cod f & dom g9 = cod g holds [f9,g9](*)[f,g] = [f9(*)f,g9(*)g] proof let f,f9 be Morphism of C; let g,g9 be Morphism of D; assume that A1: dom f9 = cod f and A2: dom g9 = cod g; A3: [f9,f] in dom(the Comp of C) & [g9,g] in dom(the Comp of D) by A1,A2, CAT_1:15; dom [f9,g9] = [dom f9,dom g9] & cod [f,g] = [cod f,cod g] by Th22; hence [f9,g9](*)[f,g] = |:the Comp of C, the Comp of D:|.([f9,g9],[f,g]) by A1,A2,CAT_1:16 .= [(the Comp of C).(f9,f),(the Comp of D).(g9,g)] by A3,FUNCT_4:def 3 .= [f9(*)f,(the Comp of D).(g9,g)] by A1,CAT_1:16 .= [f9(*)f,g9(*)g] by A2,CAT_1:16; end; theorem Th24: for f,f9 being Morphism of C for g,g9 being Morphism of D st dom [f9,g9] = cod [f,g] holds [f9,g9](*)[f,g] = [f9(*)f,g9(*)g] proof let f,f9 be Morphism of C; let g,g9 be Morphism of D such that A1: dom [f9,g9] = cod [f,g]; [dom f9,dom g9] = dom [f9,g9] & cod [f,g] = [cod f,cod g] by Th22; then dom f9 = cod f & dom g9 = cod g by A1,XTUPLE_0:1; hence thesis by Th23; end; theorem Th25: for c being Object of C, d being Object of D holds id [c,d] = [id c,id d] proof let c being Object of C; let d being Object of D; A1: dom [id c,id d] = [dom id c,dom id d] by Th22 .= [c,dom id d] .= [c,d]; cod [id c,id d] = [cod id c,cod id d] by Th22 .= [c,cod id d] .= [c,d]; then reconsider m = [id c,id d] as Morphism of [c,d],[c,d] by A1,CAT_1:4; for b being Object of [:C,D:] holds (Hom([c,d],b) <> {} implies for f being Morphism of [c,d],b holds f(*)[id c,id d] = f) & (Hom(b,[c,d]) <> {} implies for f being Morphism of b,[c,d] holds [id c,id d](*)f = f) proof let b be Object of [:C,D:]; thus Hom([c,d],b) <> {} implies for f being Morphism of [c,d],b holds f(*)[id c,id d] = f proof assume A2: Hom([c,d],b) <> {}; let f be Morphism of [c,d],b; consider fc being (Morphism of C), fd being Morphism of D such that A3: f = [fc,fd] by DOMAIN_1:1; A4: [c,d] = dom f by A2,CAT_1:5 .= [dom fc,dom fd] by A3,Th22; then A5: c = dom fc by XTUPLE_0:1; then A6: cod id c = dom fc; A7: d = dom fd by A4,XTUPLE_0:1; then cod id d = dom fd; hence f(*)[id c,id d] = [fc(*)id c,fd(*)id d] by A3,A6,Th23 .= [fc,fd(*)id d] by A5,CAT_1:22 .= f by A3,A7,CAT_1:22; end; assume A8: Hom(b,[c,d]) <> {}; let f be Morphism of b,[c,d]; consider fc being (Morphism of C), fd being Morphism of D such that A9: f = [fc,fd] by DOMAIN_1:1; A10: [c,d] = cod f by A8,CAT_1:5 .= [cod fc,cod fd] by A9,Th22; then A11: c = cod fc by XTUPLE_0:1; then A12: dom id c = cod fc; A13: d = cod fd by A10,XTUPLE_0:1; then dom id d = cod fd; hence [id c,id d](*)f = [(id c)(*)fc,(id d)(*)fd] by A9,A12,Th23 .= [fc,(id d)(*)fd] by A11,CAT_1:21 .= f by A9,A13,CAT_1:21; end; then m = id[c,d] by CAT_1:def 12; hence thesis; end; theorem for c,c9 being Object of C, d,d9 being Object of D holds Hom([c,d],[c9,d9]) = [:Hom(c,c9),Hom(d,d9):] proof let c,c9 be Object of C, d,d9 be Object of D; now let x be object; thus x in Hom([c,d],[c9,d9]) implies x in [:Hom(c,c9),Hom(d,d9):] proof assume A1: x in Hom([c,d],[c9,d9]); then reconsider fg = x as Morphism of [c,d],[c9,d9] by CAT_1:def 5; A2: dom fg = [c,d] by A1,CAT_1:1; A3: cod fg = [c9,d9] by A1,CAT_1:1; consider x1,x2 being object such that A4: x1 in the carrier' of C and A5: x2 in the carrier' of D and A6: fg = [x1,x2] by ZFMISC_1:def 2; reconsider g = x2 as Morphism of D by A5; reconsider f = x1 as Morphism of C by A4; A7: cod fg = [cod f,cod g] by A6,Th22; then A8: cod f = c9 by A3,XTUPLE_0:1; A9: cod g = d9 by A3,A7,XTUPLE_0:1; A10: dom fg = [dom f,dom g] by A6,Th22; then dom g = d by A2,XTUPLE_0:1; then A11: g in Hom(d,d9) by A9; dom f = c by A2,A10,XTUPLE_0:1; then f in Hom(c,c9) by A8; hence thesis by A6,A11,ZFMISC_1:87; end; assume x in [:Hom(c,c9),Hom(d,d9):]; then consider x1,x2 being object such that A12: x1 in Hom(c,c9) and A13: x2 in Hom(d,d9) and A14: x = [x1,x2] by ZFMISC_1:def 2; reconsider g = x2 as Morphism of d,d9 by A13,CAT_1:def 5; reconsider f = x1 as Morphism of c,c9 by A12,CAT_1:def 5; cod f = c9 & cod g = d9 by A12,A13,CAT_1:1; then A15: cod [f,g] = [c9,d9] by Th22; dom f = c & dom g = d by A12,A13,CAT_1:1; then dom [f,g] = [c,d] by Th22; hence x in Hom([c,d],[c9,d9]) by A14,A15; end; hence thesis by TARSKI:2; end; theorem for c,c9 being Object of C, f being Morphism of c,c9, d,d9 being Object of D, g being Morphism of d,d9 st Hom(c,c9) <> {} & Hom(d,d9) <> {} holds [f,g] is Morphism of [c,d],[c9,d9] proof let c,c9 be Object of C, f be Morphism of c,c9, d,d9 be Object of D, g be Morphism of d,d9; assume A1: Hom(c,c9) <> {} & Hom(d,d9) <> {}; then cod f = c9 & cod g = d9 by CAT_1:5; then A2: cod [f,g] = [c9,d9] by Th22; dom f = c & dom g = d by A1,CAT_1:5; then dom [f,g] = [c,d] by Th22; hence thesis by A2,CAT_1:4; end; :: Bifunctors definition let C,C9,D; let S being Functor of [:C,C9:],D; let m be Morphism of C; let m9 be Morphism of C9; redefine func S.(m,m9) -> Morphism of D; coherence proof S.(m,m9) = S.[m,m9]; hence thesis; end; end; theorem Th28: for S being Functor of [:C,C9:],D, c being Object of C holds ( curry S).(id c) is Functor of C9,D proof let S be Functor of [:C,C9:],D, c be Object of C; reconsider S9 = S as Function of [:the carrier' of C,the carrier' of C9:], the carrier' of D; reconsider T = (curry S9).(id c) as Function of the carrier' of C9,the carrier' of D; now thus for c9 being Object of C9 ex d being Object of D st T.(id c9) = id d proof let c9 be Object of C9; consider d being Object of D such that A1: S.(id [c,c9]) = id d by CAT_1:62; take d; thus T.(id c9) = S.(id c,id c9) by FUNCT_5:69 .= id d by A1,Th25; end; A2: dom id c = c & cod id c = c; thus for f being Morphism of C9 holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f) proof let f be Morphism of C9; thus T.(id dom f) = S.(id c,id dom f) by FUNCT_5:69 .= S.(id [c,dom f]) by Th25 .= S.(id [dom id c,dom f]) .= S.(id dom [id c,f]) by Th22 .= id dom (S.(id c,f)) by CAT_1:63 .= id dom (T.f) by FUNCT_5:69; thus T.(id cod f) = S.(id c,id cod f) by FUNCT_5:69 .= S.(id [c,cod f]) by Th25 .= S.(id [cod id c,cod f]) .= S.(id cod [id c,f]) by Th22 .= id cod (S.(id c,f)) by CAT_1:63 .= id cod (T.f) by FUNCT_5:69; end; let f,g be Morphism of C9 such that A3: dom g = cod f; Hom(c,c) <> {}; then A4: (id c)*(id c) = (id c)(*)(id c) by CAT_1:def 13; A5: dom [id c,g] = [dom id c,dom g] & cod [id c,f] = [cod id c, cod f] by Th22; thus T.(g(*)f) = S.((id c)*(id c),g(*)f) by FUNCT_5:69 .= S.([id c,g](*)[id c,f]) by A3,A2,A4,Th23 .= (S.(id c,g))(*)(S.(id c,f)) by A3,A5,CAT_1:64 .= (T.g)(*)(S.(id c,f)) by FUNCT_5:69 .= (T.g)(*)(T.f) by FUNCT_5:69; end; hence thesis by CAT_1:61; end; theorem Th29: for S being Functor of [:C,C9:],D, c9 being Object of C9 holds ( curry' S).(id c9) is Functor of C,D proof let S be Functor of [:C,C9:],D, c9 be Object of C9; reconsider S9 = S as Function of [:the carrier' of C,the carrier' of C9:], the carrier' of D; reconsider T = (curry' S9).(id c9) as Function of the carrier' of C,the carrier' of D; now thus for c being Object of C ex d being Object of D st T.(id c) = id d proof let c be Object of C; consider d being Object of D such that A1: S.(id [c,c9]) = id d by CAT_1:62; take d; thus T.(id c) = S.(id c,id c9) by FUNCT_5:70 .= id d by A1,Th25; end; A2: dom id c9 = c9 & cod id c9 = c9; thus for f being Morphism of C holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f) proof let f be Morphism of C; thus T.(id dom f) = S.(id dom f,id c9) by FUNCT_5:70 .= S.(id [dom f,c9]) by Th25 .= S.(id [dom f,dom id c9]) .= S.(id dom [f,id c9]) by Th22 .= id dom (S.(f,id c9)) by CAT_1:63 .= id dom (T.f) by FUNCT_5:70; thus T.(id cod f) = S.(id cod f,id c9) by FUNCT_5:70 .= S.(id [cod f,c9]) by Th25 .= S.(id [cod f,cod id c9]) .= S.(id cod [f,id c9]) by Th22 .= id cod (S.(f,id c9)) by CAT_1:63 .= id cod (T.f) by FUNCT_5:70; end; let f,g be Morphism of C such that A3: dom g = cod f; Hom(c9,c9) <> {}; then A4: (id c9)*(id c9) = (id c9)(*)(id c9) by CAT_1:def 13; A5: dom [g,id c9] = [dom g,dom id c9] & cod [f,id c9] = [cod f,cod id c9] by Th22; thus T.(g(*)f) = S.(g(*)f,(id c9)*(id c9)) by FUNCT_5:70 .= S.([g,id c9](*)[f,id c9]) by A3,A2,A4,Th23 .= (S.(g,id c9))(*)(S.(f,id c9)) by A3,A5,CAT_1:64 .= (T.g)(*)(S.(f,id c9)) by FUNCT_5:70 .= (T.g)(*)(T.f) by FUNCT_5:70; end; hence thesis by CAT_1:61; end; :: Partial Functors definition let C,C9,D; let S be Functor of [:C,C9:],D, c be Object of C; func S?-c -> Functor of C9,D equals (curry S).(id c); coherence by Th28; end; theorem for S being Functor of [:C,C9:],D, c being Object of C, f being Morphism of C9 holds (S?-c).f = S.(id c,f) by FUNCT_5:69; theorem for S being Functor of [:C,C9:],D, c being Object of C, c9 being Object of C9 holds (Obj S?-c).c9 = (Obj S).(c,c9) proof let S be Functor of [:C,C9:],D, c be Object of C, c9 be Object of C9; (S?-c).(id c9) = S.(id c,id c9) by FUNCT_5:69 .= S.(id [c,c9]) by Th25 .= id ((Obj S).[c,c9]) by CAT_1:68; hence thesis by CAT_1:67; end; definition let C,C9,D; let S be Functor of [:C,C9:],D, c9 be Object of C9; func S-?c9 -> Functor of C,D equals (curry' S).(id c9); coherence by Th29; end; theorem for S being Functor of [:C,C9:],D, c9 being Object of C9, f being Morphism of C holds (S-?c9).f = S.(f,id c9) by FUNCT_5:70; theorem for S being Functor of [:C,C9:],D, c being Object of C, c9 being Object of C9 holds (Obj S-?c9).c = (Obj S).(c,c9) proof let S be Functor of [:C,C9:],D, c be Object of C, c9 be Object of C9; (S-?c9).(id c) = S.(id c,id c9) by FUNCT_5:70 .= S.(id [c,c9]) by Th25 .= id ((Obj S).[c,c9]) by CAT_1:68; hence thesis by CAT_1:67; end; theorem for L being Function of the carrier of C,Funct(B,D), M being Function of the carrier of B,Funct(C,D) st ( for c being Object of C,b being Object of B holds (M.b).(id c) = (L.c).(id b) ) & ( for f being Morphism of B for g being Morphism of C holds ((M.(cod f)).g)(*)((L.(dom g)).f) = ((L.(cod g)).f)(*)((M.(dom f)).g) ) ex S being Functor of [:B,C:],D st for f being Morphism of B for g being Morphism of C holds S.(f,g) = ((L.(cod g)).f)(*)((M.(dom f)).g) proof deffunc Mor(Category) = the carrier' of $1; let L be Function of the carrier of C,Funct(B,D), M be Function of the carrier of B,Funct(C,D) such that A1: for c being Object of C, b being Object of B holds (M.b).(id c) = (L .c).(id b) and A2: for f being Morphism of B for g being Morphism of C holds ((M.(cod f )).g)(*)((L.(dom g)).f) = ((L.(cod g)).f)(*)((M.(dom f)).g); deffunc F(Element of Mor(B), Element of Mor(C)) = ((L.(cod $2)).$1)(*)((M.(dom $1)).$2); consider S being Function of [:Mor(B),Mor(C):],Mor(D) such that A3: for f being Morphism of B for g being Morphism of C holds S.(f,g) = F(f,g) from BINOP_1:sch 4; reconsider T = S as Function of Mor([:B,C:]),Mor(D); now thus for bc being Object of [:B,C:] ex d being Object of D st T.(id bc) = id d proof let bc be Object of [:B,C:]; consider b being Object of B, c being Object of C such that A4: bc = [b,c] by DOMAIN_1:1; consider d being Object of D such that A5: (L.c).(id b) = id d by CAT_1:62; take d; Hom(d,d) <> {}; then A6: (id d)*(id d) = (id d)(*)(id d) by CAT_1:def 13; A7: cod id c = c & dom id b = b; (L.c).(id b) = (M.b).(id c) by A1; then T.(id b,id c) = id d by A3,A5,A6,A7; hence thesis by A4,Th25; end; thus for fg being Morphism of [:B,C:] holds T.(id dom fg) = id dom (T.fg) & T.(id cod fg) = id cod (T.fg) proof let fg be Morphism of [:B,C:]; consider f being (Morphism of B), g being Morphism of C such that A8: fg = [f,g] by DOMAIN_1:1; set b = dom f, c = dom g; set g9 = id c, f9= id b; A9: Hom(dom ((M.b).g),dom ((M.b).g)) <> {}; id dom ((L.(cod g)).f) = (L.(cod g)).(id dom f) by CAT_1:63 .= (M.(dom f)).(id cod g) by A1 .= id cod ((M.(dom f)).g) by CAT_1:63; then A10: dom ((L.(cod g)).f) = cod ((M.(dom f)).g) by CAT_1:59; thus T.(id (dom fg)) = S.(id [b,c]) by A8,Th22 .= S.(id b,id c) by Th25 .= ((L.(cod g9)).f9)(*)((M.(dom f9)).g9) by A3 .= ((L.c).f9)(*)((M.(dom f9)).g9) .= ((L.c).f9)(*)((M.b).g9) .= ((M.b).g9)(*)((M.b).g9) by A1 .= (id dom ((M.b).g))(*)((M.b).g9) by CAT_1:63 .= (id dom ((M.b).g))(*)(id dom((M.b).g)) by CAT_1:63 .= (id dom ((M.b).g))*(id dom((M.b).g)) by A9,CAT_1:def 13 .= id dom (((L.(cod g)).f)(*)((M.(dom f)).g)) by A10,CAT_1:17 .= id dom (S.(f,g)) by A3 .= id dom(T.fg) by A8; set b = cod f, c = cod g; set g9 = id c, f9= id b; A11: Hom(cod ((L.c).f),cod ((L.c).f)) <> {}; thus T.(id (cod fg)) = S.(id [b,c]) by A8,Th22 .= S.(id b,id c) by Th25 .= ((L.(cod g9)).f9)(*)((M.(dom f9)).g9) by A3 .= ((L.c).f9)(*)((M.(dom f9)).g9) .= ((L.c).f9)(*)((M.(cod f)).g9) .= ((L.c).f9)(*)((L.c).f9) by A1 .= (id cod (((L.c).f))(*)((L.c).f9)) by CAT_1:63 .= (id cod ((L.c).f))(*)(id cod((L.c).f)) by CAT_1:63 .= (id cod ((L.c).f))*(id cod ((L.c).f)) by A11,CAT_1:def 13 .= id cod (((L.(cod g)).f)(*)((M.(dom f)).g)) by A10,CAT_1:17 .= id cod (S.(f,g)) by A3 .= id cod (T.fg) by A8; end; let fg1,fg2 be Morphism of [:B,C:] such that A12: dom fg2 = cod fg1; consider f1 being (Morphism of B), g1 being Morphism of C such that A13: fg1 = [f1,g1] by DOMAIN_1:1; consider f2 being (Morphism of B), g2 being Morphism of C such that A14: fg2 = [f2,g2] by DOMAIN_1:1; A15: [cod f1,cod g1] = cod fg1 by A13,Th22; set L1 = L.(cod g1), L2 = L.(cod g2), M1 = M.(dom f1), M2 = M.(dom f2); A16: [dom f2,dom g2] = dom fg2 by A14,Th22; then A17: dom f2 = cod f1 by A12,A15,XTUPLE_0:1; then A18: dom(L2.f2) = cod (L2.f1) by CAT_1:64; id dom (L1.f1) = L1.(id dom f1) by CAT_1:63 .= M1.(id cod g1) by A1 .= id cod (M1.g1) by CAT_1:63; then A19: dom (L1.f1) = cod (M1.g1) by CAT_1:59; then A20: cod ((L1.f1)(*)(M1.g1)) = cod (L1.f1) by CAT_1:17; A21: dom g2 = cod g1 by A12,A16,A15,XTUPLE_0:1; then A22: dom(M1.g2) = cod (M1.g1) by CAT_1:64; then A23: cod ((M1.g2)(*)(M1.g1)) = cod(M1.g2) by CAT_1:17; id dom (M2.g2) = M2.(id dom g2) by CAT_1:63 .= L1.(id cod f1) by A1,A17,A21 .= id cod (L1.f1) by CAT_1:63; then A24: dom (M2.g2) = cod(L1.f1) by CAT_1:59; id dom (L2.f2) = L2.(id dom f2) by CAT_1:63 .= M2.(id cod g2) by A1 .= id cod (M2.g2) by CAT_1:63; then A25: dom (L2.f2) = cod (M2.g2) by CAT_1:59; set f = f2(*)f1, g = g2(*)g1; id dom (L2.f1) = L2.(id dom f1) by CAT_1:63 .= M1.(id cod g2) by A1 .= id cod (M1.g2) by CAT_1:63; then A26: dom (L2.f1) = cod (M1.g2) by CAT_1:59; thus T.(fg2(*)fg1) = S.(f,g) by A12,A13,A14,Th24 .= ((L.(cod g)).f)(*)((M.(dom f)).g) by A3 .= ((L.(cod g2)).f)(*)((M.(dom f)).g) by A21,CAT_1:17 .= ((L.(cod g2)).f)(*)((M.(dom f1)).g) by A17,CAT_1:17 .= ((L2.f2)(*)(L2.f1))(*)(M1.g) by A17,CAT_1:64 .= ((L2.f2)(*)(L2.f1))(*)((M1.g2)(*)(M1.g1)) by A21,CAT_1:64 .= (L2.f2)(*)((L2.f1)(*)((M1.g2)(*)(M1.g1))) by A18,A23,A26,CAT_1:18 .= (L2.f2)(*)(((L2.f1)(*)(M1.g2))(*)(M1.g1)) by A22,A26,CAT_1:18 .= (L2.f2)(*)(((M2.g2)(*)(L1.f1))(*)(M1.g1)) by A2,A17,A21 .= (L2.f2)(*)((M2.g2)(*)((L1.f1)(*)(M1.g1))) by A19,A24,CAT_1:18 .= ((L2.f2)(*)(M2.g2))(*)((L1.f1)(*)(M1.g1)) by A24,A25,A20,CAT_1:18 .= ((L2.f2)(*)(M2.g2))(*)(S.(f1,g1)) by A3 .= (S.(f2,g2))(*)(T.fg1) by A3,A13 .= (T.fg2)(*)(T.fg1) by A14; end; then reconsider T as Functor of [:B,C:],D by CAT_1:61; take T; thus thesis by A3; end; theorem for L being Function of the carrier of C,Funct(B,D), M being Function of the carrier of B,Funct(C,D) st ex S being Functor of [:B,C:],D st for c being Object of C,b being Object of B holds S-?c = L.c & S?-b = M.b for f being Morphism of B for g being Morphism of C holds ((M.(cod f)).g)(*)((L.(dom g)).f) = ((L.(cod g)).f)(*)((M.(dom f)).g) proof let L be Function of the carrier of C,Funct(B,D), M be Function of the carrier of B,Funct(C,D); given S be Functor of [:B,C:],D such that A1: for c being Object of C, b being Object of B holds S-?c = L.c & S?-b = M.b; let f be Morphism of B; let g be Morphism of C; dom id cod f = cod f; then A2: dom [id cod f,g] = [cod f,dom g] by Th22; cod id dom g = dom g; then A3: cod [f,id dom g] = [cod f, dom g] by Th22; cod id dom f = dom f; then A4: cod [id dom f,g] = [dom f,cod g] by Th22; dom id cod g = cod g; then A5: dom [f,id cod g] = [dom f,cod g] by Th22; thus ((M.(cod f)).g)(*)((L.(dom g)).f) = ((S?-(cod f)).g)(*)((L.(dom g)).f) by A1 .= ((S?-(cod f)).g)(*)((S-?(dom g)).f) by A1 .= (S.(id cod f,g))(*)((S-?(dom g)).f) by FUNCT_5:69 .= (S.(id cod f,g))(*)(S.(f,id dom g)) by FUNCT_5:70 .= S.([id cod f,g](*)[f,id dom g]) by A2,A3,CAT_1:64 .= S.[(id cod f)(*)f,g(*)(id dom g)] by A2,A3,Th24 .= S.[f,g(*)(id dom g)] by CAT_1:21 .= S.[f,g] by CAT_1:22 .= S.[f(*)(id dom f),g] by CAT_1:22 .= S.[f(*)(id dom f),(id cod g)(*)g ] by CAT_1:21 .= S.([f,id cod g](*)[id dom f,g]) by A5,A4,Th24 .= (S.(f,id cod g))(*)(S.[id dom f,g]) by A5,A4,CAT_1:64 .= ((S-?(cod g)).f)(*)(S.(id dom f,g)) by FUNCT_5:70 .= ((S-?(cod g)).f)(*)((S?-(dom f)).g) by FUNCT_5:69 .= ((L.(cod g)).f)(*)((S?-(dom f)).g) by A1 .= ((L.(cod g)).f)(*)((M.(dom f)).g) by A1; end; definition let C,D; func pr1(C,D) -> Functor of [:C,D:],C equals pr1(the carrier' of C,the carrier' of D); coherence proof reconsider T = pr1(the carrier' of C,the carrier' of D) as Function of the carrier' of [:C,D:],the carrier' of C; now thus for cd being Object of [:C,D:] ex c being Object of C st T.(id cd) = id c proof let cd be Object of [:C,D:]; consider c being Object of C,d being Object of D such that A1: cd = [c,d] by DOMAIN_1:1; A2: T.(id c,id d) = id c by FUNCT_3:def 4; id cd = [id c,id d] by A1,Th25; hence thesis by A2; end; thus for fg being Morphism of [:C,D:] holds T.(id dom fg) = id dom (T.fg) & T.(id cod fg) = id cod (T.fg) proof let fg be Morphism of [:C,D:]; consider f being (Morphism of C), g being Morphism of D such that A3: fg = [f,g] by DOMAIN_1:1; T.(f,g) = T.fg by A3; then A4: T.fg = f by FUNCT_3:def 4; dom [f,g] = [dom f,dom g] by Th22; hence T.(id dom fg) = T.(id dom f,id dom g) by A3,Th25 .= id dom(T.fg) by A4,FUNCT_3:def 4; cod [f,g] = [cod f,cod g] by Th22; hence T.(id cod fg) = T.(id cod f,id cod g) by A3,Th25 .= id cod(T.fg) by A4,FUNCT_3:def 4; end; let fg,fg9 be Morphism of [:C,D:] such that A5: dom fg9 = cod fg; consider f being (Morphism of C), g being Morphism of D such that A6: fg = [f,g] by DOMAIN_1:1; T.(f,g) = T.fg by A6; then A7: T.fg = f by FUNCT_3:def 4; consider f9 being (Morphism of C), g9 being Morphism of D such that A8: fg9 = [f9,g9] by DOMAIN_1:1; T.(f9,g9) = T.fg9 by A8; then A9: T.fg9 = f9 by FUNCT_3:def 4; dom [f9,g9] = [dom f9,dom g9] & cod [f,g] = [cod f,cod g] by Th22; then dom f9 = cod f & dom g9 = cod g by A5,A6,A8,XTUPLE_0:1; hence T.(fg9(*)fg) = T.(f9(*)f,g9(*)g) by A6,A8,Th23 .= (T.fg9)(*)(T.fg) by A9,A7,FUNCT_3:def 4; end; hence thesis by CAT_1:61; end; func pr2(C,D) -> Functor of [:C,D:],D equals pr2(the carrier' of C,the carrier' of D); coherence proof reconsider T = pr2(the carrier' of C,the carrier' of D) as Function of the carrier' of [:C,D:],the carrier' of D; now thus for cd being Object of [:C,D:] ex d being Object of D st T.(id cd) = id d proof let cd be Object of [:C,D:]; consider c being Object of C,d being Object of D such that A10: cd = [c,d] by DOMAIN_1:1; A11: T.(id c,id d) = id d by FUNCT_3:def 5; id cd = [id c,id d] by A10,Th25; hence thesis by A11; end; thus for fg being Morphism of [:C,D:] holds T.(id dom fg) = id dom (T.fg) & T.(id cod fg) = id cod (T.fg) proof let fg be Morphism of [:C,D:]; consider f being (Morphism of C), g being Morphism of D such that A12: fg = [f,g] by DOMAIN_1:1; T.(f,g) = T.fg by A12; then A13: T.fg = g by FUNCT_3:def 5; dom [f,g] = [dom f,dom g] by Th22; hence T.(id dom fg) = T.(id dom f,id dom g) by A12,Th25 .= id dom(T.fg) by A13,FUNCT_3:def 5; cod [f,g] = [cod f,cod g] by Th22; hence T.(id cod fg) = T.(id cod f,id cod g) by A12,Th25 .= id cod(T.fg) by A13,FUNCT_3:def 5; end; let fg,fg9 be Morphism of [:C,D:] such that A14: dom fg9 = cod fg; consider f being (Morphism of C), g being Morphism of D such that A15: fg = [f,g] by DOMAIN_1:1; T.(f,g) = T.fg by A15; then A16: T.fg = g by FUNCT_3:def 5; consider f9 being (Morphism of C), g9 being Morphism of D such that A17: fg9 = [f9,g9] by DOMAIN_1:1; T.(f9,g9) = T.fg9 by A17; then A18: T.fg9 = g9 by FUNCT_3:def 5; dom [f9,g9] = [dom f9,dom g9] & cod [f,g] = [cod f,cod g] by Th22; then dom f9 = cod f & dom g9 = cod g by A14,A15,A17,XTUPLE_0:1; hence T.(fg9(*)fg) = T.(f9(*)f,g9(*)g) by A15,A17,Th23 .= (T.fg9)(*)(T.fg) by A18,A16,FUNCT_3:def 5; end; hence thesis by CAT_1:61; end; end; ::$CT 2 theorem for c being Object of C, d being Object of D holds (Obj pr1(C,D)).(c,d ) = c proof let c be Object of C, d be Object of D; id [c,d] = [id c,id d] & (pr1(C,D)).(id c,id d) = id c by Th25,FUNCT_3:def 4; hence thesis by CAT_1:67; end; theorem for c being Object of C, d being Object of D holds (Obj pr2(C,D)).(c,d ) = d proof let c be Object of C, d be Object of D; id [c,d] = [id c,id d] & (pr2(C,D)).(id c,id d) = id d by Th25,FUNCT_3:def 5; hence thesis by CAT_1:67; end; definition let C,D,D9; let T be Functor of C,D, T9 be Functor of C,D9; redefine func <:T,T9:> -> Functor of C,[:D,D9:]; coherence proof reconsider S = <:T,T9:> as Function of the carrier' of C,the carrier' of [:D,D9:]; now thus for c being Object of C ex dd9 being Object of [:D,D9:] st S.(id c) = id dd9 proof let c be Object of C; set d = (Obj T).c, d9 = (Obj T9).c; take dd9 = [d,d9]; thus S.(id c) = [T.(id c),T9.(id c)] by FUNCT_3:59 .= [id d,T9.(id c)] by CAT_1:68 .= [id d,id d9] by CAT_1:68 .= id dd9 by Th25; end; thus for f being Morphism of C holds S.(id dom f) = id dom (S.f) & S.(id cod f) = id cod (S.f) proof let f be Morphism of C; T.(id dom f) = id(dom(T.f)) & T9.(id dom f) = id(dom(T9.f)) by CAT_1:63; hence S.(id dom f) = [id(dom(T.f)),id(dom(T9.f))] by FUNCT_3:59 .= id [dom(T.f),dom(T9.f)] by Th25 .= id dom[T.f,T9.f] by Th22 .= id dom (S.f) by FUNCT_3:59; T.(id cod f) = id(cod(T.f)) & T9.(id cod f) = id(cod(T9.f)) by CAT_1:63; hence S.(id cod f) = [id(cod(T.f)),id(cod(T9.f))] by FUNCT_3:59 .= id [cod(T.f),cod(T9.f)] by Th25 .= id cod [T.f,T9.f] by Th22 .= id cod (S.f) by FUNCT_3:59; end; let f,g be Morphism of C; assume A1: dom g = cod f; then A2: dom(T.g) = cod(T.f) & dom(T9.g) = cod(T9.f) by CAT_1:64; T.(g(*)f) = (T.g)(*)(T.f) & T9.(g(*)f) = (T9.g)(*)(T9.f) by A1,CAT_1:64; hence S.(g(*)f) = [(T.g)(*)(T.f),(T9.g)(*)(T9.f)] by FUNCT_3:59 .= [T.g,T9.g](*)[T.f,T9.f] by A2,Th23 .= (S.g)(*)[T.f,T9.f] by FUNCT_3:59 .= (S.g)(*)(S.f) by FUNCT_3:59; end; hence thesis by CAT_1:61; end; end; ::$CT theorem for T being Functor of C,D, T9 being Functor of C,D9, c being Object of C holds (Obj <:T,T9:>).c = [(Obj T).c,(Obj T9).c] proof let T be Functor of C,D, T9 be Functor of C,D9, c be Object of C; A1: T.(id c) = id((Obj T).c) & T9.(id c) = id((Obj T9).c) by CAT_1:68; <:T,T9:>.(id c) = [T.(id c),T9.(id c)] & [id((Obj T).c),id((Obj T9).c)] = id [(Obj T).c,(Obj T9).c] by Th25,FUNCT_3:59; hence thesis by A1,CAT_1:67; end; theorem Th39: for T being Functor of C,D, T9 being Functor of C9,D9 holds [:T, T9:] = <:T*pr1(C,C9),T9*pr2(C,C9):> proof let T be Functor of C,D, T9 be Functor of C9,D9; dom T = the carrier' of C & dom T9 = the carrier' of C9 by FUNCT_2:def 1; hence thesis by FUNCT_3:66; end; definition let C,C9,D,D9; let T be Functor of C,D, T9 be Functor of C9,D9; redefine func [:T,T9:] -> Functor of [:C,C9:],[:D,D9:]; coherence proof [:T,T9:] = <:T*pr1(C,C9),T9*pr2(C,C9):> by Th39; hence thesis; end; end; ::$CT theorem for T being Functor of C,D, T9 being Functor of C9,D9, c being Object of C, c9 being Object of C9 holds (Obj [:T,T9:]).(c,c9) = [(Obj T).c,(Obj T9). c9] proof let T be Functor of C,D, T9 be Functor of C9,D9; let c be Object of C, c9 be Object of C9; A1: T.(id c) = id((Obj T).c) & T9.(id c9) = id((Obj T9).c9) by CAT_1:68; A2: [id((Obj T).c),id((Obj T9).c9)] = id [(Obj T).c,(Obj T9).c9] by Th25; [:T,T9:].(id c,id c9) = [T.(id c),T9.(id c9)] & [id c,id c9] = id [c,c9] by Th25,FUNCT_3:75; hence thesis by A1,A2,CAT_1:67; end;