:: Categorical Pullbacks :: by Marco Riccardi :: :: Received December 31, 2014 :: Copyright (c) 2014-2021 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 FUNCT_1, TARSKI, ZFMISC_1, XBOOLE_0, RELAT_1, SUBSET_1, WELLORD1, CAT_1, ALTCAT_1, GRAPH_1, BINOP_1, STRUCT_0, PARTFUN1, MONOID_0, NATTRA_1, MSSUBFAM, NUMBERS, ORDINAL1, CARD_1, FUNCTOR0, MOD_4, CAT_6, XTUPLE_0, RECDEF_2, MCART_1, CAT_3, PBOOLE, WELLORD2, FACIRC_1, FUNCT_2, ALTCAT_2, CAT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_3, FUNCT_4, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, PARTFUN1, FINSEQ_1, STRUCT_0, FUNCOP_1, RELSET_1, BINOP_1, GRAPH_1, CAT_1, CAT_2, NUMBERS, NAT_1, XXREAL_0, XTUPLE_0, ALG_1, XCMPLX_0, WELLORD2, CARD_1, CAT_6, ENUMSET1, WELLORD1; constructors NUMBERS, FUNCT_2, CLASSES2, FINSEQ_1, FUNCOP_1, RELAT_2, PARTFUN1, RELSET_1, BINOP_1, FUNCT_4, CAT_1, CAT_2, NAT_1, XXREAL_0, WELLORD2, XREAL_0, CARD_1, XCMPLX_0, INT_1, VALUED_0, ISOCAT_1, STRUCT_0, CAT_6, REALSET1, WELLORD1, ORDERS_2; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XTUPLE_0, CARD_1, STRUCT_0, RELSET_1, FUNCT_2, CARD_2, FINSET_1, NAT_1, WELLORD2, CAT_6; requirements SUBSET, BOOLE, NUMERALS; begin :: Preliminaries registration cluster ordinal -> non pair for set; end; registration let C be empty CategoryStr; cluster Mor(C) -> empty; end; registration let C be non empty CategoryStr; cluster Mor(C) -> non empty; end; registration let C be empty with_identities CategoryStr; cluster Ob(C) -> empty; end; registration let C be non empty with_identities CategoryStr; cluster Ob(C) -> non empty; end; registration let C be with_identities CategoryStr; let a be Object of C; cluster id- a -> identity; end; theorem :: CAT_7:1 for C being CategoryStr, f being morphism of C st C is non empty holds f in the carrier of C; theorem :: CAT_7:2 for C being with_identities CategoryStr, a being Object of C st C is non empty holds a in the carrier of C; theorem :: CAT_7:3 for C being composable CategoryStr, f1,f2,f3 being morphism of C st f1 |> f2 & f2 |> f3 & f2 is identity holds f1 |> f3; theorem :: CAT_7:4 for C being with_identities composable CategoryStr, f1,f2 being morphism of C st f1 |> f2 holds dom (f1 (*) f2) = dom f2 & cod (f1 (*) f2) = cod f1; theorem :: CAT_7:5 for C being non empty composable with_identities CategoryStr, f1,f2 being morphism of C holds f1 |> f2 iff dom f1 = cod f2; theorem :: CAT_7:6 for C being with_identities composable CategoryStr, f being morphism of C st f is identity holds dom f = f & cod f = f; theorem :: CAT_7:7 for C being composable with_identities CategoryStr, f1,f2 being morphism of C st f1 |> f2 & f1 is identity & f2 is identity holds f1 = f2; theorem :: CAT_7:8 for C being non empty composable with_identities CategoryStr, f1,f2 being morphism of C st dom f1 = f2 holds f1 |> f2 & f1 (*) f2 = f1; theorem :: CAT_7:9 for C being non empty composable with_identities CategoryStr, f1,f2 being morphism of C st f1 = cod f2 holds f1 |> f2 & f1 (*) f2 = f2; theorem :: CAT_7:10 for C1,C2,C3,C4 being category, F being Functor of C1,C2, G being Functor of C2,C3, H being Functor of C3,C4 st F is covariant & G is covariant & H is covariant holds H (*) (G (*) F) = (H (*) G) (*) F; theorem :: CAT_7:11 for C,D being category, F being Functor of C,D st F is covariant holds F (*) id C = F & id D (*) F = F; theorem :: CAT_7:12 for C,D being composable with_identities CategoryStr holds C ~= D iff ex F being Functor of C,D st F is covariant & F is bijective; theorem :: CAT_7:13 for C,D being empty with_identities CategoryStr holds C ~= D; theorem :: CAT_7:14 for C,D being with_identities CategoryStr st C ~= D holds card Mor C = card Mor D & card Ob C = card Ob D; theorem :: CAT_7:15 for C,D being with_identities CategoryStr st C ~= D & C is empty holds D is empty; begin :: Hom-sets definition let C be CategoryStr; let a,b be Object of C; func Hom(a,b) -> Subset of Mor C equals :: CAT_7:def 1 {f where f is morphism of C : ex f1,f2 being morphism of C st a = f1 & b = f2 & f |> f1 & f2 |> f}; end; definition let C be non empty composable with_identities CategoryStr; let a,b be Object of C; redefine func Hom(a,b) -> Subset of Mor(C) equals :: CAT_7:def 2 {f where f is morphism of C : dom f = a & cod f = b}; end; definition let C be CategoryStr; let a,b be Object of C; assume Hom(a,b) <> {}; mode Morphism of a,b -> morphism of C means :: CAT_7:def 3 it in Hom(a,b); end; definition let C be non empty with_identities CategoryStr; let a be Object of C; redefine func id- a -> Morphism of a, a; end; registration let C be non empty with_identities CategoryStr; let a be Object of C; cluster Hom(a,a) -> non empty; end; :: like CAT_1 definition let C be composable with_identities CategoryStr; let a,b,c be Object of C; let f be Morphism of a,b; let g be Morphism of b,c; assume Hom(a,b) <> {} & Hom(b,c) <> {}; func g * f -> Morphism of a,c equals :: CAT_7:def 4 g (*) f; end; theorem :: CAT_7:16 for C being CategoryStr, a,b being Object of C, f being Morphism of a,b st Hom(a,b) <> {} holds ex f1,f2 being morphism of C st a = f1 & b = f2 & f |> f1 & f2 |> f; theorem :: CAT_7:17 for C being composable with_identities CategoryStr, a,b,c being Object of C, f1 being Morphism of a,b, f2 being Morphism of b,c st Hom(a,b) <> {} & Hom(b,c) <> {} holds f2 |> f1; theorem :: CAT_7:18 for C being composable non empty with_identities CategoryStr, a,b being Object of C, f being Morphism of a,b st Hom(a,b) <> {} holds f * (id- a) = f & (id- b) * f = f; theorem :: CAT_7:19 for C being non empty with_identities composable CategoryStr, f being morphism of C holds f in Hom(dom f,cod f); theorem :: CAT_7:20 for C being non empty with_identities composable CategoryStr, a,b being Object of C, f being morphism of C holds f in Hom(a,b) iff dom f = a & cod f = b; theorem :: CAT_7:21 for C being non empty with_identities composable CategoryStr, a being Object of C holds a in Hom(a,a); theorem :: CAT_7:22 for C being composable with_identities CategoryStr, a,b,c being Object of C st Hom(a,b) <> {} & Hom(b,c) <> {} holds Hom(a,c) <> {}; theorem :: CAT_7:23 for C being category, a,b,c,d being Object of C, f1 being Morphism of a,b, f2 being Morphism of b,c, f3 being Morphism of c,d st Hom(a,b) <> {} & Hom(b,c) <> {} & Hom(c,d) <> {} holds f3 * (f2 * f1) = (f3 * f2) * f1; theorem :: CAT_7:24 for C being composable with_identities CategoryStr, a,b,c being Object of C, f1 being Morphism of a,b, f2 being Morphism of b,c st Hom(a,b) <> {} & Hom(b,c) <> {} holds (f1 is identity implies f2 * f1 = f2) & (f2 is identity implies f2 * f1 = f1); begin :: Monomorphisms, Epimorphisms and Isomorphisms definition let C be composable with_identities CategoryStr, a,b be Object of C, f be Morphism of a,b; attr f is monomorphism means :: CAT_7:def 5 Hom(a,b) <> {} & for c being Object of C st Hom(c,a) <> {} for g1,g2 being Morphism of c,a st f * g1 = f * g2 holds g1 = g2; attr f is epimorphism means :: CAT_7:def 6 Hom(a,b) <> {} & for c being Object of C st Hom(b,c) <> {} for g1,g2 being Morphism of b,c st g1 * f = g2 * f holds g1 = g2; end; theorem :: CAT_7:25 for C being composable with_identities CategoryStr, a,b being Object of C, f1 being Morphism of a,b st Hom(a,b) <> {} & f1 is identity holds f1 is monomorphism; theorem :: CAT_7:26 for C being category, a,b,c being Object of C, f1 being Morphism of a,b, f2 being Morphism of b,c st f1 is monomorphism & f2 is monomorphism holds f2 * f1 is monomorphism; theorem :: CAT_7:27 for C being category, a,b,c being Object of C, f1 being Morphism of a,b, f2 being Morphism of b,c st f2 * f1 is monomorphism & Hom(a,b) <> {} & Hom(b,c) <> {} holds f1 is monomorphism; definition let C be composable with_identities CategoryStr, a,b be Object of C, f be Morphism of a,b; attr f is section_ means :: CAT_7:def 7 Hom(a,b) <> {} & Hom(b,a) <> {} & ex g being Morphism of b,a st g * f = id- a; attr f is retraction means :: CAT_7:def 8 Hom(a,b) <> {} & Hom(b,a) <> {} & ex g being Morphism of b,a st f * g = id- b; end; theorem :: CAT_7:28 for C being non empty category, a,b being Object of C, f being Morphism of a,b st f is section_ holds f is monomorphism; theorem :: CAT_7:29 for C being composable with_identities CategoryStr, a,b being Object of C, f1 being Morphism of a,b st Hom(a,b) <> {} & f1 is identity holds f1 is epimorphism; theorem :: CAT_7:30 for C being category, a,b,c being Object of C, f1 being Morphism of a,b, f2 being Morphism of b,c st f1 is epimorphism & f2 is epimorphism holds f2 * f1 is epimorphism; theorem :: CAT_7:31 for C being category, a,b,c being Object of C, f1 being Morphism of a,b, f2 being Morphism of b,c st f2 * f1 is epimorphism & Hom(a,b) <> {} & Hom(b,c) <> {} holds f2 is epimorphism; theorem :: CAT_7:32 for C being non empty category, a,b being Object of C, f being Morphism of a,b st f is retraction holds f is epimorphism; definition let C be composable with_identities CategoryStr; let a,b be Object of C; let f be Morphism of a,b; attr f is isomorphism means :: CAT_7:def 9 Hom(a,b) <> {} & Hom(b,a) <> {} & ex g being Morphism of b,a st g * f = id- a & f * g = id- b; end; definition let C be composable with_identities CategoryStr; let a,b be Object of C; pred a,b are_isomorphic means :: CAT_7:def 10 ex f being Morphism of a,b st f is isomorphism; end; definition let C be composable with_identities CategoryStr; let a,b be Object of C; redefine pred a,b are_isomorphic means :: CAT_7:def 11 Hom(a,b) <> {} & Hom(b,a) <> {} & ex f being Morphism of a,b, g being Morphism of b,a st g * f = id- a & f * g = id- b; end; theorem :: CAT_7:33 for C being non empty category, a,b be Object of C, f being Morphism of a,b st f is isomorphism holds f is monomorphism & f is epimorphism; begin :: Ordinal Numbers as Categories definition let C be CategoryStr; attr C is preorder means :: CAT_7:def 12 for a,b being Object of C, f1,f2 being morphism of C holds f1 in Hom(a,b) & f2 in Hom(a,b) implies f1 = f2; end; registration cluster empty -> preorder for CategoryStr; end; registration cluster strict preorder for CategoryStr; end; registration cluster preorder -> associative for composable with_identities CategoryStr; end; definition let C be with_identities CategoryStr; func RelOb(C) -> Relation of Ob(C) equals :: CAT_7:def 13 {[a,b] where a,b is Object of C : ex f being morphism of C st f in Hom(a,b)}; end; registration let C be empty with_identities CategoryStr; cluster RelOb(C) -> empty; end; theorem :: CAT_7:34 for C being composable with_identities CategoryStr holds dom RelOb C = Ob C & rng RelOb C = Ob C; theorem :: CAT_7:35 for C1,C2 being composable with_identities CategoryStr st C1 ~= C2 holds RelOb(C1), RelOb(C2) are_isomorphic; registration let C be non empty composable with_identities CategoryStr; cluster RelOb C -> non empty; end; theorem :: CAT_7:36 for C being preorder composable with_identities CategoryStr st C is non empty holds ex F being Function of C, RelOb(C) st F is bijective & (for f being morphism of C holds F.f = [dom f,cod f]); theorem :: CAT_7:37 for O being ordinal number ex C being strict preorder category st Ob C = O & (for o1,o2 being Object of C st o1 in o2 holds Hom(o1,o2) = {[o1,o2]}) & RelOb C = RelIncl O & Mor C = O \/ {[o1,o2] where o1,o2 is Element of O: o1 in o2}; definition let O be ordinal number; let C be composable with_identities CategoryStr; attr C is O -ordered means :: CAT_7:def 14 RelOb(C), RelIncl(O) are_isomorphic; end; registration let O be non empty ordinal number; cluster O -ordered -> non empty for composable with_identities CategoryStr; end; registration let O be ordinal number; cluster strict O -ordered preorder for composable with_identities CategoryStr; end; registration let O be empty ordinal number; cluster O -ordered -> empty for composable with_identities CategoryStr; end; theorem :: CAT_7:38 for O1,O2 being ordinal number, C1 being O1 -ordered preorder category, C2 being O2 -ordered preorder category holds O1 = O2 iff C1 ~= C2; definition let O be ordinal number; func OrdC(O) -> strict O -ordered preorder category equals :: CAT_7:def 15 the strict O -ordered preorder category; end; theorem :: CAT_7:39 ex f being morphism of OrdC(2) st f is not identity & Ob OrdC 2 = {dom f, cod f} & Mor OrdC 2 = {dom f, cod f, f} & dom f, cod f, f are_mutually_distinct; definition let C be non empty category; let f be morphism of C; func MORPHISM(f) -> covariant Functor of OrdC 2, C means :: CAT_7:def 16 for g being morphism of OrdC 2 st g is not identity holds it.g = f; end; theorem :: CAT_7:40 for C being non empty category, f being morphism of C st f is identity holds for g being morphism of OrdC 2 holds (MORPHISM f).g = f; begin :: Pullbacks definition let C be category; let c,c1,c2,d be Object of C; let f1 be Morphism of c1,c such that Hom(c1,c) <> {}; let f2 be Morphism of c2,c such that Hom(c2,c) <> {}; let p1 be Morphism of d,c1 such that Hom(d,c1) <> {}; let p2 be Morphism of d,c2 such that Hom(d,c2) <> {}; pred d,p1,p2 is_pullback_of f1,f2 means :: CAT_7:def 17 f1 * p1 = f2 * p2 & for d1 being Object of C, g1 being Morphism of d1,c1, g2 being Morphism of d1,c2 st Hom(d1,c1) <> {} & Hom(d1,c2) <> {} & f1 * g1 = f2 * g2 holds Hom(d1,d) <> {} & ex h being Morphism of d1,d st p1 * h = g1 & p2 * h = g2 & for h1 being Morphism of d1,d st p1 * h1 = g1 & p2 * h1 = g2 holds h = h1; end; theorem :: CAT_7:41 for C being non empty category, c,c1,c2,d,e being Object of C, f1 being Morphism of c1,c, f2 being Morphism of c2,c, p1 being Morphism of d,c1, p2 being Morphism of d,c2, q1 being Morphism of e,c1, q2 being Morphism of e,c2 st Hom(c1,c) <> {} & Hom(c2,c) <> {} & Hom(d,c1) <> {} & Hom(d,c2) <> {} & Hom(e,c1) <> {} & Hom(e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds d,e are_isomorphic; theorem :: CAT_7:42 for C being category, c,c1,c2,d being Object of C, f1 being Morphism of c1,c, f2 being Morphism of c2,c, p1 being Morphism of d,c1, p2 being Morphism of d,c2 st Hom(c1,c) <> {} & Hom(c2,c) <> {} & Hom(d,c1) <> {} & Hom(d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 holds d,p2,p1 is_pullback_of f2,f1; theorem :: CAT_7:43 for C being category, c,c1,c2,d being Object of C, f1 being Morphism of c1,c, f2 being Morphism of c2,c, p1 being Morphism of d,c1, p2 being Morphism of d,c2 st Hom(c1,c) <> {} & Hom(c2,c) <> {} & Hom(d,c1) <> {} & Hom(d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & f1 is monomorphism holds p2 is monomorphism; theorem :: CAT_7:44 for C being non empty category, c,c1,c2,d being Object of C, f1 being Morphism of c1,c, f2 being Morphism of c2,c, p1 being Morphism of d,c1, p2 being Morphism of d,c2 st Hom(c1,c) <> {} & Hom(c2,c) <> {} & Hom(d,c1) <> {} & Hom(d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & f1 is isomorphism holds p2 is isomorphism; :: Pullback Lemma theorem :: CAT_7:45 for C being category, c1,c2,c3,c4,c5,c6 being Object of C, f1 being Morphism of c1,c2, f2 being Morphism of c2,c3, f3 being Morphism of c1,c4, f4 being Morphism of c2,c5, f5 being Morphism of c3,c6, f6 being Morphism of c4,c5, f7 being Morphism of c5,c6 st Hom(c1,c2) <> {} & Hom(c2,c3) <> {} & Hom(c1,c4) <> {} & Hom(c2,c5) <> {} & Hom(c3,c6) <> {} & Hom(c4,c5) <> {} & Hom(c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds c1,f1,f3 is_pullback_of f4,f6 iff c1,f2*f1,f3 is_pullback_of f5,f7*f6 & f4 * f1 = f6 * f3; begin :: Pullbacks of Functors definition let C,D be category; let F be Functor of C,D; attr F is monomorphism means :: CAT_7:def 18 F is covariant & for B being category, G1,G2 being Functor of B,C st G1 is covariant & G2 is covariant & F (*) G1 = F (*) G2 holds G1 = G2; attr F is isomorphism means :: CAT_7:def 19 F is covariant & ex G being Functor of D,C st G is covariant & G (*) F = id C & F (*) G = id D; end; definition let C,C1,C2,D be category; let F1 be Functor of C1,C such that F1 is covariant; let F2 be Functor of C2,C such that F2 is covariant; let P1 be Functor of D,C1 such that P1 is covariant; let P2 be Functor of D,C2 such that P2 is covariant; pred D,P1,P2 is_pullback_of F1,F2 means :: CAT_7:def 20 F1 (*) P1 = F2 (*) P2 & for D1 being category, G1 being Functor of D1,C1, G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds ex H being Functor of D1,D st H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds H = H1; end; theorem :: CAT_7:46 for C,C1,C2,D,E being category, F1 being Functor of C1,C, F2 being Functor of C2,C, P1 be Functor of D,C1, P2 be Functor of D,C2, Q1 be Functor of E,C1, Q2 be Functor of E,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & D,P1,P2 is_pullback_of F1,F2 & E,Q1,Q2 is_pullback_of F1,F2 holds D ~= E; theorem :: CAT_7:47 for C,C1,C2,D being category, F1 being Functor of C1,C, F2 being Functor of C2,C, P1 being Functor of D,C1, P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 holds D,P2,P1 is_pullback_of F2,F1; theorem :: CAT_7:48 for C,C1,C2,D being category, F1 being Functor of C1,C, F2 being Functor of C2,C, P1 being Functor of D,C1, P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is monomorphism holds P2 is monomorphism; theorem :: CAT_7:49 for C,C1,C2,D being category, F1 being Functor of C1,C, F2 being Functor of C2,C, P1 being Functor of D,C1, P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds P2 is isomorphism; theorem :: CAT_7:50 for C1,C2,C3,C4,C5,C6 being category, F1 being Functor of C1,C2, F2 being Functor of C2,C3, F3 being Functor of C1,C4, F4 being Functor of C2,C5, F5 being Functor of C3,C6, F6 being Functor of C4,C5, F7 being Functor of C5,C6 st F1 is covariant & F2 is covariant & F3 is covariant & F4 is covariant & F5 is covariant & F6 is covariant & F7 is covariant & C2,F2,F4 is_pullback_of F5,F7 holds C1,F1,F3 is_pullback_of F4,F6 iff C1,F2(*)F1,F3 is_pullback_of F5,F7(*)F6 & F4 (*) F1 = F6 (*) F3; theorem :: CAT_7:51 for C,C1,C2 being category, F1 being Functor of C1,C, F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds ex D being strict category, P1 being Functor of D,C1, P2 being Functor of D,C2 st the carrier of D = {[f1,f2] where f1 is morphism of C1, f2 is morphism of C2: f1 in the carrier of C1 & f2 in the carrier of C2 & F1.f1 = F2.f2} & the composition of D = {[[f1,f2],f3] where f1,f2,f3 is morphism of D: f1 in the carrier of D & f2 in the carrier of D & f3 in the carrier of D & for f11,f12,f13 being morphism of C1, f21,f22,f23 being morphism of C2 st f1 = [f11,f21] & f2 = [f12,f22] & f3 = [f13,f23] holds f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22} & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2; definition let C,C1,C2 be category; let F1 be Functor of C1,C such that F1 is covariant; let F2 be Functor of C2,C such that F2 is covariant; mode pullback of F1,F2 -> triple object means :: CAT_7:def 21 ex D being strict category, P1 being Functor of D,C1, P2 being Functor of D,C2 st it = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2; end; definition let C,C1,C2 be category; let F1 be Functor of C1,C such that F1 is covariant; let F2 be Functor of C2,C such that F2 is covariant; func [| F1, F2 |] -> strict category equals :: CAT_7:def 22 (the pullback of F1,F2)`1_3; end; definition let C,C1,C2 be category; let F1 be Functor of C1,C such that F1 is covariant; let F2 be Functor of C2,C such that F2 is covariant; func pr1(F1,F2) -> Functor of [|F1,F2|], C1 equals :: CAT_7:def 23 (the pullback of F1,F2)`2_3; func pr2(F1,F2) -> Functor of [|F1,F2|], C2 equals :: CAT_7:def 24 (the pullback of F1,F2)`3_3; end; theorem :: CAT_7:52 for C,C1,C2 being category, F1 being Functor of C1,C, F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds pr1(F1,F2) is covariant & pr2(F1,F2) is covariant & [|F1,F2|], pr1(F1,F2), pr2(F1,F2) is_pullback_of F1,F2; theorem :: CAT_7:53 for C,C1,C2 being category, F1 being Functor of C1,C, F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds [|F1,F2|] ~= [|F2,F1|]; theorem :: CAT_7:54 ex C,C1,C2 being Category, F1 being Functor of C1,C, F2 being Functor of C2,C st not ex D being Category, P1 being Functor of D,C1, P2 being Functor of D,C2 st F1 * P1 = F2 * P2 & for D1 being Category, G1 being Functor of D1,C1, G2 being Functor of D1,C2 st F1 * G1 = F2 * G2 holds ex H being Functor of D1,D st P1 * H = G1 & P2 * H = G2 & for H1 being Functor of D1,D st P1 * H1 = G1 & P2 * H1 = G2 holds H = H1;