:: NATTRA_1 semantic presentation begin definition let A1 be set ; let B1 be non empty set ; let f be Function of A1,B1; let Y1 be Subset of A1; :: original: | redefine funcf | Y1 -> Function of Y1,B1; coherence f | Y1 is Function of Y1,B1 by FUNCT_2:32; end; theorem Th1: :: NATTRA_1:1 for B1, B2, A1, A2 being non empty set for f being Function of A1,B1 for g being Function of A2,B2 for Y1 being non empty Subset of A1 for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):] proof let B1, B2, A1, A2 be non empty set ; ::_thesis: for f being Function of A1,B1 for g being Function of A2,B2 for Y1 being non empty Subset of A1 for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):] let f be Function of A1,B1; ::_thesis: for g being Function of A2,B2 for Y1 being non empty Subset of A1 for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):] let g be Function of A2,B2; ::_thesis: for Y1 being non empty Subset of A1 for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):] let Y1 be non empty Subset of A1; ::_thesis: for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):] let Y2 be non empty Subset of A2; ::_thesis: [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):] now__::_thesis:_for_a_being_Element_of_[:Y1,Y2:]_holds_[:(f_|_Y1),(g_|_Y2):]_._a_=_([:f,g:]_|_[:Y1,Y2:])_._a let a be Element of [:Y1,Y2:]; ::_thesis: [:(f | Y1),(g | Y2):] . a = ([:f,g:] | [:Y1,Y2:]) . a consider a1 being Element of Y1, a2 being Element of Y2 such that A1: a = [a1,a2] by DOMAIN_1:1; A2: (g | Y2) . a2 = g . a2 by FUNCT_1:49; A3: (f | Y1) . a1 = f . a1 by FUNCT_1:49; thus [:(f | Y1),(g | Y2):] . a = [:(f | Y1),(g | Y2):] . (a1,a2) by A1 .= [(f . a1),(g . a2)] by A3, A2, FUNCT_3:75 .= [:f,g:] . (a1,a2) by FUNCT_3:75 .= ([:f,g:] | [:Y1,Y2:]) . a by A1, FUNCT_1:49 ; ::_thesis: verum end; hence [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):] by FUNCT_2:63; ::_thesis: verum end; definition let A, B be non empty set ; let A1 be non empty Subset of A; let B1 be non empty Subset of B; let f be PartFunc of [:A1,A1:],A1; let g be PartFunc of [:B1,B1:],B1; :: original: |: redefine func|:f,g:| -> PartFunc of [:[:A1,B1:],[:A1,B1:]:],[:A1,B1:]; coherence |:f,g:| is PartFunc of [:[:A1,B1:],[:A1,B1:]:],[:A1,B1:] by FUNCT_4:59; end; theorem Th2: :: NATTRA_1:2 for A1, A2 being non empty set for Y1 being non empty Subset of A1 for Y2 being non empty Subset of A2 for f being PartFunc of [:A1,A1:],A1 for g being PartFunc of [:A2,A2:],A2 for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds |:F,G:| = |:f,g:| || [:Y1,Y2:] proof let A1, A2 be non empty set ; ::_thesis: for Y1 being non empty Subset of A1 for Y2 being non empty Subset of A2 for f being PartFunc of [:A1,A1:],A1 for g being PartFunc of [:A2,A2:],A2 for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds |:F,G:| = |:f,g:| || [:Y1,Y2:] let Y1 be non empty Subset of A1; ::_thesis: for Y2 being non empty Subset of A2 for f being PartFunc of [:A1,A1:],A1 for g being PartFunc of [:A2,A2:],A2 for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds |:F,G:| = |:f,g:| || [:Y1,Y2:] let Y2 be non empty Subset of A2; ::_thesis: for f being PartFunc of [:A1,A1:],A1 for g being PartFunc of [:A2,A2:],A2 for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds |:F,G:| = |:f,g:| || [:Y1,Y2:] let f be PartFunc of [:A1,A1:],A1; ::_thesis: for g being PartFunc of [:A2,A2:],A2 for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds |:F,G:| = |:f,g:| || [:Y1,Y2:] let g be PartFunc of [:A2,A2:],A2; ::_thesis: for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds |:F,G:| = |:f,g:| || [:Y1,Y2:] let F be PartFunc of [:Y1,Y1:],Y1; ::_thesis: ( F = f || Y1 implies for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds |:F,G:| = |:f,g:| || [:Y1,Y2:] ) assume A1: F = f || Y1 ; ::_thesis: for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds |:F,G:| = |:f,g:| || [:Y1,Y2:] A2: dom F c= dom f by A1, RELAT_1:60; let G be PartFunc of [:Y2,Y2:],Y2; ::_thesis: ( G = g || Y2 implies |:F,G:| = |:f,g:| || [:Y1,Y2:] ) assume A3: G = g || Y2 ; ::_thesis: |:F,G:| = |:f,g:| || [:Y1,Y2:] set X = dom |:F,G:|; A4: dom G c= dom g by A3, RELAT_1:60; A5: dom |:F,G:| = dom (|:f,g:| || [:Y1,Y2:]) proof thus dom |:F,G:| c= dom (|:f,g:| || [:Y1,Y2:]) :: according to XBOOLE_0:def_10 ::_thesis: dom (|:f,g:| || [:Y1,Y2:]) c= dom |:F,G:| proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom |:F,G:| or x in dom (|:f,g:| || [:Y1,Y2:]) ) assume x in dom |:F,G:| ; ::_thesis: x in dom (|:f,g:| || [:Y1,Y2:]) then consider x11, x21, x12, x22 being set such that A6: x = [[x11,x12],[x21,x22]] and A7: [x11,x21] in dom F and A8: [x12,x22] in dom G by FUNCT_4:def_3; A9: dom G c= [:Y2,Y2:] by A3, RELAT_1:58; then A10: x12 in Y2 by A8, ZFMISC_1:87; A11: x22 in Y2 by A8, A9, ZFMISC_1:87; A12: dom F c= [:Y1,Y1:] by A1, RELAT_1:58; then x21 in Y1 by A7, ZFMISC_1:87; then A13: [x21,x22] in [:Y1,Y2:] by A11, ZFMISC_1:87; x11 in Y1 by A7, A12, ZFMISC_1:87; then [x11,x12] in [:Y1,Y2:] by A10, ZFMISC_1:87; then A14: x in [:[:Y1,Y2:],[:Y1,Y2:]:] by A6, A13, ZFMISC_1:87; x in dom |:f,g:| by A2, A4, A6, A7, A8, FUNCT_4:def_3; then x in (dom |:f,g:|) /\ [:[:Y1,Y2:],[:Y1,Y2:]:] by A14, XBOOLE_0:def_4; hence x in dom (|:f,g:| || [:Y1,Y2:]) by RELAT_1:61; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (|:f,g:| || [:Y1,Y2:]) or x in dom |:F,G:| ) A15: dom F = (dom f) /\ [:Y1,Y1:] by A1, RELAT_1:61; assume x in dom (|:f,g:| || [:Y1,Y2:]) ; ::_thesis: x in dom |:F,G:| then A16: x in (dom |:f,g:|) /\ [:[:Y1,Y2:],[:Y1,Y2:]:] by RELAT_1:61; then A17: x in [:[:Y1,Y2:],[:Y1,Y2:]:] by XBOOLE_0:def_4; A18: dom G = (dom g) /\ [:Y2,Y2:] by A3, RELAT_1:61; x in dom |:f,g:| by A16, XBOOLE_0:def_4; then consider x11, x21, x12, x22 being set such that A19: x = [[x11,x12],[x21,x22]] and A20: [x11,x21] in dom f and A21: [x12,x22] in dom g by FUNCT_4:def_3; A22: [x21,x22] in [:Y1,Y2:] by A19, A17, ZFMISC_1:87; then A23: x22 in Y2 by ZFMISC_1:87; A24: [x11,x12] in [:Y1,Y2:] by A19, A17, ZFMISC_1:87; then x12 in Y2 by ZFMISC_1:87; then [x12,x22] in [:Y2,Y2:] by A23, ZFMISC_1:87; then A25: [x12,x22] in dom G by A21, A18, XBOOLE_0:def_4; A26: x21 in Y1 by A22, ZFMISC_1:87; x11 in Y1 by A24, ZFMISC_1:87; then [x11,x21] in [:Y1,Y1:] by A26, ZFMISC_1:87; then [x11,x21] in dom F by A20, A15, XBOOLE_0:def_4; hence x in dom |:F,G:| by A19, A25, FUNCT_4:def_3; ::_thesis: verum end; A27: now__::_thesis:_for_x_being_set_st_x_in_dom_|:F,G:|_holds_ |:F,G:|_._x_=_(|:f,g:|_||_[:Y1,Y2:])_._x let x be set ; ::_thesis: ( x in dom |:F,G:| implies |:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x ) assume A28: x in dom |:F,G:| ; ::_thesis: |:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x then consider x11, x21, x12, x22 being set such that A29: x = [[x11,x12],[x21,x22]] and A30: [x11,x21] in dom F and A31: [x12,x22] in dom G by FUNCT_4:def_3; thus |:F,G:| . x = |:F,G:| . ([x11,x12],[x21,x22]) by A29 .= [(F . (x11,x21)),(G . (x12,x22))] by A30, A31, FUNCT_4:def_3 .= [(f . [x11,x21]),(G . [x12,x22])] by A1, A30, FUNCT_1:47 .= [(f . (x11,x21)),(g . (x12,x22))] by A3, A31, FUNCT_1:47 .= |:f,g:| . ([x11,x12],[x21,x22]) by A2, A4, A30, A31, FUNCT_4:def_3 .= (|:f,g:| || [:Y1,Y2:]) . x by A5, A28, A29, FUNCT_1:47 ; ::_thesis: verum end; then A32: for x being Element of [:[:Y1,Y2:],[:Y1,Y2:]:] st x in dom |:F,G:| holds |:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x ; A33: rng (|:f,g:| || [:Y1,Y2:]) c= rng |:F,G:| proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (|:f,g:| || [:Y1,Y2:]) or x in rng |:F,G:| ) assume x in rng (|:f,g:| || [:Y1,Y2:]) ; ::_thesis: x in rng |:F,G:| then consider y being set such that A34: y in dom (|:f,g:| || [:Y1,Y2:]) and A35: x = (|:f,g:| || [:Y1,Y2:]) . y by FUNCT_1:def_3; x = |:F,G:| . y by A5, A27, A34, A35; hence x in rng |:F,G:| by A5, A34, FUNCT_1:def_3; ::_thesis: verum end; rng |:F,G:| c= [:Y1,Y2:] by RELAT_1:def_19; then rng (|:f,g:| || [:Y1,Y2:]) c= [:Y1,Y2:] by A33, XBOOLE_1:1; then |:f,g:| || [:Y1,Y2:] is PartFunc of [:[:Y1,Y2:],[:Y1,Y2:]:],[:Y1,Y2:] by RELAT_1:def_18, A5, RELSET_1:4; hence |:F,G:| = |:f,g:| || [:Y1,Y2:] by A5, A32, PARTFUN1:5; ::_thesis: verum end; theorem :: NATTRA_1:3 canceled; theorem Th4: :: NATTRA_1:4 for o, m being set for f, g being Morphism of (1Cat (o,m)) holds f = g proof let o, m be set ; ::_thesis: for f, g being Morphism of (1Cat (o,m)) holds f = g let f, g be Morphism of (1Cat (o,m)); ::_thesis: f = g f = m by TARSKI:def_1; hence f = g by TARSKI:def_1; ::_thesis: verum end; theorem Th5: :: NATTRA_1:5 for A being Category for a being Object of A holds [[(id a),(id a)],(id a)] in the Comp of A proof let A be Category; ::_thesis: for a being Object of A holds [[(id a),(id a)],(id a)] in the Comp of A let a be Object of A; ::_thesis: [[(id a),(id a)],(id a)] in the Comp of A A1: dom (id a) = a ; A2: cod (id a) = a ; then A3: [(id a),(id a)] in dom the Comp of A by A1, CAT_1:15; (id a) (*) (id a) = id a by A1, CAT_1:22; then the Comp of A . ((id a),(id a)) = id a by A1, A2, CAT_1:16; hence [[(id a),(id a)],(id a)] in the Comp of A by A3, FUNCT_1:def_2; ::_thesis: verum end; theorem Th6: :: NATTRA_1:6 for o, m being set holds the Comp of (1Cat (o,m)) = {[[m,m],m]} proof let o, m be set ; ::_thesis: the Comp of (1Cat (o,m)) = {[[m,m],m]} set A = 1Cat (o,m); reconsider f = m as Morphism of (1Cat (o,m)) by TARSKI:def_1; set a = the Object of (1Cat (o,m)); thus the Comp of (1Cat (o,m)) c= {[[m,m],m]} :: according to XBOOLE_0:def_10 ::_thesis: {[[m,m],m]} c= the Comp of (1Cat (o,m)) proof set o9 = the Object of (1Cat (o,m)); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Comp of (1Cat (o,m)) or x in {[[m,m],m]} ) A1: dom (id the Object of (1Cat (o,m))) = the Object of (1Cat (o,m)) ; A2: cod (id the Object of (1Cat (o,m))) = the Object of (1Cat (o,m)) ; assume A3: x in the Comp of (1Cat (o,m)) ; ::_thesis: x in {[[m,m],m]} then consider x1, x2 being set such that A4: x = [x1,x2] by RELAT_1:def_1; A5: x1 in dom the Comp of (1Cat (o,m)) by A3, A4, XTUPLE_0:def_12; dom the Comp of (1Cat (o,m)) c= [: the carrier' of (1Cat (o,m)), the carrier' of (1Cat (o,m)):] by RELAT_1:def_18; then consider x11, x12 being set such that A6: x11 in the carrier' of (1Cat (o,m)) and A7: x12 in the carrier' of (1Cat (o,m)) and A8: x1 = [x11,x12] by A5, ZFMISC_1:def_2; A9: x12 = id the Object of (1Cat (o,m)) by A7, Th4; x11 = id the Object of (1Cat (o,m)) by A6, Th4; then x2 = the Comp of (1Cat (o,m)) . ((id the Object of (1Cat (o,m))),(id the Object of (1Cat (o,m)))) by A3, A4, A5, A8, A9, FUNCT_1:def_2; then x2 = (id the Object of (1Cat (o,m))) (*) (id the Object of (1Cat (o,m))) by A1, A2, CAT_1:16; then A10: x2 = m by TARSKI:def_1; A11: x12 = m by A7, TARSKI:def_1; x11 = m by A6, TARSKI:def_1; hence x in {[[m,m],m]} by A4, A8, A11, A10, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {[[m,m],m]} or x in the Comp of (1Cat (o,m)) ) assume x in {[[m,m],m]} ; ::_thesis: x in the Comp of (1Cat (o,m)) then A12: x = [[m,m],m] by TARSKI:def_1; f = id the Object of (1Cat (o,m)) by TARSKI:def_1; hence x in the Comp of (1Cat (o,m)) by A12, Th5; ::_thesis: verum end; theorem Th7: :: NATTRA_1:7 for A being Category for a being Object of A holds 1Cat (a,(id a)) is Subcategory of A proof let A be Category; ::_thesis: for a being Object of A holds 1Cat (a,(id a)) is Subcategory of A let d be Object of A; ::_thesis: 1Cat (d,(id d)) is Subcategory of A thus the carrier of (1Cat (d,(id d))) c= the carrier of A :: according to CAT_2:def_4 ::_thesis: ( ( for b1, b2 being Element of the carrier of (1Cat (d,(id d))) for b3, b4 being Element of the carrier of A holds ( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of (1Cat (d,(id d))) c= the Comp of A & ( for b1 being Element of the carrier of (1Cat (d,(id d))) for b2 being Element of the carrier of A holds ( not b1 = b2 or id b1 = id b2 ) ) ) proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in the carrier of (1Cat (d,(id d))) or b in the carrier of A ) assume b in the carrier of (1Cat (d,(id d))) ; ::_thesis: b in the carrier of A then b = d by TARSKI:def_1; hence b in the carrier of A ; ::_thesis: verum end; thus for a, b being Object of (1Cat (d,(id d))) for a9, b9 being Object of A st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) ::_thesis: ( the Comp of (1Cat (d,(id d))) c= the Comp of A & ( for b1 being Element of the carrier of (1Cat (d,(id d))) for b2 being Element of the carrier of A holds ( not b1 = b2 or id b1 = id b2 ) ) ) proof let a, b be Object of (1Cat (d,(id d))); ::_thesis: for a9, b9 being Object of A st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) let a9, b9 be Object of A; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) ) assume that A1: a = a9 and A2: b = b9 ; ::_thesis: Hom (a,b) c= Hom (a9,b9) A3: b9 = d by A2, TARSKI:def_1; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Hom (a,b) or x in Hom (a9,b9) ) assume x in Hom (a,b) ; ::_thesis: x in Hom (a9,b9) then A4: x = id d by TARSKI:def_1; a9 = d by A1, TARSKI:def_1; hence x in Hom (a9,b9) by A3, A4, CAT_1:27; ::_thesis: verum end; thus the Comp of (1Cat (d,(id d))) c= the Comp of A ::_thesis: for b1 being Element of the carrier of (1Cat (d,(id d))) for b2 being Element of the carrier of A holds ( not b1 = b2 or id b1 = id b2 ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Comp of (1Cat (d,(id d))) or x in the Comp of A ) assume x in the Comp of (1Cat (d,(id d))) ; ::_thesis: x in the Comp of A then x in {[[(id d),(id d)],(id d)]} by Th6; then x = [[(id d),(id d)],(id d)] by TARSKI:def_1; hence x in the Comp of A by Th5; ::_thesis: verum end; let a be Object of (1Cat (d,(id d))); ::_thesis: for b1 being Element of the carrier of A holds ( not a = b1 or id a = id b1 ) let a9 be Object of A; ::_thesis: ( not a = a9 or id a = id a9 ) assume a = a9 ; ::_thesis: id a = id a9 then a9 = d by TARSKI:def_1; hence id a = id a9 by TARSKI:def_1; ::_thesis: verum end; theorem Th8: :: NATTRA_1:8 for A being Category for C being Subcategory of A holds ( the Source of C = the Source of A | the carrier' of C & the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C ) proof let A be Category; ::_thesis: for C being Subcategory of A holds ( the Source of C = the Source of A | the carrier' of C & the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C ) let C be Subcategory of A; ::_thesis: ( the Source of C = the Source of A | the carrier' of C & the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C ) A1: dom the Source of A = the carrier' of A by FUNCT_2:def_1; A2: now__::_thesis:_for_x_being_set_st_x_in_dom_the_Source_of_C_holds_ the_Source_of_C_._x_=_the_Source_of_A_._x let x be set ; ::_thesis: ( x in dom the Source of C implies the Source of C . x = the Source of A . x ) assume x in dom the Source of C ; ::_thesis: the Source of C . x = the Source of A . x then reconsider m = x as Morphism of C by FUNCT_2:def_1; reconsider m9 = m as Morphism of A by CAT_2:8; thus the Source of C . x = dom m .= dom m9 by CAT_2:9 .= the Source of A . x ; ::_thesis: verum end; A3: now__::_thesis:_for_x_being_set_st_x_in_dom_the_Target_of_C_holds_ the_Target_of_C_._x_=_the_Target_of_A_._x let x be set ; ::_thesis: ( x in dom the Target of C implies the Target of C . x = the Target of A . x ) assume x in dom the Target of C ; ::_thesis: the Target of C . x = the Target of A . x then reconsider m = x as Morphism of C by FUNCT_2:def_1; reconsider m9 = m as Morphism of A by CAT_2:8; thus the Target of C . x = cod m .= cod m9 by CAT_2:9 .= the Target of A . x ; ::_thesis: verum end; dom the Source of C = the carrier' of C by FUNCT_2:def_1; then dom the Source of C = (dom the Source of A) /\ the carrier' of C by A1, CAT_2:7, XBOOLE_1:28; hence the Source of C = the Source of A | the carrier' of C by A2, FUNCT_1:46; ::_thesis: ( the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C ) A4: dom the Target of A = the carrier' of A by FUNCT_2:def_1; dom the Target of C = the carrier' of C by FUNCT_2:def_1; then dom the Target of C = (dom the Target of A) /\ the carrier' of C by A4, CAT_2:7, XBOOLE_1:28; hence the Target of C = the Target of A | the carrier' of C by A3, FUNCT_1:46; ::_thesis: the Comp of C = the Comp of A || the carrier' of C A5: dom the Comp of C = (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] proof the Comp of C c= the Comp of A by CAT_2:def_4; then A6: dom the Comp of C c= dom the Comp of A by RELAT_1:11; dom the Comp of C c= [: the carrier' of C, the carrier' of C:] by RELAT_1:def_18; hence dom the Comp of C c= (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] by A6, XBOOLE_1:19; :: according to XBOOLE_0:def_10 ::_thesis: (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] c= dom the Comp of C let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] or x in dom the Comp of C ) assume A7: x in (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] ; ::_thesis: x in dom the Comp of C then x in [: the carrier' of C, the carrier' of C:] by XBOOLE_0:def_4; then reconsider f = x `1 , g = x `2 as Morphism of C by MCART_1:10; reconsider f9 = f, g9 = g as Morphism of A by CAT_2:8; x in dom the Comp of A by A7, XBOOLE_0:def_4; then A8: [f9,g9] in dom the Comp of A by MCART_1:21; dom f = dom f9 by CAT_2:9 .= cod g9 by A8, CAT_1:15 .= cod g by CAT_2:9 ; then [f,g] in dom the Comp of C by CAT_1:15; hence x in dom the Comp of C by A7, MCART_1:21; ::_thesis: verum end; the Comp of C c= the Comp of A by CAT_2:def_4; hence the Comp of C = the Comp of A | ((dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:]) by A5, GRFUNC_1:23 .= ( the Comp of A | (dom the Comp of A)) | [: the carrier' of C, the carrier' of C:] by RELAT_1:71 .= the Comp of A || the carrier' of C ; ::_thesis: verum end; theorem Th9: :: NATTRA_1:9 for A being Category for O being non empty Subset of the carrier of A for M being non empty Subset of the carrier' of A st ( for o being Element of A st o in O holds id o in M ) holds for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A proof let A be Category; ::_thesis: for O being non empty Subset of the carrier of A for M being non empty Subset of the carrier' of A st ( for o being Element of A st o in O holds id o in M ) holds for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A let O be non empty Subset of the carrier of A; ::_thesis: for M being non empty Subset of the carrier' of A st ( for o being Element of A st o in O holds id o in M ) holds for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A let M be non empty Subset of the carrier' of A; ::_thesis: ( ( for o being Element of A st o in O holds id o in M ) implies for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A ) assume A1: for o being Element of A st o in O holds id o in M ; ::_thesis: for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A let DOM, COD be Function of M,O; ::_thesis: ( DOM = the Source of A | M & COD = the Target of A | M implies for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A ) assume that A2: DOM = the Source of A | M and A3: COD = the Target of A | M ; ::_thesis: for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A let COMP be PartFunc of [:M,M:],M; ::_thesis: ( COMP = the Comp of A || M implies CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A ) assume A4: COMP = the Comp of A || M ; ::_thesis: CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A set C = CatStr(# O,M,DOM,COD,COMP #); A5: now__::_thesis:_for_f_being_Morphism_of_A for_g_being_Morphism_of_CatStr(#_O,M,DOM,COD,COMP_#)_st_f_=_g_holds_ (_dom_f_=_dom_g_&_cod_f_=_cod_g_) let f be Morphism of A; ::_thesis: for g being Morphism of CatStr(# O,M,DOM,COD,COMP #) st f = g holds ( dom f = dom g & cod f = cod g ) let g be Morphism of CatStr(# O,M,DOM,COD,COMP #); ::_thesis: ( f = g implies ( dom f = dom g & cod f = cod g ) ) assume A6: f = g ; ::_thesis: ( dom f = dom g & cod f = cod g ) dom the Source of CatStr(# O,M,DOM,COD,COMP #) = the carrier' of CatStr(# O,M,DOM,COD,COMP #) by FUNCT_2:def_1; hence dom f = dom g by A2, A6, FUNCT_1:47; ::_thesis: cod f = cod g dom the Target of CatStr(# O,M,DOM,COD,COMP #) = the carrier' of CatStr(# O,M,DOM,COD,COMP #) by FUNCT_2:def_1; hence cod f = cod g by A3, A6, FUNCT_1:47; ::_thesis: verum end; A7: dom the Comp of CatStr(# O,M,DOM,COD,COMP #) = (dom the Comp of A) /\ [: the carrier' of CatStr(# O,M,DOM,COD,COMP #), the carrier' of CatStr(# O,M,DOM,COD,COMP #):] by A4, RELAT_1:61; A8: now__::_thesis:_for_f,_g_being_Morphism_of_CatStr(#_O,M,DOM,COD,COMP_#)_st_dom_g_=_cod_f_holds_ [g,f]_in_dom_the_Comp_of_CatStr(#_O,M,DOM,COD,COMP_#) let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP #); ::_thesis: ( dom g = cod f implies [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) ) reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def_3; assume dom g = cod f ; ::_thesis: [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) then dom g9 = cod f by A5 .= cod f9 by A5 ; then A9: [g9,f9] in dom the Comp of A by CAT_1:def_6; [g,f] in [: the carrier' of CatStr(# O,M,DOM,COD,COMP #), the carrier' of CatStr(# O,M,DOM,COD,COMP #):] by ZFMISC_1:87; hence [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) by A7, A9, XBOOLE_0:def_4; ::_thesis: verum end; A10: dom the Comp of CatStr(# O,M,DOM,COD,COMP #) c= dom the Comp of A by A4, RELAT_1:60; A11: CatStr(# O,M,DOM,COD,COMP #) is Category-like proof let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def_6 ::_thesis: ( ( not [g,f] in proj1 the Comp of CatStr(# O,M,DOM,COD,COMP #) or dom g = cod f ) & ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# O,M,DOM,COD,COMP #) ) ) reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def_3; thus ( [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) implies dom g = cod f ) ::_thesis: ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# O,M,DOM,COD,COMP #) ) proof assume A12: [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) ; ::_thesis: dom g = cod f thus dom g = dom g9 by A5 .= cod f9 by A10, A12, CAT_1:def_6 .= cod f by A5 ; ::_thesis: verum end; thus ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# O,M,DOM,COD,COMP #) ) by A8; ::_thesis: verum end; A13: CatStr(# O,M,DOM,COD,COMP #) is transitive proof let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def_7 ::_thesis: ( not dom g = cod f or ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) ) reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def_3; assume A14: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) by A14, A11, CAT_1:def_6; then A15: the Comp of CatStr(# O,M,DOM,COD,COMP #) . (g,f) = g (*) f by CAT_1:def_1; A16: dom g9 = cod f by A5, A14 .= cod f9 by A5 ; then [g9,f9] in dom the Comp of A by CAT_1:def_6; then A17: the Comp of A . (g9,f9) = g9 (*) f9 by CAT_1:def_1; A18: the Comp of CatStr(# O,M,DOM,COD,COMP #) . (g,f) = the Comp of A . (g9,f9) by A4, A8, A14, FUNCT_1:47; thus dom (g (*) f) = dom (g9 (*) f9) by A5, A18, A15, A17 .= dom f9 by A16, CAT_1:def_7 .= dom f by A5 ; ::_thesis: cod (g (*) f) = cod g thus cod (g (*) f) = cod (g9 (*) f9) by A5, A18, A15, A17 .= cod g9 by A16, CAT_1:def_7 .= cod g by A5 ; ::_thesis: verum end; A19: for f, g being Morphism of CatStr(# O,M,DOM,COD,COMP #) st cod g = dom f holds for ff, gg being Morphism of A st ff = f & gg = g holds f (*) g = ff (*) gg proof let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP #); ::_thesis: ( cod g = dom f implies for ff, gg being Morphism of A st ff = f & gg = g holds f (*) g = ff (*) gg ) assume A20: cod g = dom f ; ::_thesis: for ff, gg being Morphism of A st ff = f & gg = g holds f (*) g = ff (*) gg let ff, gg be Morphism of A; ::_thesis: ( ff = f & gg = g implies f (*) g = ff (*) gg ) assume A21: ( ff = f & gg = g ) ; ::_thesis: f (*) g = ff (*) gg A22: cod gg = dom f by A20, A5, A21 .= dom ff by A5, A21 ; [f,g] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) by A20, A11, CAT_1:def_6; hence f (*) g = the Comp of CatStr(# O,M,DOM,COD,COMP #) . (f,g) by CAT_1:def_1 .= the Comp of A . (ff,gg) by A21, A4, A8, A20, FUNCT_1:47 .= ff (*) gg by A22, CAT_1:16 ; ::_thesis: verum end; A23: CatStr(# O,M,DOM,COD,COMP #) is associative proof let f, g, h be Morphism of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def_8 ::_thesis: ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f ) reconsider g9 = g, f9 = f, h9 = h as Morphism of A by TARSKI:def_3; assume that A24: dom h = cod g and A25: dom g = cod f ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f reconsider gf = the Comp of CatStr(# O,M,DOM,COD,COMP #) . (g,f), hg = the Comp of CatStr(# O,M,DOM,COD,COMP #) . [h,g] as Morphism of CatStr(# O,M,DOM,COD,COMP #) by A8, A24, A25, PARTFUN1:4; A26: dom h9 = cod g by A5, A24 .= cod g9 by A5 ; then A27: [h9,g9] in dom the Comp of A by CAT_1:def_6; A28: dom g9 = cod f by A5, A25 .= cod f9 by A5 ; then A29: [g9,f9] in dom the Comp of A by CAT_1:def_6; reconsider gf9 = g9 (*) f9, hg9 = h9 (*) g9 as Morphism of A ; the Comp of CatStr(# O,M,DOM,COD,COMP #) . (h,g) = the Comp of A . (h9,g9) by A4, A8, A24, FUNCT_1:47; then A30: hg = h9 (*) g9 by A27, CAT_1:def_1; then A31: dom hg = dom hg9 by A5 .= dom g9 by A26, CAT_1:def_7 .= cod f by A5, A25 ; the Comp of CatStr(# O,M,DOM,COD,COMP #) . (g,f) = the Comp of A . (g9,f9) by A4, A8, A25, FUNCT_1:47; then A32: gf = gf9 by A29, CAT_1:def_1; A33: dom h = cod g9 by A5, A24 .= cod gf9 by A28, CAT_1:def_7 .= cod gf by A5, A32 ; A34: h (*) g = h9 (*) g9 by A19, A24; g (*) f = g9 (*) f9 by A19, A25; hence h (*) (g (*) f) = h9 (*) (g9 (*) f9) by A19, A33, A32 .= (h9 (*) g9) (*) f9 by A26, A28, CAT_1:def_8 .= (h (*) g) (*) f by A19, A34, A30, A31 ; ::_thesis: verum end; A35: CatStr(# O,M,DOM,COD,COMP #) is reflexive proof let b be Object of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def_9 ::_thesis: not Hom (b,b) = {} reconsider b9 = b as Object of A by TARSKI:def_3; reconsider ii = id b9 as Morphism of CatStr(# O,M,DOM,COD,COMP #) by A1; A36: cod ii = cod (id b9) by A5 .= b ; dom ii = dom (id b9) by A5 .= b ; then ii in Hom (b,b) by A36; hence Hom (b,b) <> {} ; ::_thesis: verum end; A37: for a being Object of CatStr(# O,M,DOM,COD,COMP #) for aa being Element of A st a = aa holds for m being Morphism of CatStr(# O,M,DOM,COD,COMP #) st m = id aa holds for b being Object of CatStr(# O,M,DOM,COD,COMP #) holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) proof let a be Object of CatStr(# O,M,DOM,COD,COMP #); ::_thesis: for aa being Element of A st a = aa holds for m being Morphism of CatStr(# O,M,DOM,COD,COMP #) st m = id aa holds for b being Object of CatStr(# O,M,DOM,COD,COMP #) holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) let aa be Element of A; ::_thesis: ( a = aa implies for m being Morphism of CatStr(# O,M,DOM,COD,COMP #) st m = id aa holds for b being Object of CatStr(# O,M,DOM,COD,COMP #) holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) ) assume A38: a = aa ; ::_thesis: for m being Morphism of CatStr(# O,M,DOM,COD,COMP #) st m = id aa holds for b being Object of CatStr(# O,M,DOM,COD,COMP #) holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) let m be Morphism of CatStr(# O,M,DOM,COD,COMP #); ::_thesis: ( m = id aa implies for b being Object of CatStr(# O,M,DOM,COD,COMP #) holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) ) assume A39: m = id aa ; ::_thesis: for b being Object of CatStr(# O,M,DOM,COD,COMP #) holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) let b be Object of CatStr(# O,M,DOM,COD,COMP #); ::_thesis: ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) reconsider bb = b as Object of A by TARSKI:def_3; thus ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) proof assume A40: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds f (*) m = f let f be Morphism of a,b; ::_thesis: f (*) m = f reconsider ff = f as Morphism of A by TARSKI:def_3; dom f = a by A40, CAT_1:5; then A41: dom ff = aa by A38, A5; dom f = aa by A38, A40, CAT_1:5 .= cod (id aa) .= cod m by A39, A5 ; hence f (*) m = ff (*) (id aa) by A19, A39 .= f by A41, CAT_1:22 ; ::_thesis: verum end; thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ::_thesis: verum proof assume A42: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds m (*) f = f let f be Morphism of b,a; ::_thesis: m (*) f = f reconsider ff = f as Morphism of A by TARSKI:def_3; cod f = a by A42, CAT_1:5; then A43: cod ff = aa by A38, A5; dom f = b by A42, CAT_1:5; then dom ff = bb by A5; then A44: ff in Hom (bb,aa) by A43; then reconsider ff = ff as Morphism of bb,aa by CAT_1:def_5; A45: Hom (aa,aa) <> {} ; cod f = aa by A38, A42, CAT_1:5 .= dom (id aa) .= dom m by A39, A5 ; hence m (*) f = (id aa) (*) ff by A19, A39 .= (id aa) * ff by A44, A45, CAT_1:def_13 .= f by A44, CAT_1:28 ; ::_thesis: verum end; end; CatStr(# O,M,DOM,COD,COMP #) is with_identities proof let a be Element of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st for b2 being Element of the carrier of CatStr(# O,M,DOM,COD,COMP #) holds ( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) ) reconsider aa = a as Element of A by TARSKI:def_3; reconsider m = id aa as Morphism of CatStr(# O,M,DOM,COD,COMP #) by A1; A46: cod m = cod (id aa) by A5 .= a ; dom m = dom (id aa) by A5 .= a ; then m in Hom (a,a) by A46; then reconsider m = m as Morphism of a,a by CAT_1:def_5; take m ; ::_thesis: for b1 being Element of the carrier of CatStr(# O,M,DOM,COD,COMP #) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) m = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds m (*) b2 = b2 ) ) thus for b1 being Element of the carrier of CatStr(# O,M,DOM,COD,COMP #) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) m = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds m (*) b2 = b2 ) ) by A37; ::_thesis: verum end; then reconsider C = CatStr(# O,M,DOM,COD,COMP #) as Category by A11, A13, A23, A35; C is Subcategory of A proof thus the carrier of C c= the carrier of A ; :: according to CAT_2:def_4 ::_thesis: ( ( for b1, b2 being Element of the carrier of C for b3, b4 being Element of the carrier of A holds ( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of C c= the Comp of A & ( for b1 being Element of the carrier of C for b2 being Element of the carrier of A holds ( not b1 = b2 or id b1 = id b2 ) ) ) thus for a, b being Object of C for a9, b9 being Object of A st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) ::_thesis: ( the Comp of C c= the Comp of A & ( for b1 being Element of the carrier of C for b2 being Element of the carrier of A holds ( not b1 = b2 or id b1 = id b2 ) ) ) proof let a, b be Object of C; ::_thesis: for a9, b9 being Object of A st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) let a9, b9 be Object of A; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) ) assume that A47: a = a9 and A48: b = b9 ; ::_thesis: Hom (a,b) c= Hom (a9,b9) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Hom (a,b) or x in Hom (a9,b9) ) assume x in Hom (a,b) ; ::_thesis: x in Hom (a9,b9) then consider f being Morphism of C such that A49: x = f and A50: dom f = a and A51: cod f = b ; reconsider f9 = f as Morphism of A by TARSKI:def_3; A52: cod f9 = b9 by A5, A48, A51; dom f9 = a9 by A5, A47, A50; hence x in Hom (a9,b9) by A49, A52; ::_thesis: verum end; thus the Comp of C c= the Comp of A by A4, RELAT_1:59; ::_thesis: for b1 being Element of the carrier of C for b2 being Element of the carrier of A holds ( not b1 = b2 or id b1 = id b2 ) let a be Object of C; ::_thesis: for b1 being Element of the carrier of A holds ( not a = b1 or id a = id b1 ) let a9 be Object of A; ::_thesis: ( not a = a9 or id a = id a9 ) assume A53: a = a9 ; ::_thesis: id a = id a9 reconsider m = id a9 as Morphism of C by A1, A53; A54: cod m = cod (id a9) by A5 .= a by A53 ; dom m = dom (id a9) by A5 .= a by A53 ; then m in Hom (a,a) by A54; then reconsider m = m as Morphism of a,a by CAT_1:def_5; for b being Object of C holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) by A53, A37; hence id a = id a9 by CAT_1:def_12; ::_thesis: verum end; hence CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A ; ::_thesis: verum end; theorem Th10: :: NATTRA_1:10 for C being strict Category for A being strict Subcategory of C st the carrier of A = the carrier of C & the carrier' of A = the carrier' of C holds A = C proof let C be strict Category; ::_thesis: for A being strict Subcategory of C st the carrier of A = the carrier of C & the carrier' of A = the carrier' of C holds A = C let A be strict Subcategory of C; ::_thesis: ( the carrier of A = the carrier of C & the carrier' of A = the carrier' of C implies A = C ) assume that A1: the carrier of A = the carrier of C and A2: the carrier' of A = the carrier' of C ; ::_thesis: A = C A3: dom the Target of C = the carrier' of C by FUNCT_2:def_1; A4: dom the Source of C = the carrier' of C by FUNCT_2:def_1; A5: the Target of A = the Target of C | the carrier' of A by Th8 .= the Target of C by A2, A3, RELAT_1:68 ; A6: dom the Comp of C c= [: the carrier' of C, the carrier' of C:] by RELAT_1:def_18; A7: the Comp of A = the Comp of C || the carrier' of A by Th8 .= the Comp of C by A2, A6, RELAT_1:68 ; the Source of A = the Source of C | the carrier' of A by Th8 .= the Source of C by A2, A4, RELAT_1:68 ; hence A = C by A1, A2, A5, A7; ::_thesis: verum end; begin definition canceled; end; :: deftheorem NATTRA_1:def_1_:_ canceled; theorem :: NATTRA_1:11 for B, C, A being Category for F being Functor of A,B for G being Functor of B,C for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f) proof let B, C, A be Category; ::_thesis: for F being Functor of A,B for G being Functor of B,C for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f) let F be Functor of A,B; ::_thesis: for G being Functor of B,C for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f) let G be Functor of B,C; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f) let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f) ) assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f) then A2: Hom ((F . a),(F . b)) <> {} by CAT_1:84; let f be Morphism of a,b; ::_thesis: (G * F) /. f = G /. (F /. f) thus (G * F) /. f = (G * F) . f by A1, CAT_3:def_10 .= G . (F . f) by FUNCT_2:15 .= G . (F /. f) by A1, CAT_3:def_10 .= G /. (F /. f) by A2, CAT_3:def_10 ; ::_thesis: verum end; theorem :: NATTRA_1:12 for A, B being Category for F1, F2 being Functor of A,B st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds F1 . f = F2 . f ) holds F1 = F2 proof let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds F1 . f = F2 . f ) holds F1 = F2 let F1, F2 be Functor of A,B; ::_thesis: ( ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds F1 . f = F2 . f ) implies F1 = F2 ) assume A1: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds F1 . f = F2 . f ; ::_thesis: F1 = F2 now__::_thesis:_for_f_being_Morphism_of_A_holds_F1_._f_=_F2_._f let f be Morphism of A; ::_thesis: F1 . f = F2 . f reconsider f9 = f as Morphism of dom f, cod f by CAT_1:4; set a = dom f; set b = cod f; Hom ((dom f),(cod f)) <> {} by CAT_1:2; hence F1 . f = F2 . f9 by A1 .= F2 . f ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; theorem Th13: :: NATTRA_1:13 for B, A being Category for F being Functor of A,B for a, b, c being Object of A st Hom (a,b) <> {} & Hom (b,c) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f) proof let B, A be Category; ::_thesis: for F being Functor of A,B for a, b, c being Object of A st Hom (a,b) <> {} & Hom (b,c) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f) let F be Functor of A,B; ::_thesis: for a, b, c being Object of A st Hom (a,b) <> {} & Hom (b,c) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f) let a, b, c be Object of A; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies for f being Morphism of a,b for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f) ) assume that A1: Hom (a,b) <> {} and A2: Hom (b,c) <> {} ; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f) let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f) let g be Morphism of b,c; ::_thesis: F /. (g * f) = (F /. g) * (F /. f) A3: dom g = b by A2, CAT_1:5; A4: cod f = b by A1, CAT_1:5; A5: F /. g = F . g by A2, CAT_3:def_10; A6: Hom ((F . a),(F . b)) <> {} by A1, CAT_1:84; A7: F /. f = F . f by A1, CAT_3:def_10; A8: Hom ((F . b),(F . c)) <> {} by A2, CAT_1:84; Hom (a,c) <> {} by A1, A2, CAT_1:24; hence F /. (g * f) = F . (g * f) by CAT_3:def_10 .= F . (g (*) f) by A1, A2, CAT_1:def_13 .= (F . g) (*) (F . f) by A3, A4, CAT_1:64 .= (F /. g) * (F /. f) by A6, A8, A5, A7, CAT_1:def_13 ; ::_thesis: verum end; theorem :: NATTRA_1:14 for A, B being Category for F being Functor of A,B for c being Object of A for d being Object of B st F /. (id c) = id d holds F . c = d proof let A, B be Category; ::_thesis: for F being Functor of A,B for c being Object of A for d being Object of B st F /. (id c) = id d holds F . c = d let F be Functor of A,B; ::_thesis: for c being Object of A for d being Object of B st F /. (id c) = id d holds F . c = d let c be Object of A; ::_thesis: for d being Object of B st F /. (id c) = id d holds F . c = d let d be Object of B; ::_thesis: ( F /. (id c) = id d implies F . c = d ) A1: Hom (c,c) <> {} ; assume F /. (id c) = id d ; ::_thesis: F . c = d then F . (id c) = id d by A1, CAT_3:def_10; hence F . c = d by CAT_1:70; ::_thesis: verum end; theorem Th15: :: NATTRA_1:15 for B, A being Category for F being Functor of A,B for a being Object of A holds F /. (id a) = id (F . a) proof let B, A be Category; ::_thesis: for F being Functor of A,B for a being Object of A holds F /. (id a) = id (F . a) let F be Functor of A,B; ::_thesis: for a being Object of A holds F /. (id a) = id (F . a) let a be Object of A; ::_thesis: F /. (id a) = id (F . a) Hom (a,a) <> {} ; hence F /. (id a) = F . (id a) by CAT_3:def_10 .= id (F . a) by CAT_1:71 ; ::_thesis: verum end; theorem :: NATTRA_1:16 for A being Category for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (id A) /. f = f proof let A be Category; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (id A) /. f = f let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (id A) /. f = f ) assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds (id A) /. f = f let f be Morphism of a,b; ::_thesis: (id A) /. f = f thus (id A) /. f = (id A) . f by A1, CAT_3:def_10 .= f by FUNCT_1:18 ; ::_thesis: verum end; theorem Th17: :: NATTRA_1:17 for A being Category for a, b, c, d being Object of A st Hom (a,b) meets Hom (c,d) holds ( a = c & b = d ) proof let A be Category; ::_thesis: for a, b, c, d being Object of A st Hom (a,b) meets Hom (c,d) holds ( a = c & b = d ) let a, b, c, d be Object of A; ::_thesis: ( Hom (a,b) meets Hom (c,d) implies ( a = c & b = d ) ) assume Hom (a,b) meets Hom (c,d) ; ::_thesis: ( a = c & b = d ) then consider x being set such that A1: x in Hom (a,b) and A2: x in Hom (c,d) by XBOOLE_0:3; reconsider x = x as Morphism of A by A1; A3: cod x = b by A1, CAT_1:1; dom x = a by A1, CAT_1:1; hence ( a = c & b = d ) by A2, A3, CAT_1:1; ::_thesis: verum end; begin definition let A, B be Category; let F1, F2 be Functor of A,B; predF1 is_transformable_to F2 means :Def2: :: NATTRA_1:def 2 for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} ; reflexivity for F1 being Functor of A,B for a being Object of A holds Hom ((F1 . a),(F1 . a)) <> {} ; end; :: deftheorem Def2 defines is_transformable_to NATTRA_1:def_2_:_ for A, B being Category for F1, F2 being Functor of A,B holds ( F1 is_transformable_to F2 iff for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} ); theorem Th18: :: NATTRA_1:18 for A, B being Category for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds F is_transformable_to F2 proof let A, B be Category; ::_thesis: for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds F is_transformable_to F2 let F, F1, F2 be Functor of A,B; ::_thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 implies F is_transformable_to F2 ) assume that A1: F is_transformable_to F1 and A2: F1 is_transformable_to F2 ; ::_thesis: F is_transformable_to F2 let a be Object of A; :: according to NATTRA_1:def_2 ::_thesis: Hom ((F . a),(F2 . a)) <> {} A3: Hom ((F1 . a),(F2 . a)) <> {} by A2, Def2; Hom ((F . a),(F1 . a)) <> {} by A1, Def2; hence Hom ((F . a),(F2 . a)) <> {} by A3, CAT_1:24; ::_thesis: verum end; definition let A, B be Category; let F1, F2 be Functor of A,B; assume A1: F1 is_transformable_to F2 ; mode transformation of F1,F2 -> Function of the carrier of A, the carrier' of B means :Def3: :: NATTRA_1:def 3 for a being Object of A holds it . a is Morphism of F1 . a,F2 . a; existence ex b1 being Function of the carrier of A, the carrier' of B st for a being Object of A holds b1 . a is Morphism of F1 . a,F2 . a proof deffunc H1( Object of A) -> Element of bool the carrier' of B = Hom ((F1 . $1),(F2 . $1)); A2: for a being Object of A holds the carrier' of B meets H1(a) proof let a be Object of A; ::_thesis: the carrier' of B meets H1(a) set x = the Element of Hom ((F1 . a),(F2 . a)); A3: Hom ((F1 . a),(F2 . a)) <> {} by A1, Def2; now__::_thesis:_ex_x_being_Element_of_Hom_((F1_._a),(F2_._a))_st_ (_x_in_the_carrier'_of_B_&_x_in_Hom_((F1_._a),(F2_._a))_) take x = the Element of Hom ((F1 . a),(F2 . a)); ::_thesis: ( x in the carrier' of B & x in Hom ((F1 . a),(F2 . a)) ) thus ( x in the carrier' of B & x in Hom ((F1 . a),(F2 . a)) ) by A3, TARSKI:def_3; ::_thesis: verum end; hence the carrier' of B meets H1(a) by XBOOLE_0:3; ::_thesis: verum end; consider t being Function of the carrier of A, the carrier' of B such that A4: for a being Object of A holds t . a in H1(a) from FUNCT_2:sch_10(A2); take t ; ::_thesis: for a being Object of A holds t . a is Morphism of F1 . a,F2 . a let a be Object of A; ::_thesis: t . a is Morphism of F1 . a,F2 . a t . a in Hom ((F1 . a),(F2 . a)) by A4; hence t . a is Morphism of F1 . a,F2 . a by CAT_1:def_5; ::_thesis: verum end; end; :: deftheorem Def3 defines transformation NATTRA_1:def_3_:_ for A, B being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for b5 being Function of the carrier of A, the carrier' of B holds ( b5 is transformation of F1,F2 iff for a being Object of A holds b5 . a is Morphism of F1 . a,F2 . a ); definition let A, B be Category; let F be Functor of A,B; func id F -> transformation of F,F means :Def4: :: NATTRA_1:def 4 for a being Object of A holds it . a = id (F . a); existence ex b1 being transformation of F,F st for a being Object of A holds b1 . a = id (F . a) proof deffunc H1( Object of A) -> Morphism of F . $1,F . $1 = id (F . $1); consider t being Function of the carrier of A, the carrier' of B such that A1: for a being Object of A holds t . a = H1(a) from FUNCT_2:sch_4(); for a being Object of A holds t . a is Morphism of F . a,F . a proof let a be Object of A; ::_thesis: t . a is Morphism of F . a,F . a t . a = id (F . a) by A1; hence t . a is Morphism of F . a,F . a ; ::_thesis: verum end; then reconsider t = t as transformation of F,F by Def3; take t ; ::_thesis: for a being Object of A holds t . a = id (F . a) let a be Object of A; ::_thesis: t . a = id (F . a) thus t . a = id (F . a) by A1; ::_thesis: verum end; uniqueness for b1, b2 being transformation of F,F st ( for a being Object of A holds b1 . a = id (F . a) ) & ( for a being Object of A holds b2 . a = id (F . a) ) holds b1 = b2 proof let it1, it2 be transformation of F,F; ::_thesis: ( ( for a being Object of A holds it1 . a = id (F . a) ) & ( for a being Object of A holds it2 . a = id (F . a) ) implies it1 = it2 ) assume that A2: for a being Object of A holds it1 . a = id (F . a) and A3: for a being Object of A holds it2 . a = id (F . a) ; ::_thesis: it1 = it2 now__::_thesis:_for_a_being_Object_of_A_holds_it1_._a_=_it2_._a let a be Object of A; ::_thesis: it1 . a = it2 . a thus it1 . a = id (F . a) by A2 .= it2 . a by A3 ; ::_thesis: verum end; hence it1 = it2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines id NATTRA_1:def_4_:_ for A, B being Category for F being Functor of A,B for b4 being transformation of F,F holds ( b4 = id F iff for a being Object of A holds b4 . a = id (F . a) ); definition let A, B be Category; let F1, F2 be Functor of A,B; assume A1: F1 is_transformable_to F2 ; let t be transformation of F1,F2; let a be Object of A; funct . a -> Morphism of F1 . a,F2 . a equals :Def5: :: NATTRA_1:def 5 t . a; coherence t . a is Morphism of F1 . a,F2 . a by A1, Def3; end; :: deftheorem Def5 defines . NATTRA_1:def_5_:_ for A, B being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 for a being Object of A holds t . a = t . a; definition let A, B be Category; let F, F1, F2 be Functor of A,B; assume that A1: F is_transformable_to F1 and A2: F1 is_transformable_to F2 ; let t1 be transformation of F,F1; let t2 be transformation of F1,F2; funct2 `*` t1 -> transformation of F,F2 means :Def6: :: NATTRA_1:def 6 for a being Object of A holds it . a = (t2 . a) * (t1 . a); existence ex b1 being transformation of F,F2 st for a being Object of A holds b1 . a = (t2 . a) * (t1 . a) proof deffunc H1( Object of A) -> Morphism of F . $1,F2 . $1 = (t2 . $1) * (t1 . $1); consider t being Function of the carrier of A, the carrier' of B such that A3: for a being Object of A holds t . a = H1(a) from FUNCT_2:sch_4(); A4: for a being Object of A holds t . a is Morphism of F . a,F2 . a proof let a be Object of A; ::_thesis: t . a is Morphism of F . a,F2 . a t . a = (t2 . a) * (t1 . a) by A3; hence t . a is Morphism of F . a,F2 . a ; ::_thesis: verum end; F is_transformable_to F2 by A1, A2, Th18; then reconsider t9 = t as transformation of F,F2 by A4, Def3; take t9 ; ::_thesis: for a being Object of A holds t9 . a = (t2 . a) * (t1 . a) let a be Object of A; ::_thesis: t9 . a = (t2 . a) * (t1 . a) thus t9 . a = t . a by A1, A2, Def5, Th18 .= (t2 . a) * (t1 . a) by A3 ; ::_thesis: verum end; uniqueness for b1, b2 being transformation of F,F2 st ( for a being Object of A holds b1 . a = (t2 . a) * (t1 . a) ) & ( for a being Object of A holds b2 . a = (t2 . a) * (t1 . a) ) holds b1 = b2 proof let it1, it2 be transformation of F,F2; ::_thesis: ( ( for a being Object of A holds it1 . a = (t2 . a) * (t1 . a) ) & ( for a being Object of A holds it2 . a = (t2 . a) * (t1 . a) ) implies it1 = it2 ) assume that A5: for a being Object of A holds it1 . a = (t2 . a) * (t1 . a) and A6: for a being Object of A holds it2 . a = (t2 . a) * (t1 . a) ; ::_thesis: it1 = it2 now__::_thesis:_for_a_being_Object_of_A_holds_it1_._a_=_it2_._a let a be Object of A; ::_thesis: it1 . a = it2 . a thus it1 . a = it1 . a by A1, A2, Def5, Th18 .= (t2 . a) * (t1 . a) by A5 .= it2 . a by A6 .= it2 . a by A1, A2, Def5, Th18 ; ::_thesis: verum end; hence it1 = it2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def6 defines `*` NATTRA_1:def_6_:_ for A, B being Category for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds for t1 being transformation of F,F1 for t2 being transformation of F1,F2 for b8 being transformation of F,F2 holds ( b8 = t2 `*` t1 iff for a being Object of A holds b8 . a = (t2 . a) * (t1 . a) ); theorem Th19: :: NATTRA_1:19 for B, A being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds t1 = t2 proof let B, A be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds t1 = t2 let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds t1 = t2 ) assume A1: F1 is_transformable_to F2 ; ::_thesis: for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds t1 = t2 let t1, t2 be transformation of F1,F2; ::_thesis: ( ( for a being Object of A holds t1 . a = t2 . a ) implies t1 = t2 ) assume A2: for a being Object of A holds t1 . a = t2 . a ; ::_thesis: t1 = t2 now__::_thesis:_for_a_being_Object_of_A_holds_t1_._a_=_t2_._a let a be Object of A; ::_thesis: t1 . a = t2 . a thus t1 . a = t1 . a by A1, Def5 .= t2 . a by A2 .= t2 . a by A1, Def5 ; ::_thesis: verum end; hence t1 = t2 by FUNCT_2:63; ::_thesis: verum end; theorem Th20: :: NATTRA_1:20 for B, A being Category for F being Functor of A,B for a being Object of A holds (id F) . a = id (F . a) proof let B, A be Category; ::_thesis: for F being Functor of A,B for a being Object of A holds (id F) . a = id (F . a) let F be Functor of A,B; ::_thesis: for a being Object of A holds (id F) . a = id (F . a) let a be Object of A; ::_thesis: (id F) . a = id (F . a) thus (id F) . a = (id F) . a by Def5 .= id (F . a) by Def4 ; ::_thesis: verum end; theorem Th21: :: NATTRA_1:21 for A, B being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 holds ( (id F2) `*` t = t & t `*` (id F1) = t ) proof let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 holds ( (id F2) `*` t = t & t `*` (id F1) = t ) let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2 holds ( (id F2) `*` t = t & t `*` (id F1) = t ) ) assume A1: F1 is_transformable_to F2 ; ::_thesis: for t being transformation of F1,F2 holds ( (id F2) `*` t = t & t `*` (id F1) = t ) let t be transformation of F1,F2; ::_thesis: ( (id F2) `*` t = t & t `*` (id F1) = t ) now__::_thesis:_for_a_being_Object_of_A_holds_((id_F2)_`*`_t)_._a_=_t_._a let a be Object of A; ::_thesis: ((id F2) `*` t) . a = t . a A2: Hom ((F1 . a),(F2 . a)) <> {} by A1, Def2; thus ((id F2) `*` t) . a = ((id F2) . a) * (t . a) by A1, Def6 .= (id (F2 . a)) * (t . a) by Th20 .= t . a by A2, CAT_1:28 ; ::_thesis: verum end; hence (id F2) `*` t = t by A1, Th19; ::_thesis: t `*` (id F1) = t now__::_thesis:_for_a_being_Object_of_A_holds_(t_`*`_(id_F1))_._a_=_t_._a let a be Object of A; ::_thesis: (t `*` (id F1)) . a = t . a A3: Hom ((F1 . a),(F2 . a)) <> {} by A1, Def2; thus (t `*` (id F1)) . a = (t . a) * ((id F1) . a) by A1, Def6 .= (t . a) * (id (F1 . a)) by Th20 .= t . a by A3, CAT_1:29 ; ::_thesis: verum end; hence t `*` (id F1) = t by A1, Th19; ::_thesis: verum end; theorem Th22: :: NATTRA_1:22 for A, B being Category for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 holds for t1 being transformation of F,F1 for t2 being transformation of F1,F2 for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) proof let A, B be Category; ::_thesis: for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 holds for t1 being transformation of F,F1 for t2 being transformation of F1,F2 for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) let F, F1, F2, F3 be Functor of A,B; ::_thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 implies for t1 being transformation of F,F1 for t2 being transformation of F1,F2 for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) ) assume that A1: F is_transformable_to F1 and A2: F1 is_transformable_to F2 and A3: F2 is_transformable_to F3 ; ::_thesis: for t1 being transformation of F,F1 for t2 being transformation of F1,F2 for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) let t1 be transformation of F,F1; ::_thesis: for t2 being transformation of F1,F2 for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) let t2 be transformation of F1,F2; ::_thesis: for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) let t3 be transformation of F2,F3; ::_thesis: (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) A4: F1 is_transformable_to F3 by A2, A3, Th18; A5: F is_transformable_to F2 by A1, A2, Th18; now__::_thesis:_for_a_being_Object_of_A_holds_((t3_`*`_t2)_`*`_t1)_._a_=_(t3_`*`_(t2_`*`_t1))_._a let a be Object of A; ::_thesis: ((t3 `*` t2) `*` t1) . a = (t3 `*` (t2 `*` t1)) . a A6: Hom ((F . a),(F1 . a)) <> {} by A1, Def2; A7: Hom ((F1 . a),(F2 . a)) <> {} by A2, Def2; A8: Hom ((F2 . a),(F3 . a)) <> {} by A3, Def2; thus ((t3 `*` t2) `*` t1) . a = ((t3 `*` t2) . a) * (t1 . a) by A1, A4, Def6 .= ((t3 . a) * (t2 . a)) * (t1 . a) by A2, A3, Def6 .= (t3 . a) * ((t2 . a) * (t1 . a)) by A6, A7, A8, CAT_1:25 .= (t3 . a) * ((t2 `*` t1) . a) by A1, A2, Def6 .= (t3 `*` (t2 `*` t1)) . a by A3, A5, Def6 ; ::_thesis: verum end; hence (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) by A1, A4, Th18, Th19; ::_thesis: verum end; begin Lm1: for B, A being Category for F being Functor of A,B for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) proof let B, A be Category; ::_thesis: for F being Functor of A,B for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) let F be Functor of A,B; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) ) assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) let f be Morphism of a,b; ::_thesis: ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) A2: Hom (a,a) <> {} ; A3: Hom (b,b) <> {} ; thus ((id F) . b) * (F /. f) = (id (F . b)) * (F /. f) by Th20 .= (F /. (id b)) * (F /. f) by Th15 .= F /. ((id b) * f) by A1, A3, Th13 .= F /. f by A1, CAT_1:28 .= F /. (f * (id a)) by A1, CAT_1:29 .= (F /. f) * (F /. (id a)) by A1, A2, Th13 .= (F /. f) * (id (F . a)) by Th15 .= (F /. f) * ((id F) . a) by Th20 ; ::_thesis: verum end; definition let A, B be Category; let F1, F2 be Functor of A,B; predF1 is_naturally_transformable_to F2 means :Def7: :: NATTRA_1:def 7 ( F1 is_transformable_to F2 & ex t being transformation of F1,F2 st for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) ); reflexivity for F1 being Functor of A,B holds ( F1 is_transformable_to F1 & ex t being transformation of F1,F1 st for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F1 /. f) * (t . a) ) proof let F be Functor of A,B; ::_thesis: ( F is_transformable_to F & ex t being transformation of F,F st for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t . b) * (F /. f) = (F /. f) * (t . a) ) ex t being transformation of F,F st for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t . b) * (F /. f) = (F /. f) * (t . a) proof take id F ; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) thus for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) by Lm1; ::_thesis: verum end; hence ( F is_transformable_to F & ex t being transformation of F,F st for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t . b) * (F /. f) = (F /. f) * (t . a) ) ; ::_thesis: verum end; end; :: deftheorem Def7 defines is_naturally_transformable_to NATTRA_1:def_7_:_ for A, B being Category for F1, F2 being Functor of A,B holds ( F1 is_naturally_transformable_to F2 iff ( F1 is_transformable_to F2 & ex t being transformation of F1,F2 st for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) ) ); Lm2: for B, A being Category for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) proof let B, A be Category; ::_thesis: for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) let F, F1, F2 be Functor of A,B; ::_thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 implies for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) ) assume that A1: F is_transformable_to F1 and A2: F1 is_transformable_to F2 ; ::_thesis: for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) let t1 be transformation of F,F1; ::_thesis: ( ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) implies for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) ) assume A3: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ; ::_thesis: for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) let t2 be transformation of F1,F2; ::_thesis: ( ( for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) implies for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) ) assume A4: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) ) A5: Hom ((F . b),(F1 . b)) <> {} by A1, Def2; A6: Hom ((F . a),(F1 . a)) <> {} by A1, Def2; A7: Hom ((F1 . b),(F2 . b)) <> {} by A2, Def2; A8: Hom ((F1 . a),(F2 . a)) <> {} by A2, Def2; assume A9: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) then A10: Hom ((F . a),(F . b)) <> {} by CAT_1:84; let f be Morphism of a,b; ::_thesis: ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) A11: Hom ((F2 . a),(F2 . b)) <> {} by A9, CAT_1:84; A12: Hom ((F1 . a),(F1 . b)) <> {} by A9, CAT_1:84; thus ((t2 `*` t1) . b) * (F /. f) = ((t2 . b) * (t1 . b)) * (F /. f) by A1, A2, Def6 .= (t2 . b) * ((t1 . b) * (F /. f)) by A10, A5, A7, CAT_1:25 .= (t2 . b) * ((F1 /. f) * (t1 . a)) by A3, A9 .= ((t2 . b) * (F1 /. f)) * (t1 . a) by A6, A7, A12, CAT_1:25 .= ((F2 /. f) * (t2 . a)) * (t1 . a) by A4, A9 .= (F2 /. f) * ((t2 . a) * (t1 . a)) by A6, A8, A11, CAT_1:25 .= (F2 /. f) * ((t2 `*` t1) . a) by A1, A2, Def6 ; ::_thesis: verum end; theorem Th23: :: NATTRA_1:23 for A, B being Category for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds F is_naturally_transformable_to F2 proof let A, B be Category; ::_thesis: for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds F is_naturally_transformable_to F2 let F, F1, F2 be Functor of A,B; ::_thesis: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies F is_naturally_transformable_to F2 ) assume A1: F is_transformable_to F1 ; :: according to NATTRA_1:def_7 ::_thesis: ( for t being transformation of F,F1 ex a, b being Object of A st ( Hom (a,b) <> {} & not for f being Morphism of a,b holds (t . b) * (F /. f) = (F1 /. f) * (t . a) ) or not F1 is_naturally_transformable_to F2 or F is_naturally_transformable_to F2 ) given t1 being transformation of F,F1 such that A2: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ; ::_thesis: ( not F1 is_naturally_transformable_to F2 or F is_naturally_transformable_to F2 ) assume A3: F1 is_transformable_to F2 ; :: according to NATTRA_1:def_7 ::_thesis: ( for t being transformation of F1,F2 ex a, b being Object of A st ( Hom (a,b) <> {} & not for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) ) or F is_naturally_transformable_to F2 ) given t2 being transformation of F1,F2 such that A4: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ; ::_thesis: F is_naturally_transformable_to F2 thus F is_transformable_to F2 by A1, A3, Th18; :: according to NATTRA_1:def_7 ::_thesis: ex t being transformation of F,F2 st for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t . b) * (F /. f) = (F2 /. f) * (t . a) take t2 `*` t1 ; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) thus for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) by A1, A2, A3, A4, Lm2; ::_thesis: verum end; definition let A, B be Category; let F1, F2 be Functor of A,B; assume A1: F1 is_naturally_transformable_to F2 ; mode natural_transformation of F1,F2 -> transformation of F1,F2 means :Def8: :: NATTRA_1:def 8 for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (it . b) * (F1 /. f) = (F2 /. f) * (it . a); existence ex b1 being transformation of F1,F2 st for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (b1 . b) * (F1 /. f) = (F2 /. f) * (b1 . a) by A1, Def7; end; :: deftheorem Def8 defines natural_transformation NATTRA_1:def_8_:_ for A, B being Category for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds for b5 being transformation of F1,F2 holds ( b5 is natural_transformation of F1,F2 iff for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (b5 . b) * (F1 /. f) = (F2 /. f) * (b5 . a) ); definition let A, B be Category; let F be Functor of A,B; :: original: id redefine func id F -> natural_transformation of F,F; coherence id F is natural_transformation of F,F proof thus F is_naturally_transformable_to F ; :: according to NATTRA_1:def_8 ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) thus for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) by Lm1; ::_thesis: verum end; end; definition let A, B be Category; let F, F1, F2 be Functor of A,B; assume that B1: F is_naturally_transformable_to F1 and B2: F1 is_naturally_transformable_to F2 ; let t1 be natural_transformation of F,F1; let t2 be natural_transformation of F1,F2; funct2 `*` t1 -> natural_transformation of F,F2 equals :Def9: :: NATTRA_1:def 9 t2 `*` t1; coherence t2 `*` t1 is natural_transformation of F,F2 proof A1: F is_naturally_transformable_to F2 by B1, B2, Th23; A2: F1 is_transformable_to F2 by B2, Def7; A3: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) by B2, Def8; A4: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) by B1, Def8; F is_transformable_to F1 by B1, Def7; then for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) by A2, A4, A3, Lm2; hence t2 `*` t1 is natural_transformation of F,F2 by A1, Def8; ::_thesis: verum end; end; :: deftheorem Def9 defines `*` NATTRA_1:def_9_:_ for A, B being Category for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds for t1 being natural_transformation of F,F1 for t2 being natural_transformation of F1,F2 holds t2 `*` t1 = t2 `*` t1; theorem Th24: :: NATTRA_1:24 for A, B being Category for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds for t being natural_transformation of F1,F2 holds ( (id F2) `*` t = t & t `*` (id F1) = t ) proof let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds for t being natural_transformation of F1,F2 holds ( (id F2) `*` t = t & t `*` (id F1) = t ) let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds ( (id F2) `*` t = t & t `*` (id F1) = t ) ) assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2 holds ( (id F2) `*` t = t & t `*` (id F1) = t ) then A2: F1 is_transformable_to F2 by Def7; let t be natural_transformation of F1,F2; ::_thesis: ( (id F2) `*` t = t & t `*` (id F1) = t ) thus (id F2) `*` t = (id F2) `*` t by A1, Def9 .= t by A2, Th21 ; ::_thesis: t `*` (id F1) = t thus t `*` (id F1) = t `*` (id F1) by A1, Def9 .= t by A2, Th21 ; ::_thesis: verum end; theorem Th25: :: NATTRA_1:25 for B, A being Category for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds for t1 being natural_transformation of F,F1 for t2 being natural_transformation of F1,F2 for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a) proof let B, A be Category; ::_thesis: for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds for t1 being natural_transformation of F,F1 for t2 being natural_transformation of F1,F2 for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a) let F, F1, F2 be Functor of A,B; ::_thesis: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies for t1 being natural_transformation of F,F1 for t2 being natural_transformation of F1,F2 for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a) ) assume that A1: F is_naturally_transformable_to F1 and A2: F1 is_naturally_transformable_to F2 ; ::_thesis: for t1 being natural_transformation of F,F1 for t2 being natural_transformation of F1,F2 for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a) A3: F1 is_transformable_to F2 by A2, Def7; let t1 be natural_transformation of F,F1; ::_thesis: for t2 being natural_transformation of F1,F2 for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a) let t2 be natural_transformation of F1,F2; ::_thesis: for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a) let a be Object of A; ::_thesis: (t2 `*` t1) . a = (t2 . a) * (t1 . a) reconsider t19 = t1 as transformation of F,F1 ; reconsider t29 = t2 as transformation of F1,F2 ; A4: F is_transformable_to F1 by A1, Def7; thus (t2 `*` t1) . a = (t29 `*` t19) . a by A1, A2, Def9 .= (t2 . a) * (t1 . a) by A4, A3, Def6 ; ::_thesis: verum end; theorem Th26: :: NATTRA_1:26 for A, B being Category for F, F1, F2, F3 being Functor of A,B for t being natural_transformation of F,F1 for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) proof let A, B be Category; ::_thesis: for F, F1, F2, F3 being Functor of A,B for t being natural_transformation of F,F1 for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) let F, F1, F2, F3 be Functor of A,B; ::_thesis: for t being natural_transformation of F,F1 for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) let t be natural_transformation of F,F1; ::_thesis: for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) let t1 be natural_transformation of F1,F2; ::_thesis: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) ) assume that A1: F is_naturally_transformable_to F1 and A2: F1 is_naturally_transformable_to F2 and A3: F2 is_naturally_transformable_to F3 ; ::_thesis: for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) A4: F is_naturally_transformable_to F2 by A1, A2, Th23; A5: F2 is_transformable_to F3 by A3, Def7; A6: F1 is_transformable_to F2 by A2, Def7; let t3 be natural_transformation of F2,F3; ::_thesis: (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) A7: F is_transformable_to F1 by A1, Def7; F1 is_naturally_transformable_to F3 by A2, A3, Th23; hence (t3 `*` t1) `*` t = (t3 `*` t1) `*` t by A1, Def9 .= (t3 `*` t1) `*` t by A2, A3, Def9 .= t3 `*` (t1 `*` t) by A7, A6, A5, Th22 .= t3 `*` (t1 `*` t) by A1, A2, Def9 .= t3 `*` (t1 `*` t) by A3, A4, Def9 ; ::_thesis: verum end; definition let A, B be Category; let F1, F2 be Functor of A,B; let IT be transformation of F1,F2; attrIT is invertible means :Def10: :: NATTRA_1:def 10 for a being Object of A holds IT . a is invertible ; end; :: deftheorem Def10 defines invertible NATTRA_1:def_10_:_ for A, B being Category for F1, F2 being Functor of A,B for IT being transformation of F1,F2 holds ( IT is invertible iff for a being Object of A holds IT . a is invertible ); definition let A, B be Category; let F1, F2 be Functor of A,B; predF1,F2 are_naturally_equivalent means :Def11: :: NATTRA_1:def 11 ( F1 is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2 st t is invertible ); reflexivity for F1 being Functor of A,B holds ( F1 is_naturally_transformable_to F1 & ex t being natural_transformation of F1,F1 st t is invertible ) proof let F be Functor of A,B; ::_thesis: ( F is_naturally_transformable_to F & ex t being natural_transformation of F,F st t is invertible ) thus F is_naturally_transformable_to F ; ::_thesis: ex t being natural_transformation of F,F st t is invertible take id F ; ::_thesis: id F is invertible let a be Object of A; :: according to NATTRA_1:def_10 ::_thesis: (id F) . a is invertible (id F) . a = id (F . a) by Th20; hence (id F) . a is invertible by CAT_1:44; ::_thesis: verum end; end; :: deftheorem Def11 defines are_naturally_equivalent NATTRA_1:def_11_:_ for A, B being Category for F1, F2 being Functor of A,B holds ( F1,F2 are_naturally_equivalent iff ( F1 is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2 st t is invertible ) ); notation let A, B be Category; let F1, F2 be Functor of A,B; synonym F1 ~= F2 for F1,F2 are_naturally_equivalent ; end; Lm3: for A, B being Category for F1, F2 being Functor of A,B for t being transformation of F1,F2 st F1 is_transformable_to F2 & t is invertible holds F2 is_transformable_to F1 proof let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B for t being transformation of F1,F2 st F1 is_transformable_to F2 & t is invertible holds F2 is_transformable_to F1 let F1, F2 be Functor of A,B; ::_thesis: for t being transformation of F1,F2 st F1 is_transformable_to F2 & t is invertible holds F2 is_transformable_to F1 let t be transformation of F1,F2; ::_thesis: ( F1 is_transformable_to F2 & t is invertible implies F2 is_transformable_to F1 ) assume that A1: F1 is_transformable_to F2 and A2: for a being Object of A holds t . a is invertible ; :: according to NATTRA_1:def_10 ::_thesis: F2 is_transformable_to F1 let a be Object of A; :: according to NATTRA_1:def_2 ::_thesis: Hom ((F2 . a),(F1 . a)) <> {} A3: t . a is invertible by A2; Hom ((F1 . a),(F2 . a)) <> {} by A1, Def2; hence Hom ((F2 . a),(F1 . a)) <> {} by A3, CAT_1:41; ::_thesis: verum end; definition let A, B be Category; let F1, F2 be Functor of A,B; assume B1: F1 is_transformable_to F2 ; let t1 be transformation of F1,F2; assume B2: t1 is invertible ; funct1 " -> transformation of F2,F1 means :Def12: :: NATTRA_1:def 12 for a being Object of A holds it . a = (t1 . a) " ; existence ex b1 being transformation of F2,F1 st for a being Object of A holds b1 . a = (t1 . a) " proof deffunc H1( Object of A) -> Morphism of F2 . $1,F1 . $1 = (t1 . $1) " ; consider t being Function of the carrier of A, the carrier' of B such that A1: for a being Object of A holds t . a = H1(a) from FUNCT_2:sch_4(); A2: now__::_thesis:_for_a_being_Object_of_A_holds_t_._a_is_Morphism_of_F2_._a,F1_._a let a be Object of A; ::_thesis: t . a is Morphism of F2 . a,F1 . a t . a = (t1 . a) " by A1; hence t . a is Morphism of F2 . a,F1 . a ; ::_thesis: verum end; F2 is_transformable_to F1 by B1, B2, Lm3; then reconsider t = t as transformation of F2,F1 by A2, Def3; take t ; ::_thesis: for a being Object of A holds t . a = (t1 . a) " let a be Object of A; ::_thesis: t . a = (t1 . a) " thus t . a = t . a by B1, B2, Def5, Lm3 .= (t1 . a) " by A1 ; ::_thesis: verum end; uniqueness for b1, b2 being transformation of F2,F1 st ( for a being Object of A holds b1 . a = (t1 . a) " ) & ( for a being Object of A holds b2 . a = (t1 . a) " ) holds b1 = b2 proof let t, t9 be transformation of F2,F1; ::_thesis: ( ( for a being Object of A holds t . a = (t1 . a) " ) & ( for a being Object of A holds t9 . a = (t1 . a) " ) implies t = t9 ) assume that A3: for a being Object of A holds t . a = (t1 . a) " and A4: for a being Object of A holds t9 . a = (t1 . a) " ; ::_thesis: t = t9 now__::_thesis:_for_a_being_Object_of_A_holds_t_._a_=_t9_._a let a be Object of A; ::_thesis: t . a = t9 . a thus t . a = (t1 . a) " by A3 .= t9 . a by A4 ; ::_thesis: verum end; hence t = t9 by B1, B2, Lm3, Th19; ::_thesis: verum end; end; :: deftheorem Def12 defines " NATTRA_1:def_12_:_ for A, B being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t1 being transformation of F1,F2 st t1 is invertible holds for b6 being transformation of F2,F1 holds ( b6 = t1 " iff for a being Object of A holds b6 . a = (t1 . a) " ); Lm4: now__::_thesis:_for_A,_B_being_Category for_F1,_F2_being_Functor_of_A,B for_t1_being_natural_transformation_of_F1,F2_st_F1_is_naturally_transformable_to_F2_&_t1_is_invertible_holds_ for_a,_b_being_Object_of_A_st_Hom_(a,b)_<>_{}_holds_ for_f_being_Morphism_of_a,b_holds_((t1_")_._b)_*_(F2_/._f)_=_(F1_/._f)_*_((t1_")_._a) let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) let F1, F2 be Functor of A,B; ::_thesis: for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) let t1 be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & t1 is invertible implies for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) ) assume that A1: F1 is_naturally_transformable_to F2 and A2: t1 is invertible ; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) ) assume A3: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) A4: Hom ((F1 . a),(F1 . b)) <> {} by A3, CAT_1:84; let f be Morphism of a,b; ::_thesis: ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) A5: Hom ((F2 . a),(F2 . b)) <> {} by A3, CAT_1:84; A6: F1 is_transformable_to F2 by A1, Def7; A7: Hom ((F1 . b),(F2 . b)) <> {} by Def2, A1, Def7; A8: t1 . b is invertible by A2, Def10; then A9: Hom ((F2 . b),(F1 . b)) <> {} by A7, CAT_1:41; A10: Hom ((F1 . a),(F2 . a)) <> {} by A1, Def7, Def2; (F2 /. f) * (t1 . a) = (t1 . b) * (F1 /. f) by A1, A3, Def8; then A11: (((t1 . b) ") * (F2 /. f)) * (t1 . a) = ((t1 . b) ") * ((t1 . b) * (F1 /. f)) by A10, A9, A5, CAT_1:25 .= (((t1 . b) ") * (t1 . b)) * (F1 /. f) by A4, A7, A9, CAT_1:25 .= (id (F1 . b)) * (F1 /. f) by A8, CAT_1:def_17 .= F1 /. f by A4, CAT_1:28 ; A12: t1 . a is invertible by A2, Def10; then A13: Hom ((F2 . a),(F1 . a)) <> {} by A10, CAT_1:41; then A14: Hom ((F2 . a),(F1 . b)) <> {} by A4, CAT_1:24; then ((t1 . b) ") * (F2 /. f) = (((t1 . b) ") * (F2 /. f)) * (id (F2 . a)) by CAT_1:29 .= (((t1 . b) ") * (F2 /. f)) * ((t1 . a) * ((t1 . a) ")) by A12, CAT_1:def_17 .= (F1 /. f) * ((t1 . a) ") by A10, A13, A14, A11, CAT_1:25 ; hence ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 . a) ") by A2, A6, Def12 .= (F1 /. f) * ((t1 ") . a) by A2, A6, Def12 ; ::_thesis: verum end; Lm5: for A, B being Category for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds F2 is_naturally_transformable_to F1 proof let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds F2 is_naturally_transformable_to F1 let F1, F2 be Functor of A,B; ::_thesis: for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds F2 is_naturally_transformable_to F1 let t1 be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & t1 is invertible implies F2 is_naturally_transformable_to F1 ) assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: ( not t1 is invertible or F2 is_naturally_transformable_to F1 ) assume A2: t1 is invertible ; ::_thesis: F2 is_naturally_transformable_to F1 hence F2 is_transformable_to F1 by A1, Def7, Lm3; :: according to NATTRA_1:def_7 ::_thesis: ex t being transformation of F2,F1 st for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds (t . b) * (F2 /. f) = (F1 /. f) * (t . a) take t1 " ; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) thus for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) by A1, A2, Lm4; ::_thesis: verum end; definition let A, B be Category; let F1, F2 be Functor of A,B; let t1 be natural_transformation of F1,F2; assume that B1: F1 is_naturally_transformable_to F2 and B2: t1 is invertible ; funct1 " -> natural_transformation of F2,F1 equals :Def13: :: NATTRA_1:def 13 t1 " ; coherence t1 " is natural_transformation of F2,F1 proof A1: for a, b being Object of A st Hom (a,b) <> {} holds for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) by B1, B2, Lm4; F2 is_naturally_transformable_to F1 by B1, B2, Lm5; hence t1 " is natural_transformation of F2,F1 by A1, Def8; ::_thesis: verum end; end; :: deftheorem Def13 defines " NATTRA_1:def_13_:_ for A, B being Category for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds t1 " = t1 " ; theorem Th27: :: NATTRA_1:27 for A, B being Category for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds for a being Object of A holds (t1 ") . a = (t1 . a) " proof let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds for a being Object of A holds (t1 ") . a = (t1 . a) " let F1, F2 be Functor of A,B; ::_thesis: for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds for a being Object of A holds (t1 ") . a = (t1 . a) " let t1 be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & t1 is invertible implies for a being Object of A holds (t1 ") . a = (t1 . a) " ) assume that A1: F1 is_naturally_transformable_to F2 and A2: t1 is invertible ; ::_thesis: for a being Object of A holds (t1 ") . a = (t1 . a) " let a be Object of A; ::_thesis: (t1 ") . a = (t1 . a) " A3: F1 is_transformable_to F2 by A1, Def7; thus (t1 ") . a = (t1 ") . a by A1, A2, Def13 .= (t1 . a) " by A2, A3, Def12 ; ::_thesis: verum end; theorem :: NATTRA_1:28 for A, B being Category for F1, F2 being Functor of A,B st F1 ~= F2 holds F2 ~= F1 proof let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 ~= F2 holds F2 ~= F1 let F1, F2 be Functor of A,B; ::_thesis: ( F1 ~= F2 implies F2 ~= F1 ) assume A1: F1 is_naturally_transformable_to F2 ; :: according to NATTRA_1:def_11 ::_thesis: ( for t being natural_transformation of F1,F2 holds not t is invertible or F2 ~= F1 ) given t being natural_transformation of F1,F2 such that A2: t is invertible ; ::_thesis: F2 ~= F1 thus F2 is_naturally_transformable_to F1 by A1, A2, Lm5; :: according to NATTRA_1:def_11 ::_thesis: ex t being natural_transformation of F2,F1 st t is invertible take t " ; ::_thesis: t " is invertible let a be Object of A; :: according to NATTRA_1:def_10 ::_thesis: (t ") . a is invertible (t ") . a = (t . a) " by A1, A2, Th27; hence (t ") . a is invertible by A2, Def10, CAT_1:46; ::_thesis: verum end; theorem Th29: :: NATTRA_1:29 for A, B being Category for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds F1 ~= F3 proof let A, B be Category; ::_thesis: for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds F1 ~= F3 let F1, F2, F3 be Functor of A,B; ::_thesis: ( F1 ~= F2 & F2 ~= F3 implies F1 ~= F3 ) assume A1: F1 is_naturally_transformable_to F2 ; :: according to NATTRA_1:def_11 ::_thesis: ( for t being natural_transformation of F1,F2 holds not t is invertible or not F2 ~= F3 or F1 ~= F3 ) given t being natural_transformation of F1,F2 such that A2: t is invertible ; ::_thesis: ( not F2 ~= F3 or F1 ~= F3 ) assume A3: F2 is_naturally_transformable_to F3 ; :: according to NATTRA_1:def_11 ::_thesis: ( for t being natural_transformation of F2,F3 holds not t is invertible or F1 ~= F3 ) given t9 being natural_transformation of F2,F3 such that A4: t9 is invertible ; ::_thesis: F1 ~= F3 thus F1 is_naturally_transformable_to F3 by A1, A3, Th23; :: according to NATTRA_1:def_11 ::_thesis: ex t being natural_transformation of F1,F3 st t is invertible take t9 `*` t ; ::_thesis: t9 `*` t is invertible let a be Object of A; :: according to NATTRA_1:def_10 ::_thesis: (t9 `*` t) . a is invertible A5: t9 . a is invertible by A4, Def10; A6: t . a is invertible by A2, Def10; (t9 `*` t) . a = (t9 . a) * (t . a) by A1, A3, Th25; hence (t9 `*` t) . a is invertible by A5, A6, CAT_1:45; ::_thesis: verum end; definition let A, B be Category; let F1, F2 be Functor of A,B; assume A1: F1,F2 are_naturally_equivalent ; mode natural_equivalence of F1,F2 -> natural_transformation of F1,F2 means :Def14: :: NATTRA_1:def 14 it is invertible ; existence ex b1 being natural_transformation of F1,F2 st b1 is invertible by A1, Def11; end; :: deftheorem Def14 defines natural_equivalence NATTRA_1:def_14_:_ for A, B being Category for F1, F2 being Functor of A,B st F1,F2 are_naturally_equivalent holds for b5 being natural_transformation of F1,F2 holds ( b5 is natural_equivalence of F1,F2 iff b5 is invertible ); theorem :: NATTRA_1:30 for A, B being Category for F being Functor of A,B holds id F is natural_equivalence of F,F proof let A, B be Category; ::_thesis: for F being Functor of A,B holds id F is natural_equivalence of F,F let F be Functor of A,B; ::_thesis: id F is natural_equivalence of F,F thus F ~= F ; :: according to NATTRA_1:def_14 ::_thesis: id F is invertible let a be Object of A; :: according to NATTRA_1:def_10 ::_thesis: (id F) . a is invertible (id F) . a = id (F . a) by Th20; hence (id F) . a is invertible by CAT_1:44; ::_thesis: verum end; theorem :: NATTRA_1:31 for A, B being Category for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds for t being natural_equivalence of F1,F2 for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3 proof let A, B be Category; ::_thesis: for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds for t being natural_equivalence of F1,F2 for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3 let F1, F2, F3 be Functor of A,B; ::_thesis: ( F1 ~= F2 & F2 ~= F3 implies for t being natural_equivalence of F1,F2 for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3 ) assume that A1: F1,F2 are_naturally_equivalent and A2: F2,F3 are_naturally_equivalent ; ::_thesis: for t being natural_equivalence of F1,F2 for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3 let t be natural_equivalence of F1,F2; ::_thesis: for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3 let t9 be natural_equivalence of F2,F3; ::_thesis: t9 `*` t is natural_equivalence of F1,F3 thus F1,F3 are_naturally_equivalent by A1, A2, Th29; :: according to NATTRA_1:def_14 ::_thesis: t9 `*` t is invertible let a be Object of A; :: according to NATTRA_1:def_10 ::_thesis: (t9 `*` t) . a is invertible t9 is invertible by A2, Def14; then A3: t9 . a is invertible by Def10; t is invertible by A1, Def14; then A4: t . a is invertible by Def10; A5: F1 is_naturally_transformable_to F2 by A1, Def11; A6: F2 is_naturally_transformable_to F3 by A2, Def11; (t9 `*` t) . a = (t9 . a) * (t . a) by A5, A6, Th25; hence (t9 `*` t) . a is invertible by A3, A4, CAT_1:45; ::_thesis: verum end; begin definition let A, B be Category; mode NatTrans-DOMAIN of A,B -> non empty set means :Def15: :: NATTRA_1:def 15 for x being set st x in it holds ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ); existence ex b1 being non empty set st for x being set st x in b1 holds ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) proof set F = the Functor of A,B; take {[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)]} ; ::_thesis: for x being set st x in {[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)]} holds ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) let x be set ; ::_thesis: ( x in {[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)]} implies ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) assume A1: x in {[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)]} ; ::_thesis: ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) take the Functor of A,B ; ::_thesis: ex F2 being Functor of A,B ex t being natural_transformation of the Functor of A,B,F2 st ( x = [[ the Functor of A,B,F2],t] & the Functor of A,B is_naturally_transformable_to F2 ) take the Functor of A,B ; ::_thesis: ex t being natural_transformation of the Functor of A,B, the Functor of A,B st ( x = [[ the Functor of A,B, the Functor of A,B],t] & the Functor of A,B is_naturally_transformable_to the Functor of A,B ) take id the Functor of A,B ; ::_thesis: ( x = [[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)] & the Functor of A,B is_naturally_transformable_to the Functor of A,B ) thus ( x = [[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)] & the Functor of A,B is_naturally_transformable_to the Functor of A,B ) by A1, TARSKI:def_1; ::_thesis: verum end; end; :: deftheorem Def15 defines NatTrans-DOMAIN NATTRA_1:def_15_:_ for A, B being Category for b3 being non empty set holds ( b3 is NatTrans-DOMAIN of A,B iff for x being set st x in b3 holds ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ); definition let A, B be Category; func NatTrans (A,B) -> NatTrans-DOMAIN of A,B means :Def16: :: NATTRA_1:def 16 for x being set holds ( x in it iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ); existence ex b1 being NatTrans-DOMAIN of A,B st for x being set holds ( x in b1 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) proof set F = the Functor of A,B; defpred S1[ set ] means ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( $1 = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ); consider T being set such that A1: for x being set holds ( x in T iff ( x in [:[:(Funct (A,B)),(Funct (A,B)):],(Funcs ( the carrier of A, the carrier' of B)):] & S1[x] ) ) from XBOOLE_0:sch_1(); the Functor of A,B in Funct (A,B) by CAT_2:def_2; then A2: [ the Functor of A,B, the Functor of A,B] in [:(Funct (A,B)),(Funct (A,B)):] by ZFMISC_1:87; id the Functor of A,B in Funcs ( the carrier of A, the carrier' of B) by FUNCT_2:8; then [[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)] in [:[:(Funct (A,B)),(Funct (A,B)):],(Funcs ( the carrier of A, the carrier' of B)):] by A2, ZFMISC_1:87; then reconsider T = T as non empty set by A1; for x being set st x in T holds ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) by A1; then reconsider T = T as NatTrans-DOMAIN of A,B by Def15; take T ; ::_thesis: for x being set holds ( x in T iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) let x be set ; ::_thesis: ( x in T iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) thus ( x in T implies ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) by A1; ::_thesis: ( ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) implies x in T ) given F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that A3: x = [[F1,F2],t] and A4: F1 is_naturally_transformable_to F2 ; ::_thesis: x in T A5: F2 in Funct (A,B) by CAT_2:def_2; A6: t in Funcs ( the carrier of A, the carrier' of B) by FUNCT_2:8; F1 in Funct (A,B) by CAT_2:def_2; then [F1,F2] in [:(Funct (A,B)),(Funct (A,B)):] by A5, ZFMISC_1:87; then x in [:[:(Funct (A,B)),(Funct (A,B)):],(Funcs ( the carrier of A, the carrier' of B)):] by A3, A6, ZFMISC_1:87; hence x in T by A1, A3, A4; ::_thesis: verum end; uniqueness for b1, b2 being NatTrans-DOMAIN of A,B st ( for x being set holds ( x in b1 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) & ( for x being set holds ( x in b2 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) holds b1 = b2 proof let S, T be NatTrans-DOMAIN of A,B; ::_thesis: ( ( for x being set holds ( x in S iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) & ( for x being set holds ( x in T iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) implies S = T ) assume that A7: for x being set holds ( x in S iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) and A8: for x being set holds ( x in T iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ; ::_thesis: S = T now__::_thesis:_for_x_being_set_holds_ (_x_in_S_iff_x_in_T_) let x be set ; ::_thesis: ( x in S iff x in T ) ( x in S iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) by A7; hence ( x in S iff x in T ) by A8; ::_thesis: verum end; hence S = T by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def16 defines NatTrans NATTRA_1:def_16_:_ for A, B being Category for b3 being NatTrans-DOMAIN of A,B holds ( b3 = NatTrans (A,B) iff for x being set holds ( x in b3 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ); theorem Th32: :: NATTRA_1:32 for A, B being Category for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 holds ( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans (A,B) ) proof let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B for t1 being natural_transformation of F1,F2 holds ( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans (A,B) ) let F1, F2 be Functor of A,B; ::_thesis: for t1 being natural_transformation of F1,F2 holds ( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans (A,B) ) let t1 be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans (A,B) ) thus ( F1 is_naturally_transformable_to F2 implies [[F1,F2],t1] in NatTrans (A,B) ) by Def16; ::_thesis: ( [[F1,F2],t1] in NatTrans (A,B) implies F1 is_naturally_transformable_to F2 ) assume [[F1,F2],t1] in NatTrans (A,B) ; ::_thesis: F1 is_naturally_transformable_to F2 then consider F19, F29 being Functor of A,B, t being natural_transformation of F19,F29 such that A1: [[F1,F2],t1] = [[F19,F29],t] and A2: F19 is_naturally_transformable_to F29 by Def16; A3: [F1,F2] = [F19,F29] by A1, XTUPLE_0:1; then F1 = F19 by XTUPLE_0:1; hence F1 is_naturally_transformable_to F2 by A2, A3, XTUPLE_0:1; ::_thesis: verum end; definition let A, B be Category; func Functors (A,B) -> strict Category means :Def17: :: NATTRA_1:def 17 ( the carrier of it = Funct (A,B) & the carrier' of it = NatTrans (A,B) & ( for f being Morphism of it holds ( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of it st dom g = cod f holds [g,f] in dom the Comp of it ) & ( for f, g being Morphism of it st [g,f] in dom the Comp of it holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of it . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of it for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) ); existence ex b1 being strict Category st ( the carrier of b1 = Funct (A,B) & the carrier' of b1 = NatTrans (A,B) & ( for f being Morphism of b1 holds ( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b1 st dom g = cod f holds [g,f] in dom the Comp of b1 ) & ( for f, g being Morphism of b1 st [g,f] in dom the Comp of b1 holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b1 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b1 for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) ) proof defpred S1[ set , set , set ] means ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( $2 = [[F,F1],t] & $1 = [[F1,F2],t1] & $3 = [[F,F2],(t1 `*` t)] ); deffunc H1( set ) -> set = ($1 `1) `1 ; A1: now__::_thesis:_for_x,_y,_z1,_z2_being_set_st_x_in_NatTrans_(A,B)_&_y_in_NatTrans_(A,B)_&_S1[x,y,z1]_&_S1[x,y,z2]_holds_ z1_=_z2 let x, y, z1, z2 be set ; ::_thesis: ( x in NatTrans (A,B) & y in NatTrans (A,B) & S1[x,y,z1] & S1[x,y,z2] implies z1 = z2 ) assume that x in NatTrans (A,B) and y in NatTrans (A,B) ; ::_thesis: ( S1[x,y,z1] & S1[x,y,z2] implies z1 = z2 ) assume S1[x,y,z1] ; ::_thesis: ( S1[x,y,z2] implies z1 = z2 ) then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that A2: y = [[F,F1],t] and A3: x = [[F1,F2],t1] and A4: z1 = [[F,F2],(t1 `*` t)] ; assume S1[x,y,z2] ; ::_thesis: z1 = z2 then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that A5: y = [[F9,F19],t9] and A6: x = [[F19,F29],t19] and A7: z2 = [[F9,F29],(t19 `*` t9)] ; A8: t = t9 by A2, A5, XTUPLE_0:1; [F1,F2] = [F19,F29] by A3, A6, XTUPLE_0:1; then A9: F2 = F29 by XTUPLE_0:1; A10: t1 = t19 by A3, A6, XTUPLE_0:1; A11: [F,F1] = [F9,F19] by A2, A5, XTUPLE_0:1; then F = F9 by XTUPLE_0:1; hence z1 = z2 by A4, A7, A11, A8, A10, A9, XTUPLE_0:1; ::_thesis: verum end; A12: now__::_thesis:_for_x,_y,_z_being_set_st_x_in_NatTrans_(A,B)_&_y_in_NatTrans_(A,B)_&_S1[x,y,z]_holds_ z_in_NatTrans_(A,B) let x, y, z be set ; ::_thesis: ( x in NatTrans (A,B) & y in NatTrans (A,B) & S1[x,y,z] implies z in NatTrans (A,B) ) assume that A13: x in NatTrans (A,B) and A14: y in NatTrans (A,B) ; ::_thesis: ( S1[x,y,z] implies z in NatTrans (A,B) ) assume S1[x,y,z] ; ::_thesis: z in NatTrans (A,B) then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that A15: y = [[F,F1],t] and A16: x = [[F1,F2],t1] and A17: z = [[F,F2],(t1 `*` t)] ; A18: F1 is_naturally_transformable_to F2 by A13, A16, Th32; F is_naturally_transformable_to F1 by A14, A15, Th32; hence z in NatTrans (A,B) by A17, Th32, A18, Th23; ::_thesis: verum end; consider m being PartFunc of [:(NatTrans (A,B)),(NatTrans (A,B)):],(NatTrans (A,B)) such that A19: for x, y being set holds ( [x,y] in dom m iff ( x in NatTrans (A,B) & y in NatTrans (A,B) & ex z being set st S1[x,y,z] ) ) and A20: for x, y being set st [x,y] in dom m holds S1[x,y,m . (x,y)] from BINOP_1:sch_5(A12, A1); A21: now__::_thesis:_for_t_being_Element_of_NatTrans_(A,B)_holds_H1(t)_in_Funct_(A,B) let t be Element of NatTrans (A,B); ::_thesis: H1(t) in Funct (A,B) consider F1, F2 being Functor of A,B, s being natural_transformation of F1,F2 such that A22: t = [[F1,F2],s] and F1 is_naturally_transformable_to F2 by Def16; (t `1) `1 = [F1,F2] `1 by A22, MCART_1:7 .= F1 ; hence H1(t) in Funct (A,B) by CAT_2:def_2; ::_thesis: verum end; consider d being Function of (NatTrans (A,B)),(Funct (A,B)) such that A23: for t being Element of NatTrans (A,B) holds d . t = H1(t) from FUNCT_2:sch_8(A21); deffunc H2( set ) -> set = ($1 `1) `2 ; A24: now__::_thesis:_for_t_being_Element_of_NatTrans_(A,B)_holds_H2(t)_in_Funct_(A,B) let t be Element of NatTrans (A,B); ::_thesis: H2(t) in Funct (A,B) consider F1, F2 being Functor of A,B, s being natural_transformation of F1,F2 such that A25: t = [[F1,F2],s] and F1 is_naturally_transformable_to F2 by Def16; (t `1) `2 = [F1,F2] `2 by A25, MCART_1:7 .= F2 ; hence H2(t) in Funct (A,B) by CAT_2:def_2; ::_thesis: verum end; consider c being Function of (NatTrans (A,B)),(Funct (A,B)) such that A26: for t being Element of NatTrans (A,B) holds c . t = H2(t) from FUNCT_2:sch_8(A24); deffunc H3( Element of Funct (A,B)) -> set = [[$1,$1],(id $1)]; A27: for F being Element of Funct (A,B) holds H3(F) in NatTrans (A,B) by Def16; consider i being Function of (Funct (A,B)),(NatTrans (A,B)) such that A28: for F being Element of Funct (A,B) holds i . F = H3(F) from FUNCT_2:sch_8(A27); set C = CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); A29: now__::_thesis:_for_F,_F1,_F2_being_Functor_of_A,B for_t_being_natural_transformation_of_F,F1 for_t1_being_natural_transformation_of_F1,F2_st_F1_is_naturally_transformable_to_F2_&_F_is_naturally_transformable_to_F1_holds_ m_._[[[F1,F2],t1],[[F,F1],t]]_=_[[F,F2],(t1_`*`_t)] let F, F1, F2 be Functor of A,B; ::_thesis: for t being natural_transformation of F,F1 for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 holds m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)] let t be natural_transformation of F,F1; ::_thesis: for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 holds m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)] let t1 be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 implies m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)] ) assume that A30: F1 is_naturally_transformable_to F2 and A31: F is_naturally_transformable_to F1 ; ::_thesis: m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)] A32: [[F,F1],t] in NatTrans (A,B) by A31, Th32; A33: S1[[[F1,F2],t1],[[F,F1],t],[[F,F2],(t1 `*` t)]] ; [[F1,F2],t1] in NatTrans (A,B) by A30, Th32; then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that A34: [[F,F1],t] = [[F9,F19],t9] and A35: [[F1,F2],t1] = [[F19,F29],t19] and A36: m . ([[F1,F2],t1],[[F,F1],t]) = [[F9,F29],(t19 `*` t9)] by A20, A19, A32, A33; A37: t = t9 by A34, XTUPLE_0:1; [F1,F2] = [F19,F29] by A35, XTUPLE_0:1; then A38: F2 = F29 by XTUPLE_0:1; A39: t1 = t19 by A35, XTUPLE_0:1; A40: [F,F1] = [F9,F19] by A34, XTUPLE_0:1; then F = F9 by XTUPLE_0:1; hence m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)] by A36, A40, A37, A39, A38, XTUPLE_0:1; ::_thesis: verum end; A41: CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is Category-like proof let f, g be Element of the carrier' of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def_6 ::_thesis: ( ( not [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) or dom g = cod f ) & ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ) ) consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that A42: f = [[F19,F29],t9] and A43: F19 is_naturally_transformable_to F29 by Def16; thus ( [g,f] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) implies dom g = cod f ) ::_thesis: ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ) proof assume [g,f] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ; ::_thesis: dom g = cod f then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that A44: f = [[F,F1],t] and A45: g = [[F1,F2],t1] and m . (g,f) = [[F,F2],(t1 `*` t)] by A20; thus dom g = (g `1) `1 by A23 .= [F1,F2] `1 by A45, MCART_1:7 .= [F,F1] `2 .= (f `1) `2 by A44, MCART_1:7 .= cod f by A26 ; ::_thesis: verum end; assume A46: dom g = cod f ; ::_thesis: [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that A47: g = [[F1,F2],t] and A48: F1 is_naturally_transformable_to F2 by Def16; A49: F1 = [F1,F2] `1 .= (g `1) `1 by A47, MCART_1:7 .= c . f by A23, A46 .= (f `1) `2 by A26 .= [F19,F29] `2 by A42, MCART_1:7 .= F29 ; then reconsider t = t as natural_transformation of F29,F2 ; m . [g,f] = [[F19,F2],(t `*` t9)] by A29, A47, A48, A42, A43, A49; hence [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) by A19, A47, A42, A49; ::_thesis: verum end; A50: CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is transitive proof let f, g be Element of the carrier' of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def_7 ::_thesis: ( not dom g = cod f or ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) ) consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that A51: f = [[F19,F29],t9] and A52: F19 is_naturally_transformable_to F29 by Def16; assume dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) then A53: [g,f] in dom m by A41, CAT_1:def_6; then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that A54: f = [[F,F1],t] and A55: g = [[F1,F2],t1] and A56: m . (g,f) = [[F,F2],(t1 `*` t)] by A20; A57: m . (g,f) = g (*) f by A53, CAT_1:def_1; A58: [F,F1] = [F19,F29] by A54, A51, XTUPLE_0:1; then A59: F = F19 by XTUPLE_0:1; A60: F1 = F29 by A58, XTUPLE_0:1; consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that A61: g = [[F19,F29],t9] and A62: F19 is_naturally_transformable_to F29 by Def16; A63: [F1,F2] = [F19,F29] by A55, A61, XTUPLE_0:1; then A64: F2 = F29 by XTUPLE_0:1; F1 = F19 by A63, XTUPLE_0:1; then reconsider x = [[F,F2],(t1 `*` t)] as Element of NatTrans (A,B) by Th32, A52, A59, A60, A62, A64, Th23; thus dom (g (*) f) = (x `1) `1 by A23, A56, A57 .= [F,F2] `1 by MCART_1:7 .= ([[F,F1],t] `1) `1 .= dom f by A23, A54 ; ::_thesis: cod (g (*) f) = cod g thus cod (g (*) f) = (x `1) `2 by A26, A56, A57 .= [F,F2] `2 by MCART_1:7 .= ([[F1,F2],t1] `1) `2 .= cod g by A26, A55 ; ::_thesis: verum end; A65: CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is associative proof A66: for f, g being Element of the carrier' of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds ( [g,f] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) iff dom g = cod f ) by A41, CAT_1:def_6; let f, g, h be Element of the carrier' of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def_8 ::_thesis: ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f ) reconsider f9 = f, g9 = g, h9 = h as Element of NatTrans (A,B) ; assume that A67: dom h = cod g and A68: dom g = cod f ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f [g9,f9] in dom m by A41, CAT_1:def_6, A68; then consider F1, F19, F2 being Functor of A,B, t1 being natural_transformation of F1,F19, t2 being natural_transformation of F19,F2 such that A69: f9 = [[F1,F19],t1] and A70: g9 = [[F19,F2],t2] and A71: m . (g9,f9) = [[F1,F2],(t2 `*` t1)] by A20; [h9,g9] in dom m by A41, CAT_1:def_6, A67; then consider F29, F3, F39 being Functor of A,B, t29 being natural_transformation of F29,F3, t3 being natural_transformation of F3,F39 such that A72: g9 = [[F29,F3],t29] and A73: h9 = [[F3,F39],t3] and m . (h9,g9) = [[F29,F39],(t3 `*` t29)] by A20; A74: [F29,F3] = [F19,F2] by A70, A72, XTUPLE_0:1; then A75: g9 = [[F19,F3],t2] by A70, XTUPLE_0:1; reconsider t2 = t2 as natural_transformation of F19,F3 by A74, XTUPLE_0:1; A76: F2 = F3 by A74, XTUPLE_0:1; then A77: F19 is_naturally_transformable_to F3 by A70, Th32; A78: F3 is_naturally_transformable_to F39 by A73, Th32; then A79: F19 is_naturally_transformable_to F39 by A77, Th23; A80: F1 is_naturally_transformable_to F19 by A69, Th32; then A81: F1 is_naturally_transformable_to F3 by A77, Th23; A82: h (*) g = the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (h,g) by A66, A67, CAT_1:def_1; A83: dom (h (*) g) = dom g by A50, CAT_1:def_7, A67; A84: g (*) f = the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (g,f) by A66, A68, CAT_1:def_1; cod (g (*) f) = cod g by A50, CAT_1:def_7, A68; hence h (*) (g (*) f) = the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (h,( the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (g,f))) by A84, A66, A67, CAT_1:def_1 .= [[F1,F39],(t3 `*` (t2 `*` t1))] by A29, A71, A73, A76, A78, A81 .= [[F1,F39],((t3 `*` t2) `*` t1)] by A80, A77, A78, Th26 .= m . [[[F19,F39],(t3 `*` t2)],f9] by A29, A69, A80, A79 .= the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (( the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (h,g)),f) by A29, A73, A75, A77, A78 .= (h (*) g) (*) f by A83, A82, A66, A68, CAT_1:def_1 ; ::_thesis: verum end; A85: CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is reflexive proof let b be Element of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def_9 ::_thesis: not Hom (b,b) = {} reconsider F = b as Functor of A,B by CAT_2:def_2; reconsider s = [[F,F],(id F)] as Element of NatTrans (A,B) by Def16; reconsider s = s as Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ; A86: dom s = ([[F,F],(id F)] `1) `1 by A23 .= F ; cod s = ([[F,F],(id F)] `1) `2 by A26 .= F ; then s in Hom (b,b) by A86; hence Hom (b,b) <> {} ; ::_thesis: verum end; A87: for a being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) for F being Functor of A,B st a = F holds for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) proof let a be Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); ::_thesis: for F being Functor of A,B st a = F holds for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) let F be Functor of A,B; ::_thesis: ( a = F implies for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) ) assume A88: a = F ; ::_thesis: for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) let ii be Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); ::_thesis: ( ii = [[F,F],(id F)] implies for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) 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 ) ) ) assume A89: ii = [[F,F],(id F)] ; ::_thesis: for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) 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 ) ) let b be Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); ::_thesis: ( ( 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 ) ) reconsider s = [[F,F],(id F)] as Element of NatTrans (A,B) by Def16; A90: F in Funct (A,B) by CAT_2:def_2; then A91: i . F = [[F,F],(id F)] by A28; thus ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) proof assume A92: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds f (*) ii = f let f be Morphism of a,b; ::_thesis: f (*) ii = f reconsider f9 = f as Element of NatTrans (A,B) ; A93: dom f = a by A92, CAT_1:5; consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that A94: f9 = [[F1,F2],t] and F1 is_naturally_transformable_to F2 by Def16; A95: F1 = [F1,F2] `1 .= (f9 `1) `1 by A94, MCART_1:7 .= dom f by A23 .= F by A92, CAT_1:5, A88 ; then reconsider t = t as natural_transformation of F,F2 ; S1[f9,s,[[F,F2],(t `*` (id F))]] by A94, A95; then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that A96: i . F = [[F9,F19],t9] and A97: f9 = [[F19,F29],t19] and A98: m . (f9,(i . F)) = [[F9,F29],(t19 `*` t9)] by A20, A91, A19; A99: [F9,F19] = [F,F] by A96, A91, XTUPLE_0:1; then A100: F9 = F by XTUPLE_0:1; A101: F19 = F by A99, XTUPLE_0:1; A102: F19 is_naturally_transformable_to F29 by A97, Th32; A103: F29 = ([[F19,F29],t19] `1) `2 .= ([[F1,F2],t] `1) `2 by A97, A94 .= F2 ; A104: t19 = [[F19,F29],t19] `2 .= [[F1,F2],t] `2 by A97, A94 .= t ; A105: t19 `*` (id F19) = t19 by Th24, A102; cod ii = ([[F,F],(id F)] `1) `2 by A89, A26 .= a by A88 ; then [f,ii] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) by A41, CAT_1:def_6, A93; hence f (*) ii = m . (f,ii) by CAT_1:def_1 .= f by A104, A105, A95, A103, XTUPLE_0:1, A96, A91, A100, A101, A98, A89, A94 ; ::_thesis: verum end; assume A106: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds ii (*) f = f let f be Morphism of b,a; ::_thesis: ii (*) f = f reconsider f9 = f as Element of NatTrans (A,B) ; A107: cod f = a by A106, CAT_1:5; consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that A108: f9 = [[F1,F2],t] and F1 is_naturally_transformable_to F2 by Def16; A109: F2 = [F1,F2] `2 .= (f9 `1) `2 by A108, MCART_1:7 .= cod f by A26 .= F by A106, CAT_1:5, A88 ; then reconsider t = t as natural_transformation of F1,F ; S1[s,f9,[[F1,F],((id F) `*` t)]] by A108, A109; then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that A110: f9 = [[F9,F19],t9] and A111: i . F = [[F19,F29],t19] and A112: m . ((i . F),f9) = [[F9,F29],(t19 `*` t9)] by A20, A91, A19; A113: t19 = id F by A111, XTUPLE_0:1, A91; A114: [F19,F29] = [F,F] by A111, A91, XTUPLE_0:1; then A115: F19 = F by XTUPLE_0:1; A116: F9 is_naturally_transformable_to F19 by A110, Th32; A117: F9 = ([[F9,F19],t9] `1) `1 .= ([[F1,F2],t] `1) `1 by A110, A108 .= F1 ; A118: t9 = [[F9,F19],t9] `2 .= [[F1,F2],t] `2 by A110, A108 .= t ; A119: (id F19) `*` t9 = t9 by Th24, A116; dom ii = ([[F,F],(id F)] `1) `1 by A89, A23 .= a by A88 ; then [ii,f] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) by A41, CAT_1:def_6, A107; hence ii (*) f = m . (ii,f) by CAT_1:def_1 .= m . ((i . F),f9) by A89, A90, A28 .= [[F9,F29],((id F19) `*` t9)] by A113, A115, A114, XTUPLE_0:1, A112 .= f by A108, A118, A119, A114, A109, A117, XTUPLE_0:1 ; ::_thesis: verum end; CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is with_identities proof let a be Element of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st for b2 being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds ( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) ) reconsider F = a as Functor of A,B by CAT_2:def_2; reconsider s = [[F,F],(id F)] as Element of NatTrans (A,B) by Def16; reconsider s = s as Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ; A120: dom s = ([[F,F],(id F)] `1) `1 by A23 .= F ; cod s = ([[F,F],(id F)] `1) `2 by A26 .= F ; then s in Hom (a,a) by A120; then reconsider s = s as Morphism of a,a by CAT_1:def_5; take s ; ::_thesis: for b1 being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) s = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds s (*) b2 = b2 ) ) thus for b1 being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) s = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds s (*) b2 = b2 ) ) by A87; ::_thesis: verum end; then reconsider C = CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) as strict Category by A41, A50, A65, A85; take C ; ::_thesis: ( the carrier of C = Funct (A,B) & the carrier' of C = NatTrans (A,B) & ( for f being Morphism of C holds ( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C st dom g = cod f holds [g,f] in dom the Comp of C ) & ( for f, g being Morphism of C st [g,f] in dom the Comp of C holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) ) thus ( the carrier of C = Funct (A,B) & the carrier' of C = NatTrans (A,B) ) ; ::_thesis: ( ( for f being Morphism of C holds ( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C st dom g = cod f holds [g,f] in dom the Comp of C ) & ( for f, g being Morphism of C st [g,f] in dom the Comp of C holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) ) thus for f being Morphism of C holds ( dom f = (f `1) `1 & cod f = (f `1) `2 ) by A23, A26; ::_thesis: ( ( for f, g being Morphism of C st dom g = cod f holds [g,f] in dom the Comp of C ) & ( for f, g being Morphism of C st [g,f] in dom the Comp of C holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) ) thus for f, g being Morphism of C st dom g = cod f holds [g,f] in dom the Comp of C ::_thesis: ( ( for f, g being Morphism of C st [g,f] in dom the Comp of C holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) ) proof let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies [g,f] in dom the Comp of C ) assume A121: dom g = cod f ; ::_thesis: [g,f] in dom the Comp of C consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that A122: g = [[F19,F29],t9] and F19 is_naturally_transformable_to F29 by Def16; consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that A123: f = [[F1,F2],t] and F1 is_naturally_transformable_to F2 by Def16; A124: F2 = ([[F1,F2],t] `1) `2 .= cod f by A26, A123 .= ([[F19,F29],t9] `1) `1 by A23, A122, A121 .= F19 ; then reconsider t9 = t9 as natural_transformation of F2,F29 ; S1[g,f,[[F1,F29],(t9 `*` t)]] by A123, A122, A124; hence [g,f] in dom the Comp of C by A19; ::_thesis: verum end; thus for f, g being Morphism of C st [g,f] in dom the Comp of C holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ::_thesis: for a being Object of C for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] proof let f, g be Morphism of C; ::_thesis: ( [g,f] in dom the Comp of C implies ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ) assume [g,f] in dom the Comp of C ; ::_thesis: ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) then ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . (g,f) = [[F,F2],(t1 `*` t)] ) by A20; hence ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ; ::_thesis: verum end; let a be Object of C; ::_thesis: for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] let F be Functor of A,B; ::_thesis: ( F = a implies id a = [[F,F],(id F)] ) assume A125: a = F ; ::_thesis: id a = [[F,F],(id F)] reconsider m = [[F,F],(id F)] as Element of NatTrans (A,B) by Def16; reconsider m = m as Morphism of C ; A126: dom m = ([[F,F],(id F)] `1) `1 by A23 .= F ; cod m = ([[F,F],(id F)] `1) `2 by A26 .= F ; then m in Hom (a,a) by A125, A126; then reconsider m = m as Morphism of a,a by CAT_1:def_5; for b being Object of C holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) by A125, A87; hence id a = [[F,F],(id F)] by CAT_1:def_12; ::_thesis: verum end; uniqueness for b1, b2 being strict Category st the carrier of b1 = Funct (A,B) & the carrier' of b1 = NatTrans (A,B) & ( for f being Morphism of b1 holds ( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b1 st dom g = cod f holds [g,f] in dom the Comp of b1 ) & ( for f, g being Morphism of b1 st [g,f] in dom the Comp of b1 holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b1 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b1 for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) & the carrier of b2 = Funct (A,B) & the carrier' of b2 = NatTrans (A,B) & ( for f being Morphism of b2 holds ( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b2 st dom g = cod f holds [g,f] in dom the Comp of b2 ) & ( for f, g being Morphism of b2 st [g,f] in dom the Comp of b2 holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b2 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b2 for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) holds b1 = b2 proof let C1, C2 be strict Category; ::_thesis: ( the carrier of C1 = Funct (A,B) & the carrier' of C1 = NatTrans (A,B) & ( for f being Morphism of C1 holds ( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C1 st dom g = cod f holds [g,f] in dom the Comp of C1 ) & ( for f, g being Morphism of C1 st [g,f] in dom the Comp of C1 holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C1 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C1 for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) & the carrier of C2 = Funct (A,B) & the carrier' of C2 = NatTrans (A,B) & ( for f being Morphism of C2 holds ( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C2 st dom g = cod f holds [g,f] in dom the Comp of C2 ) & ( for f, g being Morphism of C2 st [g,f] in dom the Comp of C2 holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C2 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C2 for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) implies C1 = C2 ) assume that A127: the carrier of C1 = Funct (A,B) and A128: the carrier' of C1 = NatTrans (A,B) and A129: for f being Morphism of C1 holds ( dom f = (f `1) `1 & cod f = (f `1) `2 ) and A130: for f, g being Morphism of C1 st dom g = cod f holds [g,f] in dom the Comp of C1 and A131: for f, g being Morphism of C1 st [g,f] in dom the Comp of C1 holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C1 . [g,f] = [[F,F2],(t1 `*` t)] ) and for a being Object of C1 for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] and A132: the carrier of C2 = Funct (A,B) and A133: the carrier' of C2 = NatTrans (A,B) and A134: for f being Morphism of C2 holds ( dom f = (f `1) `1 & cod f = (f `1) `2 ) and A135: for f, g being Morphism of C2 st dom g = cod f holds [g,f] in dom the Comp of C2 and A136: for f, g being Morphism of C2 st [g,f] in dom the Comp of C2 holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C2 . [g,f] = [[F,F2],(t1 `*` t)] ) and for a being Object of C2 for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ; ::_thesis: C1 = C2 A137: the Target of C1 = the Target of C2 proof thus the carrier' of C1 = the carrier' of C2 by A128, A133; :: according to FUNCT_2:def_7 ::_thesis: for b1 being Element of the carrier' of C1 holds the Target of C1 . b1 = the Target of C2 . b1 let a be Morphism of C1; ::_thesis: the Target of C1 . a = the Target of C2 . a reconsider b = a as Morphism of C2 by A128, A133; thus the Target of C1 . a = cod a .= (a `1) `2 by A129 .= cod b by A134 .= the Target of C2 . a ; ::_thesis: verum end; A138: now__::_thesis:_(_dom_the_Comp_of_C1_=_dom_the_Comp_of_C2_&_(_for_x_being_set_st_x_in_dom_the_Comp_of_C1_holds_ the_Comp_of_C1_._x_=_the_Comp_of_C2_._x_)_) reconsider S1 = dom the Comp of C1, S2 = dom the Comp of C2 as Subset of [: the carrier' of C1, the carrier' of C1:] by A128, A133, RELAT_1:def_18; A139: now__::_thesis:_for_x_being_Element_of_[:_the_carrier'_of_C1,_the_carrier'_of_C1:]_holds_ (_x_in_S1_iff_x_in_S2_) let x be Element of [: the carrier' of C1, the carrier' of C1:]; ::_thesis: ( x in S1 iff x in S2 ) A140: x = [(x `1),(x `2)] by MCART_1:21; then reconsider f1 = x `2 , g1 = x `1 as Morphism of C1 by ZFMISC_1:87; reconsider f2 = x `2 , g2 = x `1 as Morphism of C2 by A128, A133, A140, ZFMISC_1:87; A141: now__::_thesis:_(_[g2,f2]_in_S2_implies_[g1,f1]_in_S1_) assume [g2,f2] in S2 ; ::_thesis: [g1,f1] in S1 then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that A142: f2 = [[F,F1],t] and A143: g2 = [[F1,F2],t1] and the Comp of C2 . [g2,f2] = [[F,F2],(t1 `*` t)] by A136; dom g1 = (g1 `1) `1 by A129 .= [F1,F2] `1 by A143, MCART_1:7 .= [F,F1] `2 .= (f2 `1) `2 by A142, MCART_1:7 .= cod f1 by A129 ; hence [g1,f1] in S1 by A130; ::_thesis: verum end; now__::_thesis:_(_[g1,f1]_in_S1_implies_[g2,f2]_in_S2_) assume [g1,f1] in S1 ; ::_thesis: [g2,f2] in S2 then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that A144: f1 = [[F,F1],t] and A145: g1 = [[F1,F2],t1] and the Comp of C1 . [g1,f1] = [[F,F2],(t1 `*` t)] by A131; dom g2 = (g2 `1) `1 by A134 .= [F1,F2] `1 by A145, MCART_1:7 .= [F,F1] `2 .= (f1 `1) `2 by A144, MCART_1:7 .= cod f2 by A134 ; hence [g2,f2] in S2 by A135; ::_thesis: verum end; hence ( x in S1 iff x in S2 ) by A141, MCART_1:21; ::_thesis: verum end; hence dom the Comp of C1 = dom the Comp of C2 by SUBSET_1:3; ::_thesis: for x being set st x in dom the Comp of C1 holds the Comp of C1 . x = the Comp of C2 . x let x be set ; ::_thesis: ( x in dom the Comp of C1 implies the Comp of C1 . x = the Comp of C2 . x ) assume A146: x in dom the Comp of C1 ; ::_thesis: the Comp of C1 . x = the Comp of C2 . x dom the Comp of C1 c= [: the carrier' of C1, the carrier' of C1:] by RELAT_1:def_18; then reconsider f = x `2 , g = x `1 as Morphism of C1 by A146, MCART_1:10; A147: [g,f] = x by A146, MCART_1:21; then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that A148: f = [[F9,F19],t9] and A149: g = [[F19,F29],t19] and A150: the Comp of C2 . [g,f] = [[F9,F29],(t19 `*` t9)] by A128, A133, A136, A139, A146; consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that A151: f = [[F,F1],t] and A152: g = [[F1,F2],t1] and A153: the Comp of C1 . [g,f] = [[F,F2],(t1 `*` t)] by A131, A146, A147; A154: [F,F1] = [F9,F19] by A151, A148, XTUPLE_0:1; then A155: F = F9 by XTUPLE_0:1; [F1,F2] = [F19,F29] by A152, A149, XTUPLE_0:1; then A156: F2 = F29 by XTUPLE_0:1; A157: F1 = F19 by A154, XTUPLE_0:1; t = t9 by A151, A148, XTUPLE_0:1; hence the Comp of C1 . x = the Comp of C2 . x by A147, A152, A153, A149, A150, A155, A157, A156, XTUPLE_0:1; ::_thesis: verum end; the Source of C1 = the Source of C2 proof thus the carrier' of C1 = the carrier' of C2 by A128, A133; :: according to FUNCT_2:def_7 ::_thesis: for b1 being Element of the carrier' of C1 holds the Source of C1 . b1 = the Source of C2 . b1 let a be Morphism of C1; ::_thesis: the Source of C1 . a = the Source of C2 . a reconsider b = a as Morphism of C2 by A128, A133; thus the Source of C1 . a = dom a .= (a `1) `1 by A129 .= dom b by A134 .= the Source of C2 . a ; ::_thesis: verum end; hence C1 = C2 by A127, A128, A132, A133, A137, A138, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def17 defines Functors NATTRA_1:def_17_:_ for A, B being Category for b3 being strict Category holds ( b3 = Functors (A,B) iff ( the carrier of b3 = Funct (A,B) & the carrier' of b3 = NatTrans (A,B) & ( for f being Morphism of b3 holds ( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b3 st dom g = cod f holds [g,f] in dom the Comp of b3 ) & ( for f, g being Morphism of b3 st [g,f] in dom the Comp of b3 holds ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b3 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b3 for F being Functor of A,B st F = a holds id a = [[F,F],(id F)] ) ) ); theorem Th33: :: NATTRA_1:33 for A, B being Category for F, F1 being Functor of A,B for t being natural_transformation of F,F1 for f being Morphism of (Functors (A,B)) st f = [[F,F1],t] holds ( dom f = F & cod f = F1 ) proof let A, B be Category; ::_thesis: for F, F1 being Functor of A,B for t being natural_transformation of F,F1 for f being Morphism of (Functors (A,B)) st f = [[F,F1],t] holds ( dom f = F & cod f = F1 ) let F, F1 be Functor of A,B; ::_thesis: for t being natural_transformation of F,F1 for f being Morphism of (Functors (A,B)) st f = [[F,F1],t] holds ( dom f = F & cod f = F1 ) let t be natural_transformation of F,F1; ::_thesis: for f being Morphism of (Functors (A,B)) st f = [[F,F1],t] holds ( dom f = F & cod f = F1 ) let f be Morphism of (Functors (A,B)); ::_thesis: ( f = [[F,F1],t] implies ( dom f = F & cod f = F1 ) ) assume A1: f = [[F,F1],t] ; ::_thesis: ( dom f = F & cod f = F1 ) thus dom f = (f `1) `1 by Def17 .= [F,F1] `1 by A1, MCART_1:7 .= F ; ::_thesis: cod f = F1 thus cod f = (f `1) `2 by Def17 .= [F,F1] `2 by A1, MCART_1:7 .= F1 ; ::_thesis: verum end; theorem :: NATTRA_1:34 for A, B being Category for a, b being Object of (Functors (A,B)) for f being Morphism of a,b st Hom (a,b) <> {} holds ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st ( a = F & b = F1 & f = [[F,F1],t] ) proof let A, B be Category; ::_thesis: for a, b being Object of (Functors (A,B)) for f being Morphism of a,b st Hom (a,b) <> {} holds ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st ( a = F & b = F1 & f = [[F,F1],t] ) let a, b be Object of (Functors (A,B)); ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st ( a = F & b = F1 & f = [[F,F1],t] ) let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st ( a = F & b = F1 & f = [[F,F1],t] ) ) assume A1: Hom (a,b) <> {} ; ::_thesis: ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st ( a = F & b = F1 & f = [[F,F1],t] ) the carrier' of (Functors (A,B)) = NatTrans (A,B) by Def17; then consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that A2: f = [[F1,F2],t] and F1 is_naturally_transformable_to F2 by Def15; take F1 ; ::_thesis: ex F1 being Functor of A,B ex t being natural_transformation of F1,F1 st ( a = F1 & b = F1 & f = [[F1,F1],t] ) take F2 ; ::_thesis: ex t being natural_transformation of F1,F2 st ( a = F1 & b = F2 & f = [[F1,F2],t] ) take t ; ::_thesis: ( a = F1 & b = F2 & f = [[F1,F2],t] ) thus a = dom f by A1, CAT_1:5 .= F1 by A2, Th33 ; ::_thesis: ( b = F2 & f = [[F1,F2],t] ) thus b = cod f by A1, CAT_1:5 .= F2 by A2, Th33 ; ::_thesis: f = [[F1,F2],t] thus f = [[F1,F2],t] by A2; ::_thesis: verum end; theorem Th35: :: NATTRA_1:35 for A, B being Category for F2, F3, F, F1 being Functor of A,B for t being natural_transformation of F,F1 for t9 being natural_transformation of F2,F3 for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds ( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 ) proof let A, B be Category; ::_thesis: for F2, F3, F, F1 being Functor of A,B for t being natural_transformation of F,F1 for t9 being natural_transformation of F2,F3 for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds ( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 ) let F2, F3, F, F1 be Functor of A,B; ::_thesis: for t being natural_transformation of F,F1 for t9 being natural_transformation of F2,F3 for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds ( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 ) let t be natural_transformation of F,F1; ::_thesis: for t9 being natural_transformation of F2,F3 for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds ( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 ) let t9 be natural_transformation of F2,F3; ::_thesis: for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds ( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 ) let f, g be Morphism of (Functors (A,B)); ::_thesis: ( f = [[F,F1],t] & g = [[F2,F3],t9] implies ( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 ) ) assume that A1: f = [[F,F1],t] and A2: g = [[F2,F3],t9] ; ::_thesis: ( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 ) thus ( [g,f] in dom the Comp of (Functors (A,B)) implies F1 = F2 ) ::_thesis: ( F1 = F2 implies [g,f] in dom the Comp of (Functors (A,B)) ) proof assume [g,f] in dom the Comp of (Functors (A,B)) ; ::_thesis: F1 = F2 then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that A3: f = [[F9,F19],t9] and A4: g = [[F19,F29],t19] and the Comp of (Functors (A,B)) . [g,f] = [[F9,F29],(t19 `*` t9)] by Def17; thus F1 = ([[F,F1],t] `1) `2 .= [F9,F19] `2 by A1, A3, MCART_1:7 .= ([[F19,F29],t19] `1) `1 .= [F2,F3] `1 by A2, A4, MCART_1:7 .= F2 ; ::_thesis: verum end; A5: cod f = F1 by A1, Th33; dom g = F2 by A2, Th33; hence ( F1 = F2 implies [g,f] in dom the Comp of (Functors (A,B)) ) by A5, Def17; ::_thesis: verum end; theorem :: NATTRA_1:36 for A, B being Category for F, F1, F2 being Functor of A,B for t being natural_transformation of F,F1 for t1 being natural_transformation of F1,F2 for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds g (*) f = [[F,F2],(t1 `*` t)] proof let A, B be Category; ::_thesis: for F, F1, F2 being Functor of A,B for t being natural_transformation of F,F1 for t1 being natural_transformation of F1,F2 for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds g (*) f = [[F,F2],(t1 `*` t)] let F, F1, F2 be Functor of A,B; ::_thesis: for t being natural_transformation of F,F1 for t1 being natural_transformation of F1,F2 for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds g (*) f = [[F,F2],(t1 `*` t)] let t be natural_transformation of F,F1; ::_thesis: for t1 being natural_transformation of F1,F2 for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds g (*) f = [[F,F2],(t1 `*` t)] let t1 be natural_transformation of F1,F2; ::_thesis: for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds g (*) f = [[F,F2],(t1 `*` t)] let f, g be Morphism of (Functors (A,B)); ::_thesis: ( f = [[F,F1],t] & g = [[F1,F2],t1] implies g (*) f = [[F,F2],(t1 `*` t)] ) assume that A1: f = [[F,F1],t] and A2: g = [[F1,F2],t1] ; ::_thesis: g (*) f = [[F,F2],(t1 `*` t)] A3: [g,f] in dom the Comp of (Functors (A,B)) by A1, A2, Th35; then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that A4: f = [[F9,F19],t9] and A5: g = [[F19,F29],t19] and A6: the Comp of (Functors (A,B)) . (g,f) = [[F9,F29],(t19 `*` t9)] by Def17; A7: t1 = t19 by A2, A5, XTUPLE_0:1; A8: [F9,F19] = [F,F1] by A1, A4, XTUPLE_0:1; then A9: F = F9 by XTUPLE_0:1; [F19,F29] = [F1,F2] by A2, A5, XTUPLE_0:1; then A10: F2 = F29 by XTUPLE_0:1; A11: F1 = F19 by A8, XTUPLE_0:1; t = t9 by A1, A4, XTUPLE_0:1; hence g (*) f = [[F,F2],(t1 `*` t)] by A3, A6, A7, A9, A11, A10, CAT_1:def_1; ::_thesis: verum end; begin definition let C be Category; attrC is discrete means :Def18: :: NATTRA_1:def 18 for f being Morphism of C ex a being Object of C st f = id a; end; :: deftheorem Def18 defines discrete NATTRA_1:def_18_:_ for C being Category holds ( C is discrete iff for f being Morphism of C ex a being Object of C st f = id a ); registration cluster non empty non void V55() Category-like transitive associative reflexive with_identities discrete for CatStr ; existence ex b1 being Category st b1 is discrete proof set o = the set ; take 1Cat ( the set , the set ) ; ::_thesis: 1Cat ( the set , the set ) is discrete let f be Morphism of (1Cat ( the set , the set )); :: according to NATTRA_1:def_18 ::_thesis: ex a being Object of (1Cat ( the set , the set )) st f = id a set a = the Object of (1Cat ( the set , the set )); take the Object of (1Cat ( the set , the set )) ; ::_thesis: f = id the Object of (1Cat ( the set , the set )) thus f = the set by TARSKI:def_1 .= id the Object of (1Cat ( the set , the set )) by TARSKI:def_1 ; ::_thesis: verum end; end; theorem Th37: :: NATTRA_1:37 for A being discrete Category for a being Object of A holds Hom (a,a) = {(id a)} proof let A be discrete Category; ::_thesis: for a being Object of A holds Hom (a,a) = {(id a)} let a be Object of A; ::_thesis: Hom (a,a) = {(id a)} A1: Hom (a,a) <> {} ; now__::_thesis:_for_g_being_Morphism_of_a,a_holds_id_a_=_g let g be Morphism of a,a; ::_thesis: id a = g consider a2 being Object of A such that A2: g = id a2 by Def18; a = dom g by A1, CAT_1:5 .= a2 by A2, CAT_1:58 ; hence id a = g by A2; ::_thesis: verum end; hence Hom (a,a) = {(id a)} by CAT_1:8; ::_thesis: verum end; theorem Th38: :: NATTRA_1:38 for A being Category holds ( A is discrete iff ( ( for a being Object of A ex B being finite set st ( B = Hom (a,a) & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds Hom (a,b) = {} ) ) ) proof let A be Category; ::_thesis: ( A is discrete iff ( ( for a being Object of A ex B being finite set st ( B = Hom (a,a) & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds Hom (a,b) = {} ) ) ) thus ( A is discrete implies ( ( for a being Object of A ex B being finite set st ( B = Hom (a,a) & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds Hom (a,b) = {} ) ) ) ::_thesis: ( ( for a being Object of A ex B being finite set st ( B = Hom (a,a) & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds Hom (a,b) = {} ) implies A is discrete ) proof assume A1: A is discrete ; ::_thesis: ( ( for a being Object of A ex B being finite set st ( B = Hom (a,a) & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds Hom (a,b) = {} ) ) hereby ::_thesis: for a, b being Object of A st a <> b holds Hom (a,b) = {} let a be Object of A; ::_thesis: ex B being finite set st ( B = Hom (a,a) & card B = 1 ) A2: Hom (a,a) = {(id a)} by A1, Th37; then reconsider B = Hom (a,a) as finite set ; take B = B; ::_thesis: ( B = Hom (a,a) & card B = 1 ) thus B = Hom (a,a) ; ::_thesis: card B = 1 thus card B = 1 by A2, CARD_1:30; ::_thesis: verum end; let a, b be Object of A; ::_thesis: ( a <> b implies Hom (a,b) = {} ) assume A3: a <> b ; ::_thesis: Hom (a,b) = {} set m = the Element of Hom (a,b); assume A4: Hom (a,b) <> {} ; ::_thesis: contradiction then reconsider m = the Element of Hom (a,b) as Morphism of A by TARSKI:def_3; consider c being Object of A such that A5: m = id c by A1, Def18; id c in Hom (c,c) by CAT_1:27; then A6: Hom (c,c) meets Hom (a,b) by A4, A5, XBOOLE_0:3; then c = a by Th17; hence contradiction by A3, A6, Th17; ::_thesis: verum end; assume that A7: for a being Object of A ex B being finite set st ( B = Hom (a,a) & card B = 1 ) and A8: for a, b being Object of A st a <> b holds Hom (a,b) = {} ; ::_thesis: A is discrete let f be Morphism of A; :: according to NATTRA_1:def_18 ::_thesis: ex a being Object of A st f = id a ex B being finite set st ( B = Hom ((dom f),(dom f)) & card B = 1 ) by A7; then consider x being set such that A9: Hom ((dom f),(dom f)) = {x} by CARD_2:42; take dom f ; ::_thesis: f = id (dom f) A10: id (dom f) in Hom ((dom f),(dom f)) by CAT_1:27; Hom ((dom f),(cod f)) <> {} by CAT_1:2; then dom f = cod f by A8; then f in Hom ((dom f),(dom f)) ; then f = x by A9, TARSKI:def_1; hence f = id (dom f) by A9, A10, TARSKI:def_1; ::_thesis: verum end; theorem Th39: :: NATTRA_1:39 for o, m being set holds 1Cat (o,m) is discrete proof let o, m be set ; ::_thesis: 1Cat (o,m) is discrete let f be Morphism of (1Cat (o,m)); :: according to NATTRA_1:def_18 ::_thesis: ex a being Object of (1Cat (o,m)) st f = id a set a = the Object of (1Cat (o,m)); f = m by TARSKI:def_1 .= id the Object of (1Cat (o,m)) by TARSKI:def_1 ; hence ex a being Object of (1Cat (o,m)) st f = id a ; ::_thesis: verum end; theorem :: NATTRA_1:40 for A being discrete Category for C being Subcategory of A holds C is discrete proof let A be discrete Category; ::_thesis: for C being Subcategory of A holds C is discrete let C be Subcategory of A; ::_thesis: C is discrete let f be Morphism of C; :: according to NATTRA_1:def_18 ::_thesis: ex a being Object of C st f = id a reconsider f9 = f as Morphism of A by CAT_2:8; take dom f ; ::_thesis: f = id (dom f) consider a9 being Object of A such that A1: f9 = id a9 by Def18; dom f9 = a9 by A1, CAT_1:58; then dom f = a9 by CAT_2:9; hence f = id (dom f) by A1, CAT_2:def_4; ::_thesis: verum end; theorem :: NATTRA_1:41 for A, B being Category st A is discrete & B is discrete holds [:A,B:] is discrete proof let A, B be Category; ::_thesis: ( A is discrete & B is discrete implies [:A,B:] is discrete ) assume that A1: A is discrete and A2: B is discrete ; ::_thesis: [:A,B:] is discrete let f be Morphism of [:A,B:]; :: according to NATTRA_1:def_18 ::_thesis: ex a being Object of [:A,B:] st f = id a consider f1 being Morphism of A, f2 being Morphism of B such that A3: f = [f1,f2] by DOMAIN_1:1; consider b being Object of B such that A4: f2 = id b by A2, Def18; consider a being Object of A such that A5: f1 = id a by A1, Def18; take [a,b] ; ::_thesis: f = id [a,b] thus f = id [a,b] by A3, A5, A4, CAT_2:31; ::_thesis: verum end; theorem Th42: :: NATTRA_1:42 for A being discrete Category for B being Category for F1, F2 being Functor of B,A st F1 is_transformable_to F2 holds F1 = F2 proof let A be discrete Category; ::_thesis: for B being Category for F1, F2 being Functor of B,A st F1 is_transformable_to F2 holds F1 = F2 let B be Category; ::_thesis: for F1, F2 being Functor of B,A st F1 is_transformable_to F2 holds F1 = F2 let F1, F2 be Functor of B,A; ::_thesis: ( F1 is_transformable_to F2 implies F1 = F2 ) assume A1: F1 is_transformable_to F2 ; ::_thesis: F1 = F2 now__::_thesis:_for_m_being_Morphism_of_B_holds_F1_._m_=_F2_._m let m be Morphism of B; ::_thesis: F1 . m = F2 . m Hom ((F1 . (dom m)),(F2 . (dom m))) <> {} by A1, Def2; then A2: F1 . (dom m) = F2 . (dom m) by Th38; A3: m in Hom ((dom m),(cod m)) ; then Hom ((F1 . (dom m)),(F1 . (cod m))) <> {} by CAT_1:81; then F1 . (dom m) = F1 . (cod m) by Th38; then A4: Hom ((F1 . (dom m)),(F1 . (cod m))) = {(id (F1 . (dom m)))} by Th37; Hom ((F2 . (dom m)),(F2 . (cod m))) <> {} by A3, CAT_1:81; then F2 . (dom m) = F2 . (cod m) by Th38; then A5: Hom ((F2 . (dom m)),(F2 . (cod m))) = {(id (F2 . (dom m)))} by Th37; F1 . m in Hom ((F1 . (dom m)),(F1 . (cod m))) by A3, CAT_1:81; then A6: F1 . m = id (F1 . (dom m)) by A4, TARSKI:def_1; F2 . m in Hom ((F2 . (dom m)),(F2 . (cod m))) by A3, CAT_1:81; hence F1 . m = F2 . m by A2, A6, A5, TARSKI:def_1; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; theorem Th43: :: NATTRA_1:43 for A being discrete Category for B being Category for F being Functor of B,A for t being transformation of F,F holds t = id F proof let A be discrete Category; ::_thesis: for B being Category for F being Functor of B,A for t being transformation of F,F holds t = id F let B be Category; ::_thesis: for F being Functor of B,A for t being transformation of F,F holds t = id F let F be Functor of B,A; ::_thesis: for t being transformation of F,F holds t = id F let t be transformation of F,F; ::_thesis: t = id F now__::_thesis:_for_a_being_Object_of_B_holds_t_._a_=_(id_F)_._a let a be Object of B; ::_thesis: t . a = (id F) . a A1: Hom ((F . a),(F . a)) = {(id (F . a))} by Th37; t . a in Hom ((F . a),(F . a)) by CAT_1:def_5; hence t . a = id (F . a) by A1, TARSKI:def_1 .= (id F) . a by Th20 ; ::_thesis: verum end; hence t = id F by Th19; ::_thesis: verum end; theorem :: NATTRA_1:44 for A, B being Category st A is discrete holds Functors (B,A) is discrete proof let A, B be Category; ::_thesis: ( A is discrete implies Functors (B,A) is discrete ) assume A1: A is discrete ; ::_thesis: Functors (B,A) is discrete let f be Morphism of (Functors (B,A)); :: according to NATTRA_1:def_18 ::_thesis: ex a being Object of (Functors (B,A)) st f = id a f in the carrier' of (Functors (B,A)) ; then f in NatTrans (B,A) by Def17; then consider F1, F2 being Functor of B,A, t being natural_transformation of F1,F2 such that A2: f = [[F1,F2],t] and A3: F1 is_naturally_transformable_to F2 by Def16; F1 in Funct (B,A) by CAT_2:def_2; then reconsider a = F1 as Object of (Functors (B,A)) by Def17; take a ; ::_thesis: f = id a A4: F1 = F2 by A1, Th42, A3, Def7; then t = id F1 by A1, Th43; hence f = id a by A2, A4, Def17; ::_thesis: verum end; registration let C be Category; cluster non empty non void V55() strict Category-like transitive associative reflexive with_identities discrete for Subcategory of C; existence ex b1 being Subcategory of C st ( b1 is strict & b1 is discrete ) proof set c = the Object of C; reconsider A = 1Cat ( the Object of C,(id the Object of C)) as Subcategory of C by Th7; take A ; ::_thesis: ( A is strict & A is discrete ) thus ( A is strict & A is discrete ) by Th39; ::_thesis: verum end; end; definition let C be Category; func IdCat C -> strict discrete Subcategory of C means :Def19: :: NATTRA_1:def 19 ( the carrier of it = the carrier of C & the carrier' of it = { (id a) where a is Object of C : verum } ); existence ex b1 being strict discrete Subcategory of C st ( the carrier of b1 = the carrier of C & the carrier' of b1 = { (id a) where a is Object of C : verum } ) proof defpred S1[ Object of C] means verum; deffunc H1( Object of C) -> Morphism of $1,$1 = id $1; defpred S2[ Object of C] means H1($1) in the carrier' of C; set M = { H1(a) where a is Object of C : S1[a] } ; set N = { H1(a) where a is Object of C : S2[a] } ; set N9 = { H1(a) where a is Object of C : ( H1(a) in the carrier' of C & S1[a] ) } ; defpred S3[ Object of C] means ( H1($1) in the carrier' of C & S1[$1] ); set N99 = { H1(a) where a is Object of C : S3[a] } ; set a = the Object of C; A1: id the Object of C in { H1(a) where a is Object of C : S1[a] } ; A2: for a being Object of C holds ( S2[a] iff S1[a] ) ; A3: { H1(a) where a is Object of C : S2[a] } = { H1(a) where a is Object of C : S1[a] } from FRAENKEL:sch_3(A2); A4: for a being Object of C holds ( S2[a] iff S3[a] ) ; A5: { H1(a) where a is Object of C : S2[a] } = { H1(a) where a is Object of C : S3[a] } from FRAENKEL:sch_3(A4); { H1(a) where a is Object of C : ( H1(a) in the carrier' of C & S1[a] ) } c= the carrier' of C from FRAENKEL:sch_17(); then reconsider M = { H1(a) where a is Object of C : S1[a] } as non empty Subset of the carrier' of C by A3, A5, A1; A6: rng ( the Comp of C || M) c= M proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ( the Comp of C || M) or x in M ) assume x in rng ( the Comp of C || M) ; ::_thesis: x in M then consider y being set such that A7: y in dom ( the Comp of C || M) and A8: x = ( the Comp of C || M) . y by FUNCT_1:def_3; A9: y in (dom the Comp of C) /\ [:M,M:] by A7, RELAT_1:61; then A10: y in dom the Comp of C by XBOOLE_0:def_4; y in [:M,M:] by A9, XBOOLE_0:def_4; then consider y1, y2 being set such that A11: y1 in M and A12: y2 in M and A13: y = [y1,y2] by ZFMISC_1:84; consider a1 being Object of C such that A14: y1 = id a1 by A11; A15: Hom (a1,a1) <> {} ; consider a2 being Object of C such that A16: y2 = id a2 by A12; A17: a1 = dom (id a1) .= cod (id a2) by A13, A14, A16, A10, CAT_1:15 .= a2 ; id a1 = (id a1) * (id a1) .= (id a1) (*) (id a2) by A15, A17, CAT_1:def_13 .= the Comp of C . ((id a1),(id a2)) by A13, A14, A16, A10, CAT_1:def_1 .= x by A8, A9, A13, A14, A16, FUNCT_1:48 ; hence x in M ; ::_thesis: verum end; the Comp of C || M is PartFunc of [:M,M:], the carrier' of C by PARTFUN1:10; then reconsider COMP = the Comp of C || M as PartFunc of [:M,M:],M by A6, RELSET_1:6; A18: the carrier of C c= the carrier of C ; for o being Element of C st o in the carrier of C holds id o in M ; then reconsider A = CatStr(# the carrier of C,M,( the Source of C | M),( the Target of C | M),COMP #) as Subcategory of C by Th9, A18; now__::_thesis:_for_f_being_Morphism_of_A_ex_a_being_Element_of_A_st_f_=_id_a let f be Morphism of A; ::_thesis: ex a being Element of A st f = id a f in M ; then consider a being Object of C such that A19: f = id a ; reconsider a = a as Element of A ; take a = a; ::_thesis: f = id a thus f = id a by A19, CAT_2:def_4; ::_thesis: verum end; then reconsider A = A as strict discrete Subcategory of C by Def18; take A ; ::_thesis: ( the carrier of A = the carrier of C & the carrier' of A = { (id a) where a is Object of C : verum } ) thus ( the carrier of A = the carrier of C & the carrier' of A = { (id a) where a is Object of C : verum } ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict discrete Subcategory of C st the carrier of b1 = the carrier of C & the carrier' of b1 = { (id a) where a is Object of C : verum } & the carrier of b2 = the carrier of C & the carrier' of b2 = { (id a) where a is Object of C : verum } holds b1 = b2 proof let It1, It2 be strict discrete Subcategory of C; ::_thesis: ( the carrier of It1 = the carrier of C & the carrier' of It1 = { (id a) where a is Object of C : verum } & the carrier of It2 = the carrier of C & the carrier' of It2 = { (id a) where a is Object of C : verum } implies It1 = It2 ) assume that A20: the carrier of It1 = the carrier of C and A21: the carrier' of It1 = { (id a) where a is Object of C : verum } and A22: the carrier of It2 = the carrier of C and A23: the carrier' of It2 = { (id a) where a is Object of C : verum } ; ::_thesis: It1 = It2 set M = the carrier' of It1; A24: the Target of It2 = the Target of C | the carrier' of It1 by A21, A23, Th8; A25: the Comp of It2 = the Comp of C || the carrier' of It1 by A21, A23, Th8; A26: the Source of It1 = the Source of C | the carrier' of It1 by Th8; A27: the Comp of It1 = the Comp of C || the carrier' of It1 by Th8; the Target of It1 = the Target of C | the carrier' of It1 by Th8; hence It1 = It2 by A20, A21, A22, A23, A26, A24, A27, A25, Th8; ::_thesis: verum end; end; :: deftheorem Def19 defines IdCat NATTRA_1:def_19_:_ for C being Category for b2 being strict discrete Subcategory of C holds ( b2 = IdCat C iff ( the carrier of b2 = the carrier of C & the carrier' of b2 = { (id a) where a is Object of C : verum } ) ); theorem Th45: :: NATTRA_1:45 for C being strict Category st C is discrete holds IdCat C = C proof let C be strict Category; ::_thesis: ( C is discrete implies IdCat C = C ) assume A1: C is discrete ; ::_thesis: IdCat C = C the carrier' of C c= { (id a) where a is Object of C : verum } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of C or x in { (id a) where a is Object of C : verum } ) assume x in the carrier' of C ; ::_thesis: x in { (id a) where a is Object of C : verum } then ex a being Object of C st x = id a by A1, Def18; hence x in { (id a) where a is Object of C : verum } ; ::_thesis: verum end; then A2: the carrier' of C c= the carrier' of (IdCat C) by Def19; the carrier' of (IdCat C) c= the carrier' of C by CAT_2:7; then the carrier' of (IdCat C) = the carrier' of C by A2, XBOOLE_0:def_10; hence IdCat C = C by Def19, Th10; ::_thesis: verum end; theorem :: NATTRA_1:46 for C being Category holds IdCat (IdCat C) = IdCat C by Th45; theorem :: NATTRA_1:47 for o, m being set holds IdCat (1Cat (o,m)) = 1Cat (o,m) proof let o, m be set ; ::_thesis: IdCat (1Cat (o,m)) = 1Cat (o,m) 1Cat (o,m) is discrete by Th39; hence IdCat (1Cat (o,m)) = 1Cat (o,m) by Th45; ::_thesis: verum end; theorem :: NATTRA_1:48 for A, B being Category holds IdCat [:A,B:] = [:(IdCat A),(IdCat B):] proof let A, B be Category; ::_thesis: IdCat [:A,B:] = [:(IdCat A),(IdCat B):] now__::_thesis:_(_[:_the_carrier_of_(IdCat_A),_the_carrier_of_(IdCat_B):]_=_the_carrier_of_(IdCat_[:A,B:])_&_the_carrier'_of_(IdCat_[:A,B:])_=_[:_the_carrier'_of_(IdCat_A),_the_carrier'_of_(IdCat_B):]_&_[:_the_Source_of_(IdCat_A),_the_Source_of_(IdCat_B):]_=_the_Source_of_(IdCat_[:A,B:])_&_[:_the_Target_of_(IdCat_A),_the_Target_of_(IdCat_B):]_=_the_Target_of_(IdCat_[:A,B:])_&_|:_the_Comp_of_(IdCat_A),_the_Comp_of_(IdCat_B):|_=_the_Comp_of_(IdCat_[:A,B:])_) reconsider OA = the carrier of (IdCat A) as non empty Subset of the carrier of A by CAT_2:def_4; set AB = { (id c) where c is Object of [:A,B:] : verum } ; set MA = { (id a) where a is Object of A : verum } ; set MB = { (id b) where b is Object of B : verum } ; A1: { (id c) where c is Object of [:A,B:] : verum } = [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] proof thus { (id c) where c is Object of [:A,B:] : verum } c= [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] :: according to XBOOLE_0:def_10 ::_thesis: [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] c= { (id c) where c is Object of [:A,B:] : verum } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (id c) where c is Object of [:A,B:] : verum } or x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] ) assume x in { (id c) where c is Object of [:A,B:] : verum } ; ::_thesis: x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] then consider c being Object of [:A,B:] such that A2: x = id c ; consider c1 being Object of A, c2 being Object of B such that A3: c = [c1,c2] by DOMAIN_1:1; A4: id c2 in { (id b) where b is Object of B : verum } ; A5: id c1 in { (id a) where a is Object of A : verum } ; id c = [(id c1),(id c2)] by A3, CAT_2:31; hence x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] by A2, A5, A4, ZFMISC_1:87; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] or x in { (id c) where c is Object of [:A,B:] : verum } ) assume x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] ; ::_thesis: x in { (id c) where c is Object of [:A,B:] : verum } then consider x1, x2 being set such that A6: x1 in { (id a) where a is Object of A : verum } and A7: x2 in { (id b) where b is Object of B : verum } and A8: x = [x1,x2] by ZFMISC_1:84; consider a being Object of A such that A9: x1 = id a by A6; consider b being Object of B such that A10: x2 = id b by A7; id [a,b] = [(id a),(id b)] by CAT_2:31; hence x in { (id c) where c is Object of [:A,B:] : verum } by A8, A9, A10; ::_thesis: verum end; reconsider OB = the carrier of (IdCat B) as non empty Subset of the carrier of B by CAT_2:def_4; reconsider MB = the carrier' of (IdCat B) as non empty Subset of the carrier' of B by CAT_2:7; reconsider MA = the carrier' of (IdCat A) as non empty Subset of the carrier' of A by CAT_2:7; A11: the carrier of (IdCat B) = the carrier of B by Def19; the carrier of (IdCat A) = the carrier of A by Def19; hence [: the carrier of (IdCat A), the carrier of (IdCat B):] = the carrier of (IdCat [:A,B:]) by A11, Def19; ::_thesis: ( the carrier' of (IdCat [:A,B:]) = [: the carrier' of (IdCat A), the carrier' of (IdCat B):] & [: the Source of (IdCat A), the Source of (IdCat B):] = the Source of (IdCat [:A,B:]) & [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) ) A12: the Target of (IdCat B) = the Target of B | the carrier' of (IdCat B) by Th8; A13: the Source of (IdCat B) = the Source of B | the carrier' of (IdCat B) by Th8; A14: the carrier' of (IdCat B) = { (id b) where b is Object of B : verum } by Def19; the carrier' of (IdCat A) = { (id a) where a is Object of A : verum } by Def19; hence A15: the carrier' of (IdCat [:A,B:]) = [: the carrier' of (IdCat A), the carrier' of (IdCat B):] by A1, A14, Def19; ::_thesis: ( [: the Source of (IdCat A), the Source of (IdCat B):] = the Source of (IdCat [:A,B:]) & [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) ) the Source of (IdCat A) = the Source of A | the carrier' of (IdCat A) by Th8; hence [: the Source of (IdCat A), the Source of (IdCat B):] = [: the Source of A, the Source of B:] | [:MA,MB:] by A13, Th1 .= the Source of (IdCat [:A,B:]) by A15, Th8 ; ::_thesis: ( [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) ) the Target of (IdCat A) = the Target of A | the carrier' of (IdCat A) by Th8; hence [: the Target of (IdCat A), the Target of (IdCat B):] = [: the Target of A, the Target of B:] | [:MA,MB:] by A12, Th1 .= the Target of (IdCat [:A,B:]) by A15, Th8 ; ::_thesis: |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) A16: the Comp of (IdCat A) = the Comp of A || MA by Th8; A17: the Comp of (IdCat B) = the Comp of B || MB by Th8; |: the Comp of A, the Comp of B:| || [:MA,MB:] = the Comp of (IdCat [:A,B:]) by A15, Th8; hence |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) by A16, A17, Th2; ::_thesis: verum end; hence IdCat [:A,B:] = [:(IdCat A),(IdCat B):] ; ::_thesis: verum end;