:: FUNCTOR3 semantic presentation begin registration cluster non empty transitive strict associative with_units for AltCatStr ; existence ex b1 being non empty AltCatStr st ( b1 is transitive & b1 is associative & b1 is with_units & b1 is strict ) proof set A = the non empty transitive strict associative with_units AltCatStr ; take the non empty transitive strict associative with_units AltCatStr ; ::_thesis: ( the non empty transitive strict associative with_units AltCatStr is transitive & the non empty transitive strict associative with_units AltCatStr is associative & the non empty transitive strict associative with_units AltCatStr is with_units & the non empty transitive strict associative with_units AltCatStr is strict ) thus ( the non empty transitive strict associative with_units AltCatStr is transitive & the non empty transitive strict associative with_units AltCatStr is associative & the non empty transitive strict associative with_units AltCatStr is with_units & the non empty transitive strict associative with_units AltCatStr is strict ) ; ::_thesis: verum end; end; registration let A be non empty transitive AltCatStr ; let B be non empty with_units AltCatStr ; cluster feasible strict Covariant Contravariant comp-preserving comp-reversing for FunctorStr over A,B; existence ex b1 being FunctorStr over A,B st ( b1 is strict & b1 is comp-preserving & b1 is comp-reversing & b1 is Covariant & b1 is Contravariant & b1 is feasible ) proof set o = the object of B; take A --> (idm the object of B) ; ::_thesis: ( A --> (idm the object of B) is strict & A --> (idm the object of B) is comp-preserving & A --> (idm the object of B) is comp-reversing & A --> (idm the object of B) is Covariant & A --> (idm the object of B) is Contravariant & A --> (idm the object of B) is feasible ) thus ( A --> (idm the object of B) is strict & A --> (idm the object of B) is comp-preserving & A --> (idm the object of B) is comp-reversing & A --> (idm the object of B) is Covariant & A --> (idm the object of B) is Contravariant & A --> (idm the object of B) is feasible ) ; ::_thesis: verum end; end; registration let A be non empty transitive with_units AltCatStr ; let B be non empty with_units AltCatStr ; cluster feasible strict Covariant Contravariant id-preserving comp-preserving comp-reversing for FunctorStr over A,B; existence ex b1 being FunctorStr over A,B st ( b1 is strict & b1 is comp-preserving & b1 is comp-reversing & b1 is Covariant & b1 is Contravariant & b1 is feasible & b1 is id-preserving ) proof set o = the object of B; take A --> (idm the object of B) ; ::_thesis: ( A --> (idm the object of B) is strict & A --> (idm the object of B) is comp-preserving & A --> (idm the object of B) is comp-reversing & A --> (idm the object of B) is Covariant & A --> (idm the object of B) is Contravariant & A --> (idm the object of B) is feasible & A --> (idm the object of B) is id-preserving ) thus ( A --> (idm the object of B) is strict & A --> (idm the object of B) is comp-preserving & A --> (idm the object of B) is comp-reversing & A --> (idm the object of B) is Covariant & A --> (idm the object of B) is Contravariant & A --> (idm the object of B) is feasible & A --> (idm the object of B) is id-preserving ) ; ::_thesis: verum end; end; registration let A be non empty transitive with_units AltCatStr ; let B be non empty with_units AltCatStr ; cluster feasible strict id-preserving covariant contravariant for Functor of A,B; existence ex b1 being Functor of A,B st ( b1 is strict & b1 is feasible & b1 is covariant & b1 is contravariant ) proof set o = the object of B; set I = A --> (idm the object of B); reconsider I = A --> (idm the object of B) as Functor of A,B by FUNCTOR0:def_25; take I ; ::_thesis: ( I is strict & I is feasible & I is covariant & I is contravariant ) thus ( I is strict & I is feasible ) ; ::_thesis: ( I is covariant & I is contravariant ) thus I is covariant ; ::_thesis: I is contravariant thus I is contravariant ; ::_thesis: verum end; end; theorem :: FUNCTOR3:1 for C being category for o1, o2, o3, o4 being object of C for a being Morphism of o1,o2 for b being Morphism of o2,o3 for c being Morphism of o1,o4 for d being Morphism of o4,o3 st b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds c * (a ") = (d ") * b proof let C be category; ::_thesis: for o1, o2, o3, o4 being object of C for a being Morphism of o1,o2 for b being Morphism of o2,o3 for c being Morphism of o1,o4 for d being Morphism of o4,o3 st b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds c * (a ") = (d ") * b let o1, o2, o3, o4 be object of C; ::_thesis: for a being Morphism of o1,o2 for b being Morphism of o2,o3 for c being Morphism of o1,o4 for d being Morphism of o4,o3 st b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds c * (a ") = (d ") * b let a be Morphism of o1,o2; ::_thesis: for b being Morphism of o2,o3 for c being Morphism of o1,o4 for d being Morphism of o4,o3 st b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds c * (a ") = (d ") * b let b be Morphism of o2,o3; ::_thesis: for c being Morphism of o1,o4 for d being Morphism of o4,o3 st b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds c * (a ") = (d ") * b let c be Morphism of o1,o4; ::_thesis: for d being Morphism of o4,o3 st b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds c * (a ") = (d ") * b let d be Morphism of o4,o3; ::_thesis: ( b * a = d * c & a * (a ") = idm o2 & (d ") * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} implies c * (a ") = (d ") * b ) assume that A1: b * a = d * c and A2: a * (a ") = idm o2 and A3: (d ") * d = idm o4 and A4: <^o1,o2^> <> {} and A5: <^o2,o1^> <> {} and A6: <^o2,o3^> <> {} and A7: <^o3,o4^> <> {} and A8: <^o4,o3^> <> {} ; ::_thesis: c * (a ") = (d ") * b A9: <^o2,o4^> <> {} by A6, A7, ALTCAT_1:def_2; <^o1,o3^> <> {} by A4, A6, ALTCAT_1:def_2; then A10: <^o1,o4^> <> {} by A7, ALTCAT_1:def_2; b = b * (idm o2) by A6, ALTCAT_1:def_17 .= (b * a) * (a ") by A2, A4, A5, A6, ALTCAT_1:21 ; hence (d ") * b = (d ") * (d * (c * (a "))) by A1, A5, A8, A10, ALTCAT_1:21 .= ((d ") * d) * (c * (a ")) by A7, A8, A9, ALTCAT_1:21 .= c * (a ") by A3, A9, ALTCAT_1:20 ; ::_thesis: verum end; theorem :: FUNCTOR3:2 for A being non empty transitive AltCatStr for B, C being non empty with_units AltCatStr for F being feasible Covariant FunctorStr over A,B for G being FunctorStr over B,C for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1)) proof let A be non empty transitive AltCatStr ; ::_thesis: for B, C being non empty with_units AltCatStr for F being feasible Covariant FunctorStr over A,B for G being FunctorStr over B,C for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1)) let B, C be non empty with_units AltCatStr ; ::_thesis: for F being feasible Covariant FunctorStr over A,B for G being FunctorStr over B,C for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1)) let F be feasible Covariant FunctorStr over A,B; ::_thesis: for G being FunctorStr over B,C for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1)) let G be FunctorStr over B,C; ::_thesis: for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1)) let o, o1 be object of A; ::_thesis: Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1)) ( dom the MorphMap of G = [: the carrier of B, the carrier of B:] & rng the ObjectMap of F c= [: the carrier of B, the carrier of B:] ) by PARTFUN1:def_2; then dom ( the MorphMap of G * the ObjectMap of F) = dom the ObjectMap of F by RELAT_1:27 .= [: the carrier of A, the carrier of A:] by FUNCT_2:def_1 ; then A1: [o,o1] in dom ( the MorphMap of G * the ObjectMap of F) by ZFMISC_1:87; then A2: ( the MorphMap of G * the ObjectMap of F) . [o,o1] = the MorphMap of G . ( the ObjectMap of F . (o,o1)) by FUNCT_1:12 .= Morph-Map (G,(F . o),(F . o1)) by FUNCTOR0:22 ; dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2; then [o,o1] in dom the MorphMap of F by ZFMISC_1:87; then [o,o1] in (dom ( the MorphMap of G * the ObjectMap of F)) /\ (dom the MorphMap of F) by A1, XBOOLE_0:def_4; then A3: [o,o1] in dom (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) by PBOOLE:def_19; thus Morph-Map ((G * F),o,o1) = (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o,o1) by FUNCTOR0:def_36 .= (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1)) by A3, A2, PBOOLE:def_19 ; ::_thesis: verum end; theorem :: FUNCTOR3:3 for A being non empty transitive AltCatStr for B, C being non empty with_units AltCatStr for F being feasible Contravariant FunctorStr over A,B for G being FunctorStr over B,C for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1)) proof let A be non empty transitive AltCatStr ; ::_thesis: for B, C being non empty with_units AltCatStr for F being feasible Contravariant FunctorStr over A,B for G being FunctorStr over B,C for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1)) let B, C be non empty with_units AltCatStr ; ::_thesis: for F being feasible Contravariant FunctorStr over A,B for G being FunctorStr over B,C for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1)) let F be feasible Contravariant FunctorStr over A,B; ::_thesis: for G being FunctorStr over B,C for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1)) let G be FunctorStr over B,C; ::_thesis: for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1)) let o, o1 be object of A; ::_thesis: Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1)) ( dom the MorphMap of G = [: the carrier of B, the carrier of B:] & rng the ObjectMap of F c= [: the carrier of B, the carrier of B:] ) by PARTFUN1:def_2; then dom ( the MorphMap of G * the ObjectMap of F) = dom the ObjectMap of F by RELAT_1:27 .= [: the carrier of A, the carrier of A:] by FUNCT_2:def_1 ; then A1: [o,o1] in dom ( the MorphMap of G * the ObjectMap of F) by ZFMISC_1:87; then A2: ( the MorphMap of G * the ObjectMap of F) . [o,o1] = the MorphMap of G . ( the ObjectMap of F . (o,o1)) by FUNCT_1:12 .= Morph-Map (G,(F . o1),(F . o)) by FUNCTOR0:23 ; dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2; then [o,o1] in dom the MorphMap of F by ZFMISC_1:87; then [o,o1] in (dom ( the MorphMap of G * the ObjectMap of F)) /\ (dom the MorphMap of F) by A1, XBOOLE_0:def_4; then A3: [o,o1] in dom (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) by PBOOLE:def_19; thus Morph-Map ((G * F),o,o1) = (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o,o1) by FUNCTOR0:def_36 .= (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1)) by A3, A2, PBOOLE:def_19 ; ::_thesis: verum end; Lm1: for I1 being set for I2 being non empty set for f being Function of I1,I2 for A being ManySortedSet of I1 for B being ManySortedSet of I2 for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M proof let I1 be set ; ::_thesis: for I2 being non empty set for f being Function of I1,I2 for A being ManySortedSet of I1 for B being ManySortedSet of I2 for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M let I2 be non empty set ; ::_thesis: for f being Function of I1,I2 for A being ManySortedSet of I1 for B being ManySortedSet of I2 for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M let f be Function of I1,I2; ::_thesis: for A being ManySortedSet of I1 for B being ManySortedSet of I2 for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M let A be ManySortedSet of I1; ::_thesis: for B being ManySortedSet of I2 for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M let B be ManySortedSet of I2; ::_thesis: for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M let M be ManySortedFunction of A,B * f; ::_thesis: ((id B) * f) ** M = M A1: now__::_thesis:_for_i_being_set_st_i_in_I1_holds_ (_(B_*_f)_._i_=_B_._(f_._i)_&_((id_B)_*_f)_._i_=_id_((B_*_f)_._i)_) let i be set ; ::_thesis: ( i in I1 implies ( (B * f) . i = B . (f . i) & ((id B) * f) . i = id ((B * f) . i) ) ) assume A2: i in I1 ; ::_thesis: ( (B * f) . i = B . (f . i) & ((id B) * f) . i = id ((B * f) . i) ) hence A3: (B * f) . i = B . (f . i) by FUNCT_2:15; ::_thesis: ((id B) * f) . i = id ((B * f) . i) ( ((id B) * f) . i = (id B) . (f . i) & f . i in I2 ) by A2, FUNCT_2:5, FUNCT_2:15; hence ((id B) * f) . i = id ((B * f) . i) by A3, MSUALG_3:def_1; ::_thesis: verum end; now__::_thesis:_for_i_being_set_st_i_in_I1_holds_ (((id_B)_*_f)_**_M)_._i_=_M_._i A4: (id B) * f is ManySortedFunction of B * f,B * f proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I1 or ((id B) * f) . i is M2( bool [:((B * f) . i),((B * f) . i):]) ) assume i in I1 ; ::_thesis: ((id B) * f) . i is M2( bool [:((B * f) . i),((B * f) . i):]) then ((id B) * f) . i = id ((B * f) . i) by A1; hence ((id B) * f) . i is M2( bool [:((B * f) . i),((B * f) . i):]) ; ::_thesis: verum end; let i be set ; ::_thesis: ( i in I1 implies (((id B) * f) ** M) . i = M . i ) assume A5: i in I1 ; ::_thesis: (((id B) * f) ** M) . i = M . i then A6: M . i is Function of (A . i),((B * f) . i) by PBOOLE:def_15; ( ((id B) * f) . i = (id B) . (f . i) & f . i in I2 ) by A5, FUNCT_2:5, FUNCT_2:15; then A7: ((id B) * f) . i = id (B . (f . i)) by MSUALG_3:def_1; (B * f) . i = B . (f . i) by A1, A5; hence (((id B) * f) ** M) . i = (id ((B * f) . i)) * (M . i) by A5, A4, A7, MSUALG_3:2 .= M . i by A6, FUNCT_2:17 ; ::_thesis: verum end; hence ((id B) * f) ** M = M by PBOOLE:3; ::_thesis: verum end; theorem :: FUNCTOR3:4 for A being non empty transitive AltCatStr for B being non empty with_units AltCatStr for F being feasible FunctorStr over A,B holds (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #) proof let A be non empty transitive AltCatStr ; ::_thesis: for B being non empty with_units AltCatStr for F being feasible FunctorStr over A,B holds (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #) let B be non empty with_units AltCatStr ; ::_thesis: for F being feasible FunctorStr over A,B holds (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #) let F be feasible FunctorStr over A,B; ::_thesis: (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #) A1: the ObjectMap of ((id B) * F) = the ObjectMap of (id B) * the ObjectMap of F by FUNCTOR0:def_36 .= (id [: the carrier of B, the carrier of B:]) * the ObjectMap of F by FUNCTOR0:def_29 .= the ObjectMap of F by FUNCT_2:17 ; A2: the MorphMap of F is ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F by FUNCTOR0:def_4; the MorphMap of ((id B) * F) = ( the MorphMap of (id B) * the ObjectMap of F) ** the MorphMap of F by FUNCTOR0:def_36 .= ((id the Arrows of B) * the ObjectMap of F) ** the MorphMap of F by FUNCTOR0:def_29 .= the MorphMap of F by A2, Lm1 ; hence (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #) by A1; ::_thesis: verum end; theorem :: FUNCTOR3:5 for A being non empty transitive with_units AltCatStr for B being non empty with_units AltCatStr for F being feasible FunctorStr over A,B holds F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #) proof let A be non empty transitive with_units AltCatStr ; ::_thesis: for B being non empty with_units AltCatStr for F being feasible FunctorStr over A,B holds F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #) let B be non empty with_units AltCatStr ; ::_thesis: for F being feasible FunctorStr over A,B holds F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #) let F be feasible FunctorStr over A,B; ::_thesis: F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #) A1: the ObjectMap of (F * (id A)) = the ObjectMap of F * the ObjectMap of (id A) by FUNCTOR0:def_36 .= the ObjectMap of F * (id [: the carrier of A, the carrier of A:]) by FUNCTOR0:def_29 .= the ObjectMap of F by FUNCT_2:17 ; A2: the MorphMap of F is ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F by FUNCTOR0:def_4; the MorphMap of (F * (id A)) = ( the MorphMap of F * the ObjectMap of (id A)) ** the MorphMap of (id A) by FUNCTOR0:def_36 .= ( the MorphMap of F * (id [: the carrier of A, the carrier of A:])) ** the MorphMap of (id A) by FUNCTOR0:def_29 .= the MorphMap of F ** the MorphMap of (id A) by FUNCTOR0:2 .= the MorphMap of F ** (id the Arrows of A) by FUNCTOR0:def_29 .= the MorphMap of F by A2, MSUALG_3:3 ; hence F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #) by A1; ::_thesis: verum end; theorem Th6: :: FUNCTOR3:6 for A being non empty AltCatStr for B, C being non empty reflexive AltCatStr for F being feasible Covariant FunctorStr over A,B for G being feasible Covariant FunctorStr over B,C for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (G * F) . m = G . (F . m) proof let A be non empty AltCatStr ; ::_thesis: for B, C being non empty reflexive AltCatStr for F being feasible Covariant FunctorStr over A,B for G being feasible Covariant FunctorStr over B,C for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (G * F) . m = G . (F . m) let B, C be non empty reflexive AltCatStr ; ::_thesis: for F being feasible Covariant FunctorStr over A,B for G being feasible Covariant FunctorStr over B,C for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (G * F) . m = G . (F . m) let F be feasible Covariant FunctorStr over A,B; ::_thesis: for G being feasible Covariant FunctorStr over B,C for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (G * F) . m = G . (F . m) let G be feasible Covariant FunctorStr over B,C; ::_thesis: for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (G * F) . m = G . (F . m) let o1, o2 be object of A; ::_thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (G * F) . m = G . (F . m) let m be Morphism of o1,o2; ::_thesis: ( <^o1,o2^> <> {} implies (G * F) . m = G . (F . m) ) set I = the carrier of A; reconsider s = the MorphMap of F . (o1,o2) as Function ; reconsider r = (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o1,o2) as Function ; reconsider t = ( the MorphMap of G * the ObjectMap of F) . (o1,o2) as Function ; A1: dom (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) = (dom ( the MorphMap of G * the ObjectMap of F)) /\ (dom the MorphMap of F) by PBOOLE:def_19 .= [: the carrier of A, the carrier of A:] /\ (dom the MorphMap of F) by PARTFUN1:def_2 .= [: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:] by PARTFUN1:def_2 .= [: the carrier of A, the carrier of A:] ; A2: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def_1; A3: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def_2; assume A4: <^o1,o2^> <> {} ; ::_thesis: (G * F) . m = G . (F . m) then A5: <^(F . o1),(F . o2)^> <> {} by FUNCTOR0:def_18; then A6: dom (Morph-Map (F,o1,o2)) = <^o1,o2^> by FUNCT_2:def_1; A7: <^(G . (F . o1)),(G . (F . o2))^> <> {} by A5, FUNCTOR0:def_18; ( (G * F) . o1 = G . (F . o1) & (G * F) . o2 = G . (F . o2) ) by FUNCTOR0:33; hence (G * F) . m = (Morph-Map ((G * F),o1,o2)) . m by A4, A7, FUNCTOR0:def_15 .= r . m by FUNCTOR0:def_36 .= (t * s) . m by A1, A3, PBOOLE:def_19 .= t . ((Morph-Map (F,o1,o2)) . m) by A4, A6, FUNCT_1:13 .= t . (F . m) by A4, A5, FUNCTOR0:def_15 .= ( the MorphMap of G . ( the ObjectMap of F . (o1,o2))) . (F . m) by A2, A3, FUNCT_1:13 .= (Morph-Map (G,(F . o1),(F . o2))) . (F . m) by FUNCTOR0:22 .= G . (F . m) by A5, A7, FUNCTOR0:def_15 ; ::_thesis: verum end; theorem Th7: :: FUNCTOR3:7 for A being non empty AltCatStr for B, C being non empty reflexive AltCatStr for M being feasible Contravariant FunctorStr over A,B for N being feasible Contravariant FunctorStr over B,C for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (N * M) . m = N . (M . m) proof let A be non empty AltCatStr ; ::_thesis: for B, C being non empty reflexive AltCatStr for M being feasible Contravariant FunctorStr over A,B for N being feasible Contravariant FunctorStr over B,C for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (N * M) . m = N . (M . m) let B, C be non empty reflexive AltCatStr ; ::_thesis: for M being feasible Contravariant FunctorStr over A,B for N being feasible Contravariant FunctorStr over B,C for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (N * M) . m = N . (M . m) let M be feasible Contravariant FunctorStr over A,B; ::_thesis: for N being feasible Contravariant FunctorStr over B,C for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (N * M) . m = N . (M . m) let N be feasible Contravariant FunctorStr over B,C; ::_thesis: for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (N * M) . m = N . (M . m) let o1, o2 be object of A; ::_thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (N * M) . m = N . (M . m) let m be Morphism of o1,o2; ::_thesis: ( <^o1,o2^> <> {} implies (N * M) . m = N . (M . m) ) set I = the carrier of A; reconsider s = the MorphMap of M . (o1,o2) as Function ; reconsider r = (( the MorphMap of N * the ObjectMap of M) ** the MorphMap of M) . (o1,o2) as Function ; reconsider t = ( the MorphMap of N * the ObjectMap of M) . (o1,o2) as Function ; A1: dom (( the MorphMap of N * the ObjectMap of M) ** the MorphMap of M) = (dom ( the MorphMap of N * the ObjectMap of M)) /\ (dom the MorphMap of M) by PBOOLE:def_19 .= [: the carrier of A, the carrier of A:] /\ (dom the MorphMap of M) by PARTFUN1:def_2 .= [: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:] by PARTFUN1:def_2 .= [: the carrier of A, the carrier of A:] ; A2: dom the ObjectMap of M = [: the carrier of A, the carrier of A:] by FUNCT_2:def_1; A3: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def_2; assume A4: <^o1,o2^> <> {} ; ::_thesis: (N * M) . m = N . (M . m) then A5: <^(M . o2),(M . o1)^> <> {} by FUNCTOR0:def_19; then A6: dom (Morph-Map (M,o1,o2)) = <^o1,o2^> by FUNCT_2:def_1; A7: <^(N . (M . o1)),(N . (M . o2))^> <> {} by A5, FUNCTOR0:def_19; ( (N * M) . o1 = N . (M . o1) & (N * M) . o2 = N . (M . o2) ) by FUNCTOR0:33; hence (N * M) . m = (Morph-Map ((N * M),o1,o2)) . m by A4, A7, FUNCTOR0:def_15 .= r . m by FUNCTOR0:def_36 .= (t * s) . m by A1, A3, PBOOLE:def_19 .= t . ((Morph-Map (M,o1,o2)) . m) by A4, A6, FUNCT_1:13 .= t . (M . m) by A4, A5, FUNCTOR0:def_16 .= ( the MorphMap of N . ( the ObjectMap of M . (o1,o2))) . (M . m) by A2, A3, FUNCT_1:13 .= (Morph-Map (N,(M . o2),(M . o1))) . (M . m) by FUNCTOR0:23 .= N . (M . m) by A5, A7, FUNCTOR0:def_16 ; ::_thesis: verum end; theorem Th8: :: FUNCTOR3:8 for A being non empty AltCatStr for B, C being non empty reflexive AltCatStr for F being feasible Covariant FunctorStr over A,B for N being feasible Contravariant FunctorStr over B,C for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (N * F) . m = N . (F . m) proof let A be non empty AltCatStr ; ::_thesis: for B, C being non empty reflexive AltCatStr for F being feasible Covariant FunctorStr over A,B for N being feasible Contravariant FunctorStr over B,C for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (N * F) . m = N . (F . m) let B, C be non empty reflexive AltCatStr ; ::_thesis: for F being feasible Covariant FunctorStr over A,B for N being feasible Contravariant FunctorStr over B,C for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (N * F) . m = N . (F . m) let F be feasible Covariant FunctorStr over A,B; ::_thesis: for N being feasible Contravariant FunctorStr over B,C for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (N * F) . m = N . (F . m) let N be feasible Contravariant FunctorStr over B,C; ::_thesis: for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (N * F) . m = N . (F . m) let o1, o2 be object of A; ::_thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (N * F) . m = N . (F . m) let m be Morphism of o1,o2; ::_thesis: ( <^o1,o2^> <> {} implies (N * F) . m = N . (F . m) ) set I = the carrier of A; reconsider s = the MorphMap of F . (o1,o2) as Function ; reconsider r = (( the MorphMap of N * the ObjectMap of F) ** the MorphMap of F) . (o1,o2) as Function ; reconsider t = ( the MorphMap of N * the ObjectMap of F) . (o1,o2) as Function ; A1: dom (( the MorphMap of N * the ObjectMap of F) ** the MorphMap of F) = (dom ( the MorphMap of N * the ObjectMap of F)) /\ (dom the MorphMap of F) by PBOOLE:def_19 .= [: the carrier of A, the carrier of A:] /\ (dom the MorphMap of F) by PARTFUN1:def_2 .= [: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:] by PARTFUN1:def_2 .= [: the carrier of A, the carrier of A:] ; A2: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def_1; A3: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def_2; assume A4: <^o1,o2^> <> {} ; ::_thesis: (N * F) . m = N . (F . m) then A5: <^(F . o1),(F . o2)^> <> {} by FUNCTOR0:def_18; then A6: dom (Morph-Map (F,o1,o2)) = <^o1,o2^> by FUNCT_2:def_1; A7: <^(N . (F . o2)),(N . (F . o1))^> <> {} by A5, FUNCTOR0:def_19; ( (N * F) . o1 = N . (F . o1) & (N * F) . o2 = N . (F . o2) ) by FUNCTOR0:33; hence (N * F) . m = (Morph-Map ((N * F),o1,o2)) . m by A4, A7, FUNCTOR0:def_16 .= r . m by FUNCTOR0:def_36 .= (t * s) . m by A1, A3, PBOOLE:def_19 .= t . ((Morph-Map (F,o1,o2)) . m) by A4, A6, FUNCT_1:13 .= t . (F . m) by A4, A5, FUNCTOR0:def_15 .= ( the MorphMap of N . ( the ObjectMap of F . (o1,o2))) . (F . m) by A2, A3, FUNCT_1:13 .= (Morph-Map (N,(F . o1),(F . o2))) . (F . m) by FUNCTOR0:22 .= N . (F . m) by A5, A7, FUNCTOR0:def_16 ; ::_thesis: verum end; theorem Th9: :: FUNCTOR3:9 for A being non empty AltCatStr for C, B being non empty reflexive AltCatStr for G being feasible Covariant FunctorStr over B,C for M being feasible Contravariant FunctorStr over A,B for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (G * M) . m = G . (M . m) proof let A be non empty AltCatStr ; ::_thesis: for C, B being non empty reflexive AltCatStr for G being feasible Covariant FunctorStr over B,C for M being feasible Contravariant FunctorStr over A,B for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (G * M) . m = G . (M . m) let C, B be non empty reflexive AltCatStr ; ::_thesis: for G being feasible Covariant FunctorStr over B,C for M being feasible Contravariant FunctorStr over A,B for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (G * M) . m = G . (M . m) let G be feasible Covariant FunctorStr over B,C; ::_thesis: for M being feasible Contravariant FunctorStr over A,B for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (G * M) . m = G . (M . m) let M be feasible Contravariant FunctorStr over A,B; ::_thesis: for o1, o2 being object of A for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (G * M) . m = G . (M . m) let o1, o2 be object of A; ::_thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (G * M) . m = G . (M . m) let m be Morphism of o1,o2; ::_thesis: ( <^o1,o2^> <> {} implies (G * M) . m = G . (M . m) ) set I = the carrier of A; reconsider s = the MorphMap of M . (o1,o2) as Function ; reconsider r = (( the MorphMap of G * the ObjectMap of M) ** the MorphMap of M) . (o1,o2) as Function ; reconsider t = ( the MorphMap of G * the ObjectMap of M) . (o1,o2) as Function ; A1: dom (( the MorphMap of G * the ObjectMap of M) ** the MorphMap of M) = (dom ( the MorphMap of G * the ObjectMap of M)) /\ (dom the MorphMap of M) by PBOOLE:def_19 .= [: the carrier of A, the carrier of A:] /\ (dom the MorphMap of M) by PARTFUN1:def_2 .= [: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:] by PARTFUN1:def_2 .= [: the carrier of A, the carrier of A:] ; A2: dom the ObjectMap of M = [: the carrier of A, the carrier of A:] by FUNCT_2:def_1; A3: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def_2; assume A4: <^o1,o2^> <> {} ; ::_thesis: (G * M) . m = G . (M . m) then A5: <^(M . o2),(M . o1)^> <> {} by FUNCTOR0:def_19; then A6: dom (Morph-Map (M,o1,o2)) = <^o1,o2^> by FUNCT_2:def_1; A7: <^(G . (M . o2)),(G . (M . o1))^> <> {} by A5, FUNCTOR0:def_18; ( (G * M) . o1 = G . (M . o1) & (G * M) . o2 = G . (M . o2) ) by FUNCTOR0:33; hence (G * M) . m = (Morph-Map ((G * M),o1,o2)) . m by A4, A7, FUNCTOR0:def_16 .= r . m by FUNCTOR0:def_36 .= (t * s) . m by A1, A3, PBOOLE:def_19 .= t . ((Morph-Map (M,o1,o2)) . m) by A4, A6, FUNCT_1:13 .= t . (M . m) by A4, A5, FUNCTOR0:def_16 .= ( the MorphMap of G . ( the ObjectMap of M . (o1,o2))) . (M . m) by A2, A3, FUNCT_1:13 .= (Morph-Map (G,(M . o2),(M . o1))) . (M . m) by FUNCTOR0:23 .= G . (M . m) by A5, A7, FUNCTOR0:def_15 ; ::_thesis: verum end; registration let A be non empty transitive AltCatStr ; let B be non empty transitive with_units AltCatStr ; let C be non empty with_units AltCatStr ; let F be feasible Covariant comp-preserving FunctorStr over A,B; let G be feasible Covariant comp-preserving FunctorStr over B,C; clusterG * F -> comp-preserving ; coherence G * F is comp-preserving proof let o1, o2, o3 be object of A; :: according to FUNCTOR0:def_23 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b1 being M2(<^o1,o2^>) for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b2) * ((G * F) . b1) ) assume that A1: <^o1,o2^> <> {} and A2: <^o2,o3^> <> {} ; ::_thesis: for b1 being M2(<^o1,o2^>) for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b2) * ((G * F) . b1) A3: ( <^(F . o1),(F . o2)^> <> {} & <^(F . o2),(F . o3)^> <> {} ) by A1, A2, FUNCTOR0:def_18; let f be Morphism of o1,o2; ::_thesis: for b1 being M2(<^o2,o3^>) holds (G * F) . (b1 * f) = ((G * F) . b1) * ((G * F) . f) let g be Morphism of o2,o3; ::_thesis: (G * F) . (g * f) = ((G * F) . g) * ((G * F) . f) A4: ( (G * F) . o1 = G . (F . o1) & (G * F) . o3 = G . (F . o3) ) by FUNCTOR0:33; A5: (G * F) . o2 = G . (F . o2) by FUNCTOR0:33; then reconsider GFg = (G * F) . g as Morphism of (G . (F . o2)),(G . (F . o3)) by FUNCTOR0:33; <^o1,o3^> <> {} by A1, A2, ALTCAT_1:def_2; hence (G * F) . (g * f) = G . (F . (g * f)) by Th6 .= G . ((F . g) * (F . f)) by A1, A2, FUNCTOR0:def_23 .= (G . (F . g)) * (G . (F . f)) by A3, FUNCTOR0:def_23 .= GFg * (G . (F . f)) by A2, Th6 .= ((G * F) . g) * ((G * F) . f) by A1, A5, A4, Th6 ; ::_thesis: verum end; end; registration let A be non empty transitive AltCatStr ; let B be non empty transitive with_units AltCatStr ; let C be non empty with_units AltCatStr ; let F be feasible Contravariant comp-reversing FunctorStr over A,B; let G be feasible Contravariant comp-reversing FunctorStr over B,C; clusterG * F -> comp-preserving ; coherence G * F is comp-preserving proof let o1, o2, o3 be object of A; :: according to FUNCTOR0:def_23 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b1 being M2(<^o1,o2^>) for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b2) * ((G * F) . b1) ) assume that A1: <^o1,o2^> <> {} and A2: <^o2,o3^> <> {} ; ::_thesis: for b1 being M2(<^o1,o2^>) for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b2) * ((G * F) . b1) A3: ( <^(F . o2),(F . o1)^> <> {} & <^(F . o3),(F . o2)^> <> {} ) by A1, A2, FUNCTOR0:def_19; let f be Morphism of o1,o2; ::_thesis: for b1 being M2(<^o2,o3^>) holds (G * F) . (b1 * f) = ((G * F) . b1) * ((G * F) . f) let g be Morphism of o2,o3; ::_thesis: (G * F) . (g * f) = ((G * F) . g) * ((G * F) . f) A4: ( (G * F) . o1 = G . (F . o1) & (G * F) . o3 = G . (F . o3) ) by FUNCTOR0:33; A5: (G * F) . o2 = G . (F . o2) by FUNCTOR0:33; then reconsider GFg = (G * F) . g as Morphism of (G . (F . o2)),(G . (F . o3)) by FUNCTOR0:33; <^o1,o3^> <> {} by A1, A2, ALTCAT_1:def_2; hence (G * F) . (g * f) = G . (F . (g * f)) by Th7 .= G . ((F . f) * (F . g)) by A1, A2, FUNCTOR0:def_24 .= (G . (F . g)) * (G . (F . f)) by A3, FUNCTOR0:def_24 .= GFg * (G . (F . f)) by A2, Th7 .= ((G * F) . g) * ((G * F) . f) by A1, A5, A4, Th7 ; ::_thesis: verum end; end; registration let A be non empty transitive AltCatStr ; let B be non empty transitive with_units AltCatStr ; let C be non empty with_units AltCatStr ; let F be feasible Covariant comp-preserving FunctorStr over A,B; let G be feasible Contravariant comp-reversing FunctorStr over B,C; clusterG * F -> comp-reversing ; coherence G * F is comp-reversing proof let o1, o2, o3 be object of A; :: according to FUNCTOR0:def_24 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b1 being M2(<^o1,o2^>) for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b1) * ((G * F) . b2) ) assume that A1: <^o1,o2^> <> {} and A2: <^o2,o3^> <> {} ; ::_thesis: for b1 being M2(<^o1,o2^>) for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b1) * ((G * F) . b2) A3: ( <^(F . o1),(F . o2)^> <> {} & <^(F . o2),(F . o3)^> <> {} ) by A1, A2, FUNCTOR0:def_18; let f be Morphism of o1,o2; ::_thesis: for b1 being M2(<^o2,o3^>) holds (G * F) . (b1 * f) = ((G * F) . f) * ((G * F) . b1) let g be Morphism of o2,o3; ::_thesis: (G * F) . (g * f) = ((G * F) . f) * ((G * F) . g) A4: ( (G * F) . o2 = G . (F . o2) & (G * F) . o3 = G . (F . o3) ) by FUNCTOR0:33; A5: (G * F) . o1 = G . (F . o1) by FUNCTOR0:33; then reconsider GFf = (G * F) . f as Morphism of (G . (F . o2)),(G . (F . o1)) by FUNCTOR0:33; <^o1,o3^> <> {} by A1, A2, ALTCAT_1:def_2; hence (G * F) . (g * f) = G . (F . (g * f)) by Th8 .= G . ((F . g) * (F . f)) by A1, A2, FUNCTOR0:def_23 .= (G . (F . f)) * (G . (F . g)) by A3, FUNCTOR0:def_24 .= GFf * (G . (F . g)) by A1, Th8 .= ((G * F) . f) * ((G * F) . g) by A2, A5, A4, Th8 ; ::_thesis: verum end; end; registration let A be non empty transitive AltCatStr ; let B be non empty transitive with_units AltCatStr ; let C be non empty with_units AltCatStr ; let F be feasible Contravariant comp-reversing FunctorStr over A,B; let G be feasible Covariant comp-preserving FunctorStr over B,C; clusterG * F -> comp-reversing ; coherence G * F is comp-reversing proof let o1, o2, o3 be object of A; :: according to FUNCTOR0:def_24 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b1 being M2(<^o1,o2^>) for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b1) * ((G * F) . b2) ) assume that A1: <^o1,o2^> <> {} and A2: <^o2,o3^> <> {} ; ::_thesis: for b1 being M2(<^o1,o2^>) for b2 being M2(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b1) * ((G * F) . b2) A3: ( <^(F . o2),(F . o1)^> <> {} & <^(F . o3),(F . o2)^> <> {} ) by A1, A2, FUNCTOR0:def_19; let f be Morphism of o1,o2; ::_thesis: for b1 being M2(<^o2,o3^>) holds (G * F) . (b1 * f) = ((G * F) . f) * ((G * F) . b1) let g be Morphism of o2,o3; ::_thesis: (G * F) . (g * f) = ((G * F) . f) * ((G * F) . g) A4: ( (G * F) . o2 = G . (F . o2) & (G * F) . o3 = G . (F . o3) ) by FUNCTOR0:33; A5: (G * F) . o1 = G . (F . o1) by FUNCTOR0:33; then reconsider GFf = (G * F) . f as Morphism of (G . (F . o2)),(G . (F . o1)) by FUNCTOR0:33; <^o1,o3^> <> {} by A1, A2, ALTCAT_1:def_2; hence (G * F) . (g * f) = G . (F . (g * f)) by Th9 .= G . ((F . f) * (F . g)) by A1, A2, FUNCTOR0:def_24 .= (G . (F . f)) * (G . (F . g)) by A3, FUNCTOR0:def_23 .= GFf * (G . (F . g)) by A1, Th9 .= ((G * F) . f) * ((G * F) . g) by A2, A5, A4, Th9 ; ::_thesis: verum end; end; definition let A, B be non empty transitive with_units AltCatStr ; let C be non empty with_units AltCatStr ; let F be covariant Functor of A,B; let G be covariant Functor of B,C; :: original: * redefine funcG * F -> strict covariant Functor of A,C; coherence G * F is strict covariant Functor of A,C by FUNCTOR0:def_25; end; definition let A, B be non empty transitive with_units AltCatStr ; let C be non empty with_units AltCatStr ; let F be contravariant Functor of A,B; let G be contravariant Functor of B,C; :: original: * redefine funcG * F -> strict covariant Functor of A,C; coherence G * F is strict covariant Functor of A,C by FUNCTOR0:def_25; end; definition let A, B be non empty transitive with_units AltCatStr ; let C be non empty with_units AltCatStr ; let F be covariant Functor of A,B; let G be contravariant Functor of B,C; :: original: * redefine funcG * F -> strict contravariant Functor of A,C; coherence G * F is strict contravariant Functor of A,C by FUNCTOR0:def_25; end; definition let A, B be non empty transitive with_units AltCatStr ; let C be non empty with_units AltCatStr ; let F be contravariant Functor of A,B; let G be covariant Functor of B,C; :: original: * redefine funcG * F -> strict contravariant Functor of A,C; coherence G * F is strict contravariant Functor of A,C by FUNCTOR0:def_25; end; theorem Th10: :: FUNCTOR3:10 for A, B, C being non empty transitive with_units AltCatStr for F1, F2 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds G1 * F1 is_transformable_to G2 * F2 proof let A, B, C be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds G1 * F1 is_transformable_to G2 * F2 let F1, F2 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds G1 * F1 is_transformable_to G2 * F2 let G1, G2 be covariant Functor of B,C; ::_thesis: ( F1 is_transformable_to F2 & G1 is_transformable_to G2 implies G1 * F1 is_transformable_to G2 * F2 ) assume A1: for a being object of A holds <^(F1 . a),(F2 . a)^> <> {} ; :: according to FUNCTOR2:def_1 ::_thesis: ( not G1 is_transformable_to G2 or G1 * F1 is_transformable_to G2 * F2 ) assume A2: for a being object of B holds <^(G1 . a),(G2 . a)^> <> {} ; :: according to FUNCTOR2:def_1 ::_thesis: G1 * F1 is_transformable_to G2 * F2 let a be object of A; :: according to FUNCTOR2:def_1 ::_thesis: not <^((G1 * F1) . a),((G2 * F2) . a)^> = {} <^(F1 . a),(F2 . a)^> <> {} by A1; then A3: <^(G1 . (F1 . a)),(G1 . (F2 . a))^> <> {} by FUNCTOR0:def_18; A4: ( (G1 * F1) . a = G1 . (F1 . a) & (G2 * F2) . a = G2 . (F2 . a) ) by FUNCTOR0:33; <^(G1 . (F2 . a)),(G2 . (F2 . a))^> <> {} by A2; hence not <^((G1 * F1) . a),((G2 * F2) . a)^> = {} by A4, A3, ALTCAT_1:def_2; ::_thesis: verum end; begin definition let A, B, C be non empty transitive with_units AltCatStr ; let F1, F2 be covariant Functor of A,B; let t be transformation of F1,F2; let G be covariant Functor of B,C; assume B1: F1 is_transformable_to F2 ; funcG * t -> transformation of G * F1,G * F2 means :Def1: :: FUNCTOR3:def 1 for o being object of A holds it . o = G . (t ! o); existence ex b1 being transformation of G * F1,G * F2 st for o being object of A holds b1 . o = G . (t ! o) proof defpred S1[ set , set ] means ex o being object of A st ( \$1 = o & \$2 = G . (t ! o) ); set I = the carrier of A; A1: for i being set st i in the carrier of A holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in the carrier of A implies ex j being set st S1[i,j] ) assume i in the carrier of A ; ::_thesis: ex j being set st S1[i,j] then reconsider o = i as object of A ; take G . (t ! o) ; ::_thesis: S1[i,G . (t ! o)] thus S1[i,G . (t ! o)] ; ::_thesis: verum end; consider IT being ManySortedSet of the carrier of A such that A2: for o being set st o in the carrier of A holds S1[o,IT . o] from PBOOLE:sch_3(A1); IT is transformation of G * F1,G * F2 proof thus G * F1 is_transformable_to G * F2 by B1, Th10; :: according to FUNCTOR2:def_2 ::_thesis: for b1 being M2( the carrier of A) holds IT . b1 is M2(<^((G * F1) . b1),((G * F2) . b1)^>) let o be object of A; ::_thesis: IT . o is M2(<^((G * F1) . o),((G * F2) . o)^>) ( S1[o,IT . o] & G . (F1 . o) = (G * F1) . o ) by A2, FUNCTOR0:33; hence IT . o is M2(<^((G * F1) . o),((G * F2) . o)^>) by FUNCTOR0:33; ::_thesis: verum end; then reconsider IT = IT as transformation of G * F1,G * F2 ; take IT ; ::_thesis: for o being object of A holds IT . o = G . (t ! o) let o be object of A; ::_thesis: IT . o = G . (t ! o) S1[o,IT . o] by A2; hence IT . o = G . (t ! o) ; ::_thesis: verum end; uniqueness for b1, b2 being transformation of G * F1,G * F2 st ( for o being object of A holds b1 . o = G . (t ! o) ) & ( for o being object of A holds b2 . o = G . (t ! o) ) holds b1 = b2 proof let X, Y be transformation of G * F1,G * F2; ::_thesis: ( ( for o being object of A holds X . o = G . (t ! o) ) & ( for o being object of A holds Y . o = G . (t ! o) ) implies X = Y ) assume that A3: for o being object of A holds X . o = G . (t ! o) and A4: for o being object of A holds Y . o = G . (t ! o) ; ::_thesis: X = Y A5: G * F1 is_transformable_to G * F2 by B1, Th10; now__::_thesis:_for_o_being_object_of_A_holds_X_!_o_=_Y_!_o let o be object of A; ::_thesis: X ! o = Y ! o thus X ! o = X . o by A5, FUNCTOR2:def_4 .= G . (t ! o) by A3 .= Y . o by A4 .= Y ! o by A5, FUNCTOR2:def_4 ; ::_thesis: verum end; hence X = Y by B1, Th10, FUNCTOR2:3; ::_thesis: verum end; end; :: deftheorem Def1 defines * FUNCTOR3:def_1_:_ for A, B, C being non empty transitive with_units AltCatStr for F1, F2 being covariant Functor of A,B for t being transformation of F1,F2 for G being covariant Functor of B,C st F1 is_transformable_to F2 holds for b8 being transformation of G * F1,G * F2 holds ( b8 = G * t iff for o being object of A holds b8 . o = G . (t ! o) ); theorem Th11: :: FUNCTOR3:11 for C, B, A being non empty transitive with_units AltCatStr for F1, F2 being covariant Functor of A,B for G1 being covariant Functor of B,C for p being transformation of F1,F2 for o being object of A st F1 is_transformable_to F2 holds (G1 * p) ! o = G1 . (p ! o) proof let C, B, A be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B for G1 being covariant Functor of B,C for p being transformation of F1,F2 for o being object of A st F1 is_transformable_to F2 holds (G1 * p) ! o = G1 . (p ! o) let F1, F2 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C for p being transformation of F1,F2 for o being object of A st F1 is_transformable_to F2 holds (G1 * p) ! o = G1 . (p ! o) let G1 be covariant Functor of B,C; ::_thesis: for p being transformation of F1,F2 for o being object of A st F1 is_transformable_to F2 holds (G1 * p) ! o = G1 . (p ! o) let p be transformation of F1,F2; ::_thesis: for o being object of A st F1 is_transformable_to F2 holds (G1 * p) ! o = G1 . (p ! o) let o be object of A; ::_thesis: ( F1 is_transformable_to F2 implies (G1 * p) ! o = G1 . (p ! o) ) assume A1: F1 is_transformable_to F2 ; ::_thesis: (G1 * p) ! o = G1 . (p ! o) then G1 * F1 is_transformable_to G1 * F2 by Th10; hence (G1 * p) ! o = (G1 * p) . o by FUNCTOR2:def_4 .= G1 . (p ! o) by A1, Def1 ; ::_thesis: verum end; definition let A, B, C be non empty transitive with_units AltCatStr ; let G1, G2 be covariant Functor of B,C; let F be covariant Functor of A,B; let s be transformation of G1,G2; assume B1: G1 is_transformable_to G2 ; funcs * F -> transformation of G1 * F,G2 * F means :Def2: :: FUNCTOR3:def 2 for o being object of A holds it . o = s ! (F . o); existence ex b1 being transformation of G1 * F,G2 * F st for o being object of A holds b1 . o = s ! (F . o) proof defpred S1[ set , set ] means ex o being object of A st ( \$1 = o & \$2 = s ! (F . o) ); set I = the carrier of A; A1: for i being set st i in the carrier of A holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in the carrier of A implies ex j being set st S1[i,j] ) assume i in the carrier of A ; ::_thesis: ex j being set st S1[i,j] then reconsider o = i as object of A ; take s ! (F . o) ; ::_thesis: S1[i,s ! (F . o)] thus S1[i,s ! (F . o)] ; ::_thesis: verum end; consider IT being ManySortedSet of the carrier of A such that A2: for o being set st o in the carrier of A holds S1[o,IT . o] from PBOOLE:sch_3(A1); IT is transformation of G1 * F,G2 * F proof thus G1 * F is_transformable_to G2 * F by B1, Th10; :: according to FUNCTOR2:def_2 ::_thesis: for b1 being M2( the carrier of A) holds IT . b1 is M2(<^((G1 * F) . b1),((G2 * F) . b1)^>) let o be object of A; ::_thesis: IT . o is M2(<^((G1 * F) . o),((G2 * F) . o)^>) ( S1[o,IT . o] & G1 . (F . o) = (G1 * F) . o ) by A2, FUNCTOR0:33; hence IT . o is M2(<^((G1 * F) . o),((G2 * F) . o)^>) by FUNCTOR0:33; ::_thesis: verum end; then reconsider IT = IT as transformation of G1 * F,G2 * F ; take IT ; ::_thesis: for o being object of A holds IT . o = s ! (F . o) let o be object of A; ::_thesis: IT . o = s ! (F . o) S1[o,IT . o] by A2; hence IT . o = s ! (F . o) ; ::_thesis: verum end; uniqueness for b1, b2 being transformation of G1 * F,G2 * F st ( for o being object of A holds b1 . o = s ! (F . o) ) & ( for o being object of A holds b2 . o = s ! (F . o) ) holds b1 = b2 proof let X, Y be transformation of G1 * F,G2 * F; ::_thesis: ( ( for o being object of A holds X . o = s ! (F . o) ) & ( for o being object of A holds Y . o = s ! (F . o) ) implies X = Y ) assume that A3: for o being object of A holds X . o = s ! (F . o) and A4: for o being object of A holds Y . o = s ! (F . o) ; ::_thesis: X = Y A5: G1 * F is_transformable_to G2 * F by B1, Th10; now__::_thesis:_for_o_being_object_of_A_holds_X_!_o_=_Y_!_o let o be object of A; ::_thesis: X ! o = Y ! o thus X ! o = X . o by A5, FUNCTOR2:def_4 .= s ! (F . o) by A3 .= Y . o by A4 .= Y ! o by A5, FUNCTOR2:def_4 ; ::_thesis: verum end; hence X = Y by B1, Th10, FUNCTOR2:3; ::_thesis: verum end; end; :: deftheorem Def2 defines * FUNCTOR3:def_2_:_ for A, B, C being non empty transitive with_units AltCatStr for G1, G2 being covariant Functor of B,C for F being covariant Functor of A,B for s being transformation of G1,G2 st G1 is_transformable_to G2 holds for b8 being transformation of G1 * F,G2 * F holds ( b8 = s * F iff for o being object of A holds b8 . o = s ! (F . o) ); theorem Th12: :: FUNCTOR3:12 for B, C, A being non empty transitive with_units AltCatStr for F1 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for q being transformation of G1,G2 for o being object of A st G1 is_transformable_to G2 holds (q * F1) ! o = q ! (F1 . o) proof let B, C, A be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for q being transformation of G1,G2 for o being object of A st G1 is_transformable_to G2 holds (q * F1) ! o = q ! (F1 . o) let F1 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C for q being transformation of G1,G2 for o being object of A st G1 is_transformable_to G2 holds (q * F1) ! o = q ! (F1 . o) let G1, G2 be covariant Functor of B,C; ::_thesis: for q being transformation of G1,G2 for o being object of A st G1 is_transformable_to G2 holds (q * F1) ! o = q ! (F1 . o) let q be transformation of G1,G2; ::_thesis: for o being object of A st G1 is_transformable_to G2 holds (q * F1) ! o = q ! (F1 . o) let o be object of A; ::_thesis: ( G1 is_transformable_to G2 implies (q * F1) ! o = q ! (F1 . o) ) assume A1: G1 is_transformable_to G2 ; ::_thesis: (q * F1) ! o = q ! (F1 . o) then G1 * F1 is_transformable_to G2 * F1 by Th10; hence (q * F1) ! o = (q * F1) . o by FUNCTOR2:def_4 .= q ! (F1 . o) by A1, Def2 ; ::_thesis: verum end; theorem Th13: :: FUNCTOR3:13 for C, A, B being non empty transitive with_units AltCatStr for F1, F2, F3 being covariant Functor of A,B for G1 being covariant Functor of B,C for p being transformation of F1,F2 for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p) proof let C, A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2, F3 being covariant Functor of A,B for G1 being covariant Functor of B,C for p being transformation of F1,F2 for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p) let F1, F2, F3 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C for p being transformation of F1,F2 for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p) let G1 be covariant Functor of B,C; ::_thesis: for p being transformation of F1,F2 for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p) let p be transformation of F1,F2; ::_thesis: for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p) let p1 be transformation of F2,F3; ::_thesis: ( F1 is_transformable_to F2 & F2 is_transformable_to F3 implies G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p) ) assume that A1: F1 is_transformable_to F2 and A2: F2 is_transformable_to F3 ; ::_thesis: G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p) A3: ( G1 * F1 is_transformable_to G1 * F2 & G1 * F2 is_transformable_to G1 * F3 ) by A1, A2, Th10; A4: now__::_thesis:_for_a_being_object_of_A_holds_(G1_*_(p1_`*`_p))_!_a_=_((G1_*_p1)_`*`_(G1_*_p))_!_a let a be object of A; ::_thesis: (G1 * (p1 `*` p)) ! a = ((G1 * p1) `*` (G1 * p)) ! a A5: ( G1 . (F2 . a) = (G1 * F2) . a & G1 . (F3 . a) = (G1 * F3) . a ) by FUNCTOR0:33; A6: G1 . (F1 . a) = (G1 * F1) . a by FUNCTOR0:33; then reconsider G1ta = (G1 * p) ! a as Morphism of (G1 . (F1 . a)),(G1 . (F2 . a)) by FUNCTOR0:33; A7: ( <^(F1 . a),(F2 . a)^> <> {} & <^(F2 . a),(F3 . a)^> <> {} ) by A1, A2, FUNCTOR2:def_1; thus (G1 * (p1 `*` p)) ! a = G1 . ((p1 `*` p) ! a) by A1, A2, Th11, FUNCTOR2:2 .= G1 . ((p1 ! a) * (p ! a)) by A1, A2, FUNCTOR2:def_5 .= (G1 . (p1 ! a)) * (G1 . (p ! a)) by A7, FUNCTOR0:def_23 .= (G1 . (p1 ! a)) * G1ta by A1, Th11 .= ((G1 * p1) ! a) * ((G1 * p) ! a) by A2, A6, A5, Th11 .= ((G1 * p1) `*` (G1 * p)) ! a by A3, FUNCTOR2:def_5 ; ::_thesis: verum end; F1 is_transformable_to F3 by A1, A2, FUNCTOR2:2; hence G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p) by A4, Th10, FUNCTOR2:3; ::_thesis: verum end; theorem Th14: :: FUNCTOR3:14 for A, B, C being non empty transitive with_units AltCatStr for F1 being covariant Functor of A,B for G1, G2, G3 being covariant Functor of B,C for q being transformation of G1,G2 for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) proof let A, B, C be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B for G1, G2, G3 being covariant Functor of B,C for q being transformation of G1,G2 for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) let F1 be covariant Functor of A,B; ::_thesis: for G1, G2, G3 being covariant Functor of B,C for q being transformation of G1,G2 for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) let G1, G2, G3 be covariant Functor of B,C; ::_thesis: for q being transformation of G1,G2 for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) let q be transformation of G1,G2; ::_thesis: for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) let q1 be transformation of G2,G3; ::_thesis: ( G1 is_transformable_to G2 & G2 is_transformable_to G3 implies (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) ) assume that A1: G1 is_transformable_to G2 and A2: G2 is_transformable_to G3 ; ::_thesis: (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) A3: ( G1 * F1 is_transformable_to G2 * F1 & G2 * F1 is_transformable_to G3 * F1 ) by A1, A2, Th10; A4: now__::_thesis:_for_a_being_object_of_A_holds_((q1_`*`_q)_*_F1)_!_a_=_((q1_*_F1)_`*`_(q_*_F1))_!_a let a be object of A; ::_thesis: ((q1 `*` q) * F1) ! a = ((q1 * F1) `*` (q * F1)) ! a A5: ( G1 . (F1 . a) = (G1 * F1) . a & G3 . (F1 . a) = (G3 * F1) . a ) by FUNCTOR0:33; A6: G2 . (F1 . a) = (G2 * F1) . a by FUNCTOR0:33; then reconsider s1F1a = (q1 * F1) ! a as Morphism of (G2 . (F1 . a)),(G3 . (F1 . a)) by FUNCTOR0:33; thus ((q1 `*` q) * F1) ! a = (q1 `*` q) ! (F1 . a) by A1, A2, Th12, FUNCTOR2:2 .= (q1 ! (F1 . a)) * (q ! (F1 . a)) by A1, A2, FUNCTOR2:def_5 .= s1F1a * (q ! (F1 . a)) by A2, Th12 .= ((q1 * F1) ! a) * ((q * F1) ! a) by A1, A6, A5, Th12 .= ((q1 * F1) `*` (q * F1)) ! a by A3, FUNCTOR2:def_5 ; ::_thesis: verum end; G1 is_transformable_to G3 by A1, A2, FUNCTOR2:2; hence (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) by A4, Th10, FUNCTOR2:3; ::_thesis: verum end; theorem Th15: :: FUNCTOR3:15 for A, B, C, D being non empty transitive with_units AltCatStr for F1 being covariant Functor of A,B for G1 being covariant Functor of B,C for H1, H2 being covariant Functor of C,D for r being transformation of H1,H2 st H1 is_transformable_to H2 holds (r * G1) * F1 = r * (G1 * F1) proof let A, B, C, D be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B for G1 being covariant Functor of B,C for H1, H2 being covariant Functor of C,D for r being transformation of H1,H2 st H1 is_transformable_to H2 holds (r * G1) * F1 = r * (G1 * F1) let F1 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C for H1, H2 being covariant Functor of C,D for r being transformation of H1,H2 st H1 is_transformable_to H2 holds (r * G1) * F1 = r * (G1 * F1) let G1 be covariant Functor of B,C; ::_thesis: for H1, H2 being covariant Functor of C,D for r being transformation of H1,H2 st H1 is_transformable_to H2 holds (r * G1) * F1 = r * (G1 * F1) let H1, H2 be covariant Functor of C,D; ::_thesis: for r being transformation of H1,H2 st H1 is_transformable_to H2 holds (r * G1) * F1 = r * (G1 * F1) let r be transformation of H1,H2; ::_thesis: ( H1 is_transformable_to H2 implies (r * G1) * F1 = r * (G1 * F1) ) A1: (H2 * G1) * F1 = H2 * (G1 * F1) by FUNCTOR0:32; then reconsider m = r * (G1 * F1) as transformation of (H1 * G1) * F1,(H2 * G1) * F1 by FUNCTOR0:32; assume A2: H1 is_transformable_to H2 ; ::_thesis: (r * G1) * F1 = r * (G1 * F1) A3: now__::_thesis:_for_a_being_object_of_A_holds_((r_*_G1)_*_F1)_!_a_=_m_!_a let a be object of A; ::_thesis: ((r * G1) * F1) ! a = m ! a thus ((r * G1) * F1) ! a = (r * G1) ! (F1 . a) by A2, Th10, Th12 .= r ! (G1 . (F1 . a)) by A2, Th12 .= r ! ((G1 * F1) . a) by FUNCTOR0:33 .= (r * (G1 * F1)) ! a by A2, Th12 .= m ! a by A1, FUNCTOR0:32 ; ::_thesis: verum end; H1 * G1 is_transformable_to H2 * G1 by A2, Th10; hence (r * G1) * F1 = r * (G1 * F1) by A3, Th10, FUNCTOR2:3; ::_thesis: verum end; theorem Th16: :: FUNCTOR3:16 for A, D, B, C being non empty transitive with_units AltCatStr for F1 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for H1 being covariant Functor of C,D for q being transformation of G1,G2 st G1 is_transformable_to G2 holds (H1 * q) * F1 = H1 * (q * F1) proof let A, D, B, C be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for H1 being covariant Functor of C,D for q being transformation of G1,G2 st G1 is_transformable_to G2 holds (H1 * q) * F1 = H1 * (q * F1) let F1 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C for H1 being covariant Functor of C,D for q being transformation of G1,G2 st G1 is_transformable_to G2 holds (H1 * q) * F1 = H1 * (q * F1) let G1, G2 be covariant Functor of B,C; ::_thesis: for H1 being covariant Functor of C,D for q being transformation of G1,G2 st G1 is_transformable_to G2 holds (H1 * q) * F1 = H1 * (q * F1) let H1 be covariant Functor of C,D; ::_thesis: for q being transformation of G1,G2 st G1 is_transformable_to G2 holds (H1 * q) * F1 = H1 * (q * F1) let q be transformation of G1,G2; ::_thesis: ( G1 is_transformable_to G2 implies (H1 * q) * F1 = H1 * (q * F1) ) A1: (H1 * G2) * F1 = H1 * (G2 * F1) by FUNCTOR0:32; then reconsider m = H1 * (q * F1) as transformation of (H1 * G1) * F1,(H1 * G2) * F1 by FUNCTOR0:32; assume A2: G1 is_transformable_to G2 ; ::_thesis: (H1 * q) * F1 = H1 * (q * F1) A3: now__::_thesis:_for_a_being_object_of_A_holds_((H1_*_q)_*_F1)_!_a_=_m_!_a let a be object of A; ::_thesis: ((H1 * q) * F1) ! a = m ! a A4: ( (G1 * F1) . a = G1 . (F1 . a) & (G2 * F1) . a = G2 . (F1 . a) ) by FUNCTOR0:33; thus ((H1 * q) * F1) ! a = (H1 * q) ! (F1 . a) by A2, Th10, Th12 .= H1 . (q ! (F1 . a)) by A2, Th11 .= H1 . ((q * F1) ! a) by A2, A4, Th12 .= (H1 * (q * F1)) ! a by A2, Th10, Th11 .= m ! a by A1, FUNCTOR0:32 ; ::_thesis: verum end; H1 * G1 is_transformable_to H1 * G2 by A2, Th10; hence (H1 * q) * F1 = H1 * (q * F1) by A3, Th10, FUNCTOR2:3; ::_thesis: verum end; theorem Th17: :: FUNCTOR3:17 for C, D, A, B being non empty transitive with_units AltCatStr for F1, F2 being covariant Functor of A,B for G1 being covariant Functor of B,C for H1 being covariant Functor of C,D for p being transformation of F1,F2 st F1 is_transformable_to F2 holds (H1 * G1) * p = H1 * (G1 * p) proof let C, D, A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B for G1 being covariant Functor of B,C for H1 being covariant Functor of C,D for p being transformation of F1,F2 st F1 is_transformable_to F2 holds (H1 * G1) * p = H1 * (G1 * p) let F1, F2 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C for H1 being covariant Functor of C,D for p being transformation of F1,F2 st F1 is_transformable_to F2 holds (H1 * G1) * p = H1 * (G1 * p) let G1 be covariant Functor of B,C; ::_thesis: for H1 being covariant Functor of C,D for p being transformation of F1,F2 st F1 is_transformable_to F2 holds (H1 * G1) * p = H1 * (G1 * p) let H1 be covariant Functor of C,D; ::_thesis: for p being transformation of F1,F2 st F1 is_transformable_to F2 holds (H1 * G1) * p = H1 * (G1 * p) let p be transformation of F1,F2; ::_thesis: ( F1 is_transformable_to F2 implies (H1 * G1) * p = H1 * (G1 * p) ) A1: (H1 * G1) * F2 = H1 * (G1 * F2) by FUNCTOR0:32; then reconsider m = H1 * (G1 * p) as transformation of (H1 * G1) * F1,(H1 * G1) * F2 by FUNCTOR0:32; assume A2: F1 is_transformable_to F2 ; ::_thesis: (H1 * G1) * p = H1 * (G1 * p) now__::_thesis:_for_a_being_object_of_A_holds_((H1_*_G1)_*_p)_!_a_=_m_!_a let a be object of A; ::_thesis: ((H1 * G1) * p) ! a = m ! a A3: ( (G1 * F1) . a = G1 . (F1 . a) & (G1 * F2) . a = G1 . (F2 . a) ) by FUNCTOR0:33; A4: <^(F1 . a),(F2 . a)^> <> {} by A2, FUNCTOR2:def_1; thus ((H1 * G1) * p) ! a = (H1 * G1) . (p ! a) by A2, Th11 .= H1 . (G1 . (p ! a)) by A4, Th6 .= H1 . ((G1 * p) ! a) by A2, A3, Th11 .= (H1 * (G1 * p)) ! a by A2, Th10, Th11 .= m ! a by A1, FUNCTOR0:32 ; ::_thesis: verum end; hence (H1 * G1) * p = H1 * (G1 * p) by A2, Th10, FUNCTOR2:3; ::_thesis: verum end; theorem Th18: :: FUNCTOR3:18 for A, B, C being non empty transitive with_units AltCatStr for F1 being covariant Functor of A,B for G1 being covariant Functor of B,C holds (idt G1) * F1 = idt (G1 * F1) proof let A, B, C be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B for G1 being covariant Functor of B,C holds (idt G1) * F1 = idt (G1 * F1) let F1 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C holds (idt G1) * F1 = idt (G1 * F1) let G1 be covariant Functor of B,C; ::_thesis: (idt G1) * F1 = idt (G1 * F1) now__::_thesis:_for_a_being_object_of_A_holds_((idt_G1)_*_F1)_!_a_=_(idt_(G1_*_F1))_!_a let a be object of A; ::_thesis: ((idt G1) * F1) ! a = (idt (G1 * F1)) ! a thus ((idt G1) * F1) ! a = (idt G1) ! (F1 . a) by Th12 .= idm (G1 . (F1 . a)) by FUNCTOR2:4 .= idm ((G1 * F1) . a) by FUNCTOR0:33 .= (idt (G1 * F1)) ! a by FUNCTOR2:4 ; ::_thesis: verum end; hence (idt G1) * F1 = idt (G1 * F1) by FUNCTOR2:3; ::_thesis: verum end; theorem Th19: :: FUNCTOR3:19 for A, B, C being non empty transitive with_units AltCatStr for F1 being covariant Functor of A,B for G1 being covariant Functor of B,C holds G1 * (idt F1) = idt (G1 * F1) proof let A, B, C be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B for G1 being covariant Functor of B,C holds G1 * (idt F1) = idt (G1 * F1) let F1 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C holds G1 * (idt F1) = idt (G1 * F1) let G1 be covariant Functor of B,C; ::_thesis: G1 * (idt F1) = idt (G1 * F1) now__::_thesis:_for_a_being_object_of_A_holds_(G1_*_(idt_F1))_!_a_=_(idt_(G1_*_F1))_!_a let a be object of A; ::_thesis: (G1 * (idt F1)) ! a = (idt (G1 * F1)) ! a thus (G1 * (idt F1)) ! a = G1 . ((idt F1) ! a) by Th11 .= G1 . (idm (F1 . a)) by FUNCTOR2:4 .= idm (G1 . (F1 . a)) by FUNCTOR2:1 .= idm ((G1 * F1) . a) by FUNCTOR0:33 .= (idt (G1 * F1)) ! a by FUNCTOR2:4 ; ::_thesis: verum end; hence G1 * (idt F1) = idt (G1 * F1) by FUNCTOR2:3; ::_thesis: verum end; theorem Th20: :: FUNCTOR3:20 for A, B being non empty transitive with_units AltCatStr for F1, F2 being covariant Functor of A,B for p being transformation of F1,F2 st F1 is_transformable_to F2 holds (id B) * p = p proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B for p being transformation of F1,F2 st F1 is_transformable_to F2 holds (id B) * p = p let F1, F2 be covariant Functor of A,B; ::_thesis: for p being transformation of F1,F2 st F1 is_transformable_to F2 holds (id B) * p = p let p be transformation of F1,F2; ::_thesis: ( F1 is_transformable_to F2 implies (id B) * p = p ) assume A1: F1 is_transformable_to F2 ; ::_thesis: (id B) * p = p now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_A_holds_ ((id_B)_*_p)_._i_=_p_._i let i be set ; ::_thesis: ( i in the carrier of A implies ((id B) * p) . i = p . i ) assume i in the carrier of A ; ::_thesis: ((id B) * p) . i = p . i then reconsider a = i as object of A ; A2: <^(F1 . a),(F2 . a)^> <> {} by A1, FUNCTOR2:def_1; thus ((id B) * p) . i = (id B) . (p ! a) by A1, Def1 .= p ! a by A2, FUNCTOR0:31 .= p . i by A1, FUNCTOR2:def_4 ; ::_thesis: verum end; hence (id B) * p = p by PBOOLE:3; ::_thesis: verum end; theorem Th21: :: FUNCTOR3:21 for C, B being non empty transitive with_units AltCatStr for G1, G2 being covariant Functor of B,C for q being transformation of G1,G2 st G1 is_transformable_to G2 holds q * (id B) = q proof let C, B be non empty transitive with_units AltCatStr ; ::_thesis: for G1, G2 being covariant Functor of B,C for q being transformation of G1,G2 st G1 is_transformable_to G2 holds q * (id B) = q let G1, G2 be covariant Functor of B,C; ::_thesis: for q being transformation of G1,G2 st G1 is_transformable_to G2 holds q * (id B) = q let q be transformation of G1,G2; ::_thesis: ( G1 is_transformable_to G2 implies q * (id B) = q ) assume A1: G1 is_transformable_to G2 ; ::_thesis: q * (id B) = q now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_B_holds_ (q_*_(id_B))_._i_=_q_._i let i be set ; ::_thesis: ( i in the carrier of B implies (q * (id B)) . i = q . i ) assume i in the carrier of B ; ::_thesis: (q * (id B)) . i = q . i then reconsider a = i as object of B ; thus (q * (id B)) . i = q ! ((id B) . a) by A1, Def2 .= q ! a by FUNCTOR0:29 .= q . i by A1, FUNCTOR2:def_4 ; ::_thesis: verum end; hence q * (id B) = q by PBOOLE:3; ::_thesis: verum end; begin definition let A, B, C be non empty transitive with_units AltCatStr ; let F1, F2 be covariant Functor of A,B; let G1, G2 be covariant Functor of B,C; let t be transformation of F1,F2; let s be transformation of G1,G2; funcs (#) t -> transformation of G1 * F1,G2 * F2 equals :: FUNCTOR3:def 3 (s * F2) `*` (G1 * t); coherence (s * F2) `*` (G1 * t) is transformation of G1 * F1,G2 * F2 ; end; :: deftheorem defines (#) FUNCTOR3:def_3_:_ for A, B, C being non empty transitive with_units AltCatStr for F1, F2 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for t being transformation of F1,F2 for s being transformation of G1,G2 holds s (#) t = (s * F2) `*` (G1 * t); theorem Th22: :: FUNCTOR3:22 for C, A, B being non empty transitive with_units AltCatStr for F1, F2 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for p being transformation of F1,F2 for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds q (#) p = (G2 * p) `*` (q * F1) proof let C, A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for p being transformation of F1,F2 for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds q (#) p = (G2 * p) `*` (q * F1) let F1, F2 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C for p being transformation of F1,F2 for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds q (#) p = (G2 * p) `*` (q * F1) let G1, G2 be covariant Functor of B,C; ::_thesis: for p being transformation of F1,F2 for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds q (#) p = (G2 * p) `*` (q * F1) let p be transformation of F1,F2; ::_thesis: for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds q (#) p = (G2 * p) `*` (q * F1) let q be natural_transformation of G1,G2; ::_thesis: ( F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 implies q (#) p = (G2 * p) `*` (q * F1) ) assume that A1: F1 is_transformable_to F2 and A2: G1 is_naturally_transformable_to G2 ; ::_thesis: q (#) p = (G2 * p) `*` (q * F1) A3: G1 * F1 is_transformable_to G1 * F2 by A1, Th10; A4: G2 * F1 is_transformable_to G2 * F2 by A1, Th10; A5: G1 is_transformable_to G2 by A2, FUNCTOR2:def_6; then A6: G1 * F1 is_transformable_to G2 * F1 by Th10; A7: G1 * F2 is_transformable_to G2 * F2 by A5, Th10; now__::_thesis:_for_a_being_object_of_A_holds_((q_*_F2)_`*`_(G1_*_p))_!_a_=_((G2_*_p)_`*`_(q_*_F1))_!_a let a be object of A; ::_thesis: ((q * F2) `*` (G1 * p)) ! a = ((G2 * p) `*` (q * F1)) ! a A8: G1 . (F1 . a) = (G1 * F1) . a by FUNCTOR0:33; A9: G2 . (F2 . a) = (G2 * F2) . a by FUNCTOR0:33; then reconsider sF2a = q ! (F2 . a) as Morphism of ((G1 * F2) . a),((G2 * F2) . a) by FUNCTOR0:33; reconsider G2ta = (G2 * p) ! a as Morphism of (G2 . (F1 . a)),(G2 . (F2 . a)) by A9, FUNCTOR0:33; A10: G1 . (F2 . a) = (G1 * F2) . a by FUNCTOR0:33; A11: <^(F1 . a),(F2 . a)^> <> {} by A1, FUNCTOR2:def_1; A12: G2 . (F1 . a) = (G2 * F1) . a by FUNCTOR0:33; thus ((q * F2) `*` (G1 * p)) ! a = ((q * F2) ! a) * ((G1 * p) ! a) by A7, A3, FUNCTOR2:def_5 .= sF2a * ((G1 * p) ! a) by A5, Th12 .= (q ! (F2 . a)) * (G1 . (p ! a)) by A1, A8, A10, A9, Th11 .= (G2 . (p ! a)) * (q ! (F1 . a)) by A2, A11, FUNCTOR2:def_7 .= G2ta * (q ! (F1 . a)) by A1, Th11 .= ((G2 * p) ! a) * ((q * F1) ! a) by A5, A8, A12, A9, Th12 .= ((G2 * p) `*` (q * F1)) ! a by A6, A4, FUNCTOR2:def_5 ; ::_thesis: verum end; hence q (#) p = (G2 * p) `*` (q * F1) by A1, A5, Th10, FUNCTOR2:3; ::_thesis: verum end; theorem :: FUNCTOR3:23 for A, B being non empty transitive with_units AltCatStr for F1, F2 being covariant Functor of A,B for p being transformation of F1,F2 st F1 is_transformable_to F2 holds (idt (id B)) (#) p = p proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B for p being transformation of F1,F2 st F1 is_transformable_to F2 holds (idt (id B)) (#) p = p let F1, F2 be covariant Functor of A,B; ::_thesis: for p being transformation of F1,F2 st F1 is_transformable_to F2 holds (idt (id B)) (#) p = p let p be transformation of F1,F2; ::_thesis: ( F1 is_transformable_to F2 implies (idt (id B)) (#) p = p ) assume A1: F1 is_transformable_to F2 ; ::_thesis: (idt (id B)) (#) p = p then A2: (id B) * F1 is_transformable_to (id B) * F2 by Th10; thus (idt (id B)) (#) p = (idt ((id B) * F2)) `*` ((id B) * p) by Th18 .= (id B) * p by A2, FUNCTOR2:5 .= p by A1, Th20 ; ::_thesis: verum end; theorem :: FUNCTOR3:24 for C, B being non empty transitive with_units AltCatStr for G1, G2 being covariant Functor of B,C for q being transformation of G1,G2 st G1 is_transformable_to G2 holds q (#) (idt (id B)) = q proof let C, B be non empty transitive with_units AltCatStr ; ::_thesis: for G1, G2 being covariant Functor of B,C for q being transformation of G1,G2 st G1 is_transformable_to G2 holds q (#) (idt (id B)) = q let G1, G2 be covariant Functor of B,C; ::_thesis: for q being transformation of G1,G2 st G1 is_transformable_to G2 holds q (#) (idt (id B)) = q let q be transformation of G1,G2; ::_thesis: ( G1 is_transformable_to G2 implies q (#) (idt (id B)) = q ) assume A1: G1 is_transformable_to G2 ; ::_thesis: q (#) (idt (id B)) = q then A2: G1 * (id B) is_transformable_to G2 * (id B) by Th10; thus q (#) (idt (id B)) = (q * (id B)) `*` (idt (G1 * (id B))) by Th19 .= q * (id B) by A2, FUNCTOR2:5 .= q by A1, Th21 ; ::_thesis: verum end; theorem :: FUNCTOR3:25 for C, A, B being non empty transitive with_units AltCatStr for F1, F2 being covariant Functor of A,B for G1 being covariant Functor of B,C for p being transformation of F1,F2 st F1 is_transformable_to F2 holds G1 * p = (idt G1) (#) p proof let C, A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B for G1 being covariant Functor of B,C for p being transformation of F1,F2 st F1 is_transformable_to F2 holds G1 * p = (idt G1) (#) p let F1, F2 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C for p being transformation of F1,F2 st F1 is_transformable_to F2 holds G1 * p = (idt G1) (#) p let G1 be covariant Functor of B,C; ::_thesis: for p being transformation of F1,F2 st F1 is_transformable_to F2 holds G1 * p = (idt G1) (#) p let p be transformation of F1,F2; ::_thesis: ( F1 is_transformable_to F2 implies G1 * p = (idt G1) (#) p ) assume F1 is_transformable_to F2 ; ::_thesis: G1 * p = (idt G1) (#) p then G1 * F1 is_transformable_to G1 * F2 by Th10; hence G1 * p = (idt (G1 * F2)) `*` (G1 * p) by FUNCTOR2:5 .= (idt G1) (#) p by Th18 ; ::_thesis: verum end; theorem :: FUNCTOR3:26 for A, B, C being non empty transitive with_units AltCatStr for F1 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for q being transformation of G1,G2 st G1 is_transformable_to G2 holds q * F1 = q (#) (idt F1) proof let A, B, C be non empty transitive with_units AltCatStr ; ::_thesis: for F1 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for q being transformation of G1,G2 st G1 is_transformable_to G2 holds q * F1 = q (#) (idt F1) let F1 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C for q being transformation of G1,G2 st G1 is_transformable_to G2 holds q * F1 = q (#) (idt F1) let G1, G2 be covariant Functor of B,C; ::_thesis: for q being transformation of G1,G2 st G1 is_transformable_to G2 holds q * F1 = q (#) (idt F1) let q be transformation of G1,G2; ::_thesis: ( G1 is_transformable_to G2 implies q * F1 = q (#) (idt F1) ) assume G1 is_transformable_to G2 ; ::_thesis: q * F1 = q (#) (idt F1) then G1 * F1 is_transformable_to G2 * F1 by Th10; hence q * F1 = (q * F1) `*` (idt (G1 * F1)) by FUNCTOR2:5 .= q (#) (idt F1) by Th19 ; ::_thesis: verum end; theorem :: FUNCTOR3:27 for A, B, C, D being category for F1, F2 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for H1, H2 being covariant Functor of C,D for t being transformation of F1,F2 for s being transformation of G1,G2 for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds (u (#) s) (#) t = u (#) (s (#) t) proof let A, B, C, D be category; ::_thesis: for F1, F2 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for H1, H2 being covariant Functor of C,D for t being transformation of F1,F2 for s being transformation of G1,G2 for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds (u (#) s) (#) t = u (#) (s (#) t) let F1, F2 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C for H1, H2 being covariant Functor of C,D for t being transformation of F1,F2 for s being transformation of G1,G2 for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds (u (#) s) (#) t = u (#) (s (#) t) let G1, G2 be covariant Functor of B,C; ::_thesis: for H1, H2 being covariant Functor of C,D for t being transformation of F1,F2 for s being transformation of G1,G2 for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds (u (#) s) (#) t = u (#) (s (#) t) let H1, H2 be covariant Functor of C,D; ::_thesis: for t being transformation of F1,F2 for s being transformation of G1,G2 for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds (u (#) s) (#) t = u (#) (s (#) t) let t be transformation of F1,F2; ::_thesis: for s being transformation of G1,G2 for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds (u (#) s) (#) t = u (#) (s (#) t) let s be transformation of G1,G2; ::_thesis: for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds (u (#) s) (#) t = u (#) (s (#) t) let u be transformation of H1,H2; ::_thesis: ( F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 implies (u (#) s) (#) t = u (#) (s (#) t) ) assume that A1: F1 is_transformable_to F2 and A2: G1 is_transformable_to G2 and A3: H1 is_transformable_to H2 ; ::_thesis: (u (#) s) (#) t = u (#) (s (#) t) A4: ( G1 * F2 is_transformable_to G2 * F2 & G1 * F1 is_transformable_to G1 * F2 ) by A1, A2, Th10; A5: ( (H1 * s) * F2 = H1 * (s * F2) & (H1 * G1) * t = H1 * (G1 * t) ) by A1, A2, Th16, Th17; A6: ( (H1 * G2) * F2 = H1 * (G2 * F2) & (H2 * G2) * F2 = H2 * (G2 * F2) ) by FUNCTOR0:32; A7: ( (H1 * G1) * F1 is_transformable_to (H1 * G1) * F2 & (u * G2) * F2 = u * (G2 * F2) ) by A1, A3, Th10, Th15; A8: ( (H1 * G1) * F1 = H1 * (G1 * F1) & (H1 * G1) * F2 = H1 * (G1 * F2) ) by FUNCTOR0:32; A9: H1 * G1 is_transformable_to H1 * G2 by A2, Th10; then A10: (H1 * G1) * F2 is_transformable_to (H1 * G2) * F2 by Th10; A11: H1 * G2 is_transformable_to H2 * G2 by A3, Th10; then A12: (H1 * G2) * F2 is_transformable_to (H2 * G2) * F2 by Th10; thus (u (#) s) (#) t = (((u * G2) * F2) `*` ((H1 * s) * F2)) `*` ((H1 * G1) * t) by A11, A9, Th14 .= (u * (G2 * F2)) `*` ((H1 * (s * F2)) `*` (H1 * (G1 * t))) by A12, A10, A7, A5, A8, A6, FUNCTOR2:6 .= u (#) (s (#) t) by A4, Th13 ; ::_thesis: verum end; Lm2: now__::_thesis:_for_A,_B,_C_being_category for_F1,_F2_being_covariant_Functor_of_A,B for_G1,_G2_being_covariant_Functor_of_B,C for_s_being_natural_transformation_of_G1,G2 for_t_being_natural_transformation_of_F1,F2_st_F1_is_naturally_transformable_to_F2_&_G1_is_naturally_transformable_to_G2_holds_ (_G1_*_F1_is_naturally_transformable_to_G2_*_F2_&_s_(#)_t_is_natural_transformation_of_G1_*_F1,G2_*_F2_) let A, B, C be category; ::_thesis: for F1, F2 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for s being natural_transformation of G1,G2 for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) let F1, F2 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C for s being natural_transformation of G1,G2 for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) let G1, G2 be covariant Functor of B,C; ::_thesis: for s being natural_transformation of G1,G2 for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) let s be natural_transformation of G1,G2; ::_thesis: for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) let t be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) ) set k = s (#) t; assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: ( G1 is_naturally_transformable_to G2 implies ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) ) then A2: F1 is_transformable_to F2 by FUNCTOR2:def_6; assume A3: G1 is_naturally_transformable_to G2 ; ::_thesis: ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) then A4: G1 is_transformable_to G2 by FUNCTOR2:def_6; A5: now__::_thesis:_for_a,_b_being_object_of_A_st_<^a,b^>_<>_{}_holds_ for_f_being_Morphism_of_a,b_holds_((s_(#)_t)_!_b)_*_((G1_*_F1)_._f)_=_((G2_*_F2)_._f)_*_((s_(#)_t)_!_a) let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds ((s (#) t) ! b) * ((G1 * F1) . f) = ((G2 * F2) . f) * ((s (#) t) ! a) ) assume A6: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds ((s (#) t) ! b) * ((G1 * F1) . f) = ((G2 * F2) . f) * ((s (#) t) ! a) A7: <^((G1 * F1) . a),((G1 * F1) . b)^> <> {} by A6, FUNCTOR0:def_18; A8: (G2 * F2) . a = G2 . (F2 . a) by FUNCTOR0:33; then reconsider sF2a = s ! (F2 . a) as Morphism of ((G1 * F2) . a),((G2 * F2) . a) by FUNCTOR0:33; A9: (G2 * F2) . b = G2 . (F2 . b) by FUNCTOR0:33; then reconsider sF2b = s ! (F2 . b) as Morphism of ((G1 * F2) . b),((G2 * F2) . b) by FUNCTOR0:33; <^(G1 . (F2 . b)),(G2 . (F2 . b))^> <> {} by A4, FUNCTOR2:def_1; then A10: <^((G1 * F2) . b),((G2 * F2) . b)^> <> {} by A9, FUNCTOR0:33; let f be Morphism of a,b; ::_thesis: ((s (#) t) ! b) * ((G1 * F1) . f) = ((G2 * F2) . f) * ((s (#) t) ! a) A11: (G1 * F1) . a = G1 . (F1 . a) by FUNCTOR0:33; then reconsider G1tbF1f = G1 . ((t ! b) * (F1 . f)) as Morphism of ((G1 * F1) . a),((G1 * F2) . b) by FUNCTOR0:33; reconsider G1ta = G1 . (t ! a) as Morphism of ((G1 * F1) . a),((G1 * F2) . a) by A11, FUNCTOR0:33; A12: <^(G1 . (F1 . a)),(G2 . (F1 . a))^> <> {} by A4, FUNCTOR2:def_1; A13: (G1 * F1) . b = G1 . (F1 . b) by FUNCTOR0:33; then reconsider G1tb = G1 . (t ! b) as Morphism of ((G1 * F1) . b),((G1 * F2) . b) by FUNCTOR0:33; A14: <^(F1 . b),(F2 . b)^> <> {} by A2, FUNCTOR2:def_1; then <^(G1 . (F1 . b)),(G1 . (F2 . b))^> <> {} by FUNCTOR0:def_18; then A15: <^((G1 * F1) . b),((G1 * F2) . b)^> <> {} by A13, FUNCTOR0:33; A16: <^(F1 . a),(F1 . b)^> <> {} by A6, FUNCTOR0:def_18; then A17: <^(F1 . a),(F2 . b)^> <> {} by A14, ALTCAT_1:def_2; reconsider G1F1f = G1 . (F1 . f) as Morphism of ((G1 * F1) . a),((G1 * F1) . b) by A13, FUNCTOR0:33; A18: s ! (F2 . a) = (s * F2) . a by A4, Def2; A19: G1 . ((t ! b) * (F1 . f)) = (G1 . (t ! b)) * (G1 . (F1 . f)) by A14, A16, FUNCTOR0:def_23 .= G1tb * G1F1f by A11, A13, FUNCTOR0:33 ; reconsider G2F2f = G2 . (F2 . f) as Morphism of ((G2 * F2) . a),((G2 * F2) . b) by A8, FUNCTOR0:33; A20: s ! (F2 . b) = (s * F2) . b by A4, Def2; A21: G1 * F2 is_transformable_to G2 * F2 by A4, Th10; A22: <^(F2 . a),(F2 . b)^> <> {} by A6, FUNCTOR0:def_18; then A23: <^(G2 . (F2 . a)),(G2 . (F2 . b))^> <> {} by FUNCTOR0:def_18; A24: <^(F1 . a),(F2 . a)^> <> {} by A2, FUNCTOR2:def_1; then A25: <^(G2 . (F1 . a)),(G2 . (F2 . a))^> <> {} by FUNCTOR0:def_18; A26: G1 * F1 is_transformable_to G1 * F2 by A2, Th10; hence ((s (#) t) ! b) * ((G1 * F1) . f) = (((s * F2) ! b) * ((G1 * t) ! b)) * ((G1 * F1) . f) by A21, FUNCTOR2:def_5 .= (sF2b * ((G1 * t) ! b)) * ((G1 * F1) . f) by A21, A20, FUNCTOR2:def_4 .= (sF2b * G1tb) * ((G1 * F1) . f) by A2, Th11 .= (sF2b * G1tb) * G1F1f by A6, Th6 .= sF2b * G1tbF1f by A7, A15, A10, A19, ALTCAT_1:21 .= (s ! (F2 . b)) * (G1 . ((t ! b) * (F1 . f))) by A11, A9, FUNCTOR0:33 .= (G2 . ((t ! b) * (F1 . f))) * (s ! (F1 . a)) by A3, A17, FUNCTOR2:def_7 .= (G2 . ((F2 . f) * (t ! a))) * (s ! (F1 . a)) by A1, A6, FUNCTOR2:def_7 .= ((G2 . (F2 . f)) * (G2 . (t ! a))) * (s ! (F1 . a)) by A22, A24, FUNCTOR0:def_23 .= (G2 . (F2 . f)) * ((G2 . (t ! a)) * (s ! (F1 . a))) by A12, A25, A23, ALTCAT_1:21 .= (G2 . (F2 . f)) * ((s ! (F2 . a)) * (G1 . (t ! a))) by A3, A24, FUNCTOR2:def_7 .= G2F2f * (sF2a * G1ta) by A11, A8, A9, FUNCTOR0:33 .= ((G2 * F2) . f) * (sF2a * G1ta) by A6, Th6 .= ((G2 * F2) . f) * (((s * F2) ! a) * G1ta) by A21, A18, FUNCTOR2:def_4 .= ((G2 * F2) . f) * (((s * F2) ! a) * ((G1 * t) ! a)) by A2, Th11 .= ((G2 * F2) . f) * ((s (#) t) ! a) by A21, A26, FUNCTOR2:def_5 ; ::_thesis: verum end; thus G1 * F1 is_naturally_transformable_to G2 * F2 ::_thesis: s (#) t is natural_transformation of G1 * F1,G2 * F2 proof thus G1 * F1 is_transformable_to G2 * F2 by A2, A4, Th10; :: according to FUNCTOR2:def_6 ::_thesis: ex b1 being transformation of G1 * F1,G2 * F2 st for b2, b3 being M2( the carrier of A) holds ( <^b2,b3^> = {} or for b4 being M2(<^b2,b3^>) holds (b1 ! b3) * ((G1 * F1) . b4) = ((G2 * F2) . b4) * (b1 ! b2) ) take s (#) t ; ::_thesis: for b1, b2 being M2( the carrier of A) holds ( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((s (#) t) ! b2) * ((G1 * F1) . b3) = ((G2 * F2) . b3) * ((s (#) t) ! b1) ) thus for b1, b2 being M2( the carrier of A) holds ( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((s (#) t) ! b2) * ((G1 * F1) . b3) = ((G2 * F2) . b3) * ((s (#) t) ! b1) ) by A5; ::_thesis: verum end; hence s (#) t is natural_transformation of G1 * F1,G2 * F2 by A5, FUNCTOR2:def_7; ::_thesis: verum end; theorem Th28: :: FUNCTOR3:28 for C, A, B being category for F1, F2 being covariant Functor of A,B for G1 being covariant Functor of B,C for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds G1 * t is natural_transformation of G1 * F1,G1 * F2 proof let C, A, B be category; ::_thesis: for F1, F2 being covariant Functor of A,B for G1 being covariant Functor of B,C for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds G1 * t is natural_transformation of G1 * F1,G1 * F2 let F1, F2 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds G1 * t is natural_transformation of G1 * F1,G1 * F2 let G1 be covariant Functor of B,C; ::_thesis: for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds G1 * t is natural_transformation of G1 * F1,G1 * F2 let t be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 implies G1 * t is natural_transformation of G1 * F1,G1 * F2 ) assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: G1 * t is natural_transformation of G1 * F1,G1 * F2 then A2: F1 is_transformable_to F2 by FUNCTOR2:def_6; thus G1 * F1 is_naturally_transformable_to G1 * F2 by A1, Lm2; :: according to FUNCTOR2:def_7 ::_thesis: for b1, b2 being M2( the carrier of A) holds ( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((G1 * t) ! b2) * ((G1 * F1) . b3) = ((G1 * F2) . b3) * ((G1 * t) ! b1) ) let a, b be object of A; ::_thesis: ( <^a,b^> = {} or for b1 being M2(<^a,b^>) holds ((G1 * t) ! b) * ((G1 * F1) . b1) = ((G1 * F2) . b1) * ((G1 * t) ! a) ) assume A3: <^a,b^> <> {} ; ::_thesis: for b1 being M2(<^a,b^>) holds ((G1 * t) ! b) * ((G1 * F1) . b1) = ((G1 * F2) . b1) * ((G1 * t) ! a) A4: ( (G1 * F1) . b = G1 . (F1 . b) & <^(F1 . a),(F1 . b)^> <> {} ) by A3, FUNCTOR0:33, FUNCTOR0:def_18; A5: <^(F1 . b),(F2 . b)^> <> {} by A2, FUNCTOR2:def_1; A6: <^(F1 . a),(F2 . a)^> <> {} by A2, FUNCTOR2:def_1; reconsider G1ta = G1 . (t ! a) as Morphism of (G1 . (F1 . a)),((G1 * F2) . a) by FUNCTOR0:33; reconsider G1tb = G1 . (t ! b) as Morphism of ((G1 * F1) . b),(G1 . (F2 . b)) by FUNCTOR0:33; let f be Morphism of a,b; ::_thesis: ((G1 * t) ! b) * ((G1 * F1) . f) = ((G1 * F2) . f) * ((G1 * t) ! a) A7: (G1 * F2) . a = G1 . (F2 . a) by FUNCTOR0:33; A8: <^(F2 . a),(F2 . b)^> <> {} by A3, FUNCTOR0:def_18; A9: (G1 * F1) . a = G1 . (F1 . a) by FUNCTOR0:33; then reconsider G1F1f = G1 . (F1 . f) as Morphism of ((G1 * F1) . a),((G1 * F1) . b) by FUNCTOR0:33; A10: (G1 * F2) . b = G1 . (F2 . b) by FUNCTOR0:33; hence ((G1 * t) ! b) * ((G1 * F1) . f) = G1tb * ((G1 * F1) . f) by A2, Th11 .= G1tb * G1F1f by A3, Th6 .= G1 . ((t ! b) * (F1 . f)) by A9, A4, A5, FUNCTOR0:def_23 .= G1 . ((F2 . f) * (t ! a)) by A1, A3, FUNCTOR2:def_7 .= (G1 . (F2 . f)) * (G1 . (t ! a)) by A6, A8, FUNCTOR0:def_23 .= ((G1 * F2) . f) * G1ta by A3, A7, A10, Th6 .= ((G1 * F2) . f) * ((G1 * t) ! a) by A2, A9, Th11 ; ::_thesis: verum end; theorem Th29: :: FUNCTOR3:29 for A, B, C being category for F1 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for s being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds s * F1 is natural_transformation of G1 * F1,G2 * F1 proof let A, B, C be category; ::_thesis: for F1 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for s being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds s * F1 is natural_transformation of G1 * F1,G2 * F1 let F1 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C for s being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds s * F1 is natural_transformation of G1 * F1,G2 * F1 let G1, G2 be covariant Functor of B,C; ::_thesis: for s being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds s * F1 is natural_transformation of G1 * F1,G2 * F1 let s be natural_transformation of G1,G2; ::_thesis: ( G1 is_naturally_transformable_to G2 implies s * F1 is natural_transformation of G1 * F1,G2 * F1 ) assume A1: G1 is_naturally_transformable_to G2 ; ::_thesis: s * F1 is natural_transformation of G1 * F1,G2 * F1 thus G1 * F1 is_naturally_transformable_to G2 * F1 by A1, Lm2; :: according to FUNCTOR2:def_7 ::_thesis: for b1, b2 being M2( the carrier of A) holds ( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((s * F1) ! b2) * ((G1 * F1) . b3) = ((G2 * F1) . b3) * ((s * F1) ! b1) ) let a, b be object of A; ::_thesis: ( <^a,b^> = {} or for b1 being M2(<^a,b^>) holds ((s * F1) ! b) * ((G1 * F1) . b1) = ((G2 * F1) . b1) * ((s * F1) ! a) ) assume A2: <^a,b^> <> {} ; ::_thesis: for b1 being M2(<^a,b^>) holds ((s * F1) ! b) * ((G1 * F1) . b1) = ((G2 * F1) . b1) * ((s * F1) ! a) A3: <^(F1 . a),(F1 . b)^> <> {} by A2, FUNCTOR0:def_18; reconsider sF1a = s ! (F1 . a) as Morphism of (G1 . (F1 . a)),((G2 * F1) . a) by FUNCTOR0:33; let f be Morphism of a,b; ::_thesis: ((s * F1) ! b) * ((G1 * F1) . f) = ((G2 * F1) . f) * ((s * F1) ! a) A4: (G2 * F1) . a = G2 . (F1 . a) by FUNCTOR0:33; A5: (G2 * F1) . b = G2 . (F1 . b) by FUNCTOR0:33; then reconsider sF1b = s ! (F1 . b) as Morphism of ((G1 * F1) . b),((G2 * F1) . b) by FUNCTOR0:33; A6: ( (G1 * F1) . b = G1 . (F1 . b) & (G2 * F1) . b = G2 . (F1 . b) ) by FUNCTOR0:33; A7: (G1 * F1) . a = G1 . (F1 . a) by FUNCTOR0:33; then reconsider G1F1f = G1 . (F1 . f) as Morphism of ((G1 * F1) . a),((G1 * F1) . b) by FUNCTOR0:33; A8: G1 is_transformable_to G2 by A1, FUNCTOR2:def_6; hence ((s * F1) ! b) * ((G1 * F1) . f) = sF1b * ((G1 * F1) . f) by Th12 .= sF1b * G1F1f by A2, Th6 .= (G2 . (F1 . f)) * (s ! (F1 . a)) by A1, A7, A6, A3, FUNCTOR2:def_7 .= ((G2 * F1) . f) * sF1a by A2, A4, A5, Th6 .= ((G2 * F1) . f) * ((s * F1) ! a) by A8, A7, Th12 ; ::_thesis: verum end; theorem :: FUNCTOR3:30 for A, B, C being category for F1, F2 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for t being natural_transformation of F1,F2 for s being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) by Lm2; theorem :: FUNCTOR3:31 for A, B, C being category for F1, F2, F3 being covariant Functor of A,B for G1, G2, G3 being covariant Functor of B,C for s being natural_transformation of G1,G2 for s1 being natural_transformation of G2,G3 for t being transformation of F1,F2 for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t) proof let A, B, C be category; ::_thesis: for F1, F2, F3 being covariant Functor of A,B for G1, G2, G3 being covariant Functor of B,C for s being natural_transformation of G1,G2 for s1 being natural_transformation of G2,G3 for t being transformation of F1,F2 for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t) let F1, F2, F3 be covariant Functor of A,B; ::_thesis: for G1, G2, G3 being covariant Functor of B,C for s being natural_transformation of G1,G2 for s1 being natural_transformation of G2,G3 for t being transformation of F1,F2 for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t) let G1, G2, G3 be covariant Functor of B,C; ::_thesis: for s being natural_transformation of G1,G2 for s1 being natural_transformation of G2,G3 for t being transformation of F1,F2 for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t) let s be natural_transformation of G1,G2; ::_thesis: for s1 being natural_transformation of G2,G3 for t being transformation of F1,F2 for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t) let s1 be natural_transformation of G2,G3; ::_thesis: for t being transformation of F1,F2 for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t) let t be transformation of F1,F2; ::_thesis: for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t) let t1 be transformation of F2,F3; ::_thesis: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 implies (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t) ) assume that A1: F1 is_naturally_transformable_to F2 and A2: F2 is_naturally_transformable_to F3 and A3: G1 is_naturally_transformable_to G2 and A4: G2 is_naturally_transformable_to G3 ; ::_thesis: (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t) A5: F1 is_transformable_to F2 by A1, FUNCTOR2:def_6; then A6: s (#) t = (G2 * t) `*` (s * F1) by A3, Th22; A7: G2 * F1 is_transformable_to G2 * F2 by A5, Th10; A8: G3 * F1 is_transformable_to G3 * F2 by A5, Th10; G1 * F1 is_naturally_transformable_to G2 * F2 by A1, A3, Lm2; then A9: G1 * F1 is_transformable_to G2 * F2 by FUNCTOR2:def_6; A10: G1 is_transformable_to G2 by A3, FUNCTOR2:def_6; then A11: G1 * F1 is_transformable_to G2 * F1 by Th10; A12: F2 is_transformable_to F3 by A2, FUNCTOR2:def_6; then A13: s1 (#) t1 = (G3 * t1) `*` (s1 * F2) by A4, Th22; A14: G3 * F2 is_transformable_to G3 * F3 by A12, Th10; A15: G2 is_transformable_to G3 by A4, FUNCTOR2:def_6; then A16: G2 * F1 is_transformable_to G3 * F1 by Th10; G1 is_transformable_to G3 by A10, A15, FUNCTOR2:2; then A17: G1 * F1 is_transformable_to G3 * F1 by Th10; A18: G2 * F2 is_transformable_to G3 * F2 by A15, Th10; F1 is_transformable_to F3 by A5, A12, FUNCTOR2:2; hence (s1 `*` s) (#) (t1 `*` t) = (G3 * (t1 `*` t)) `*` ((s1 `*` s) * F1) by A3, A4, Th22, FUNCTOR2:8 .= ((G3 * t1) `*` (G3 * t)) `*` ((s1 `*` s) * F1) by A5, A12, Th13 .= ((G3 * t1) `*` (G3 * t)) `*` ((s1 `*` s) * F1) by A3, A4, FUNCTOR2:def_8 .= ((G3 * t1) `*` (G3 * t)) `*` ((s1 * F1) `*` (s * F1)) by A10, A15, Th14 .= (G3 * t1) `*` ((G3 * t) `*` ((s1 * F1) `*` (s * F1))) by A14, A8, A17, FUNCTOR2:6 .= (G3 * t1) `*` (((G3 * t) `*` (s1 * F1)) `*` (s * F1)) by A8, A11, A16, FUNCTOR2:6 .= (G3 * t1) `*` ((s1 (#) t) `*` (s * F1)) by A4, A5, Th22 .= (G3 * t1) `*` ((s1 * F2) `*` ((G2 * t) `*` (s * F1))) by A11, A18, A7, FUNCTOR2:6 .= (s1 (#) t1) `*` (s (#) t) by A14, A18, A9, A13, A6, FUNCTOR2:6 ; ::_thesis: verum end; begin theorem Th32: :: FUNCTOR3:32 for B, A being category for F1, F2 being covariant Functor of A,B for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ( for a being object of A holds t ! a is iso ) holds ( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st for a being object of A holds ( f . a = (t ! a) " & f ! a is iso ) ) proof let B, A be category; ::_thesis: for F1, F2 being covariant Functor of A,B for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ( for a being object of A holds t ! a is iso ) holds ( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st for a being object of A holds ( f . a = (t ! a) " & f ! a is iso ) ) let F1, F2 be covariant Functor of A,B; ::_thesis: for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ( for a being object of A holds t ! a is iso ) holds ( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st for a being object of A holds ( f . a = (t ! a) " & f ! a is iso ) ) let t be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ( for a being object of A holds t ! a is iso ) implies ( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st for a being object of A holds ( f . a = (t ! a) " & f ! a is iso ) ) ) assume that A1: F1 is_naturally_transformable_to F2 and A2: F2 is_transformable_to F1 and A3: for a being object of A holds t ! a is iso ; ::_thesis: ( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st for a being object of A holds ( f . a = (t ! a) " & f ! a is iso ) ) defpred S1[ set , set ] means ex a being object of A st ( a = \$1 & \$2 = (t ! a) " ); set I = the carrier of A; A4: for i being set st i in the carrier of A holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in the carrier of A implies ex j being set st S1[i,j] ) assume i in the carrier of A ; ::_thesis: ex j being set st S1[i,j] then reconsider o = i as object of A ; take (t ! o) " ; ::_thesis: S1[i,(t ! o) " ] thus S1[i,(t ! o) " ] ; ::_thesis: verum end; consider f being ManySortedSet of the carrier of A such that A5: for i being set st i in the carrier of A holds S1[i,f . i] from PBOOLE:sch_3(A4); f is transformation of F2,F1 proof thus F2 is_transformable_to F1 by A2; :: according to FUNCTOR2:def_2 ::_thesis: for b1 being M2( the carrier of A) holds f . b1 is M2(<^(F2 . b1),(F1 . b1)^>) let a be object of A; ::_thesis: f . a is M2(<^(F2 . a),(F1 . a)^>) ex b being object of A st ( b = a & f . a = (t ! b) " ) by A5; hence f . a is M2(<^(F2 . a),(F1 . a)^>) ; ::_thesis: verum end; then reconsider f = f as transformation of F2,F1 ; A6: F1 is_transformable_to F2 by A1, FUNCTOR2:def_6; A7: now__::_thesis:_for_a,_b_being_object_of_A_st_<^a,b^>_<>_{}_holds_ for_g_being_Morphism_of_a,b_holds_(f_!_b)_*_(F2_._g)_=_(F1_._g)_*_(f_!_a) let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for g being Morphism of a,b holds (f ! b) * (F2 . g) = (F1 . g) * (f ! a) ) assume A8: <^a,b^> <> {} ; ::_thesis: for g being Morphism of a,b holds (f ! b) * (F2 . g) = (F1 . g) * (f ! a) A9: <^(F1 . a),(F1 . b)^> <> {} by A8, FUNCTOR0:def_18; let g be Morphism of a,b; ::_thesis: (f ! b) * (F2 . g) = (F1 . g) * (f ! a) A10: ex bb being object of A st ( bb = b & f . b = (t ! bb) " ) by A5; A11: t ! b is iso by A3; A12: <^(F2 . a),(F1 . a)^> <> {} by A2, FUNCTOR2:def_1; A13: <^(F1 . a),(F2 . a)^> <> {} by A6, FUNCTOR2:def_1; A14: ex aa being object of A st ( aa = a & f . a = (t ! aa) " ) by A5; then reconsider fa = f . a as Morphism of (F2 . a),(F1 . a) ; A15: t ! a is iso by A3; A16: <^(F1 . b),(F2 . b)^> <> {} by A6, FUNCTOR2:def_1; A17: <^(F2 . b),(F1 . b)^> <> {} by A2, FUNCTOR2:def_1; A18: <^(F2 . a),(F2 . b)^> <> {} by A8, FUNCTOR0:def_18; then A19: <^(F2 . a),(F1 . b)^> <> {} by A17, ALTCAT_1:def_2; hence (f ! b) * (F2 . g) = ((f ! b) * (F2 . g)) * (idm (F2 . a)) by ALTCAT_1:def_17 .= ((f ! b) * (F2 . g)) * ((t ! a) * fa) by A14, A15, ALTCAT_3:def_5 .= ((f ! b) * (F2 . g)) * ((t ! a) * (f ! a)) by A2, FUNCTOR2:def_4 .= (((f ! b) * (F2 . g)) * (t ! a)) * (f ! a) by A13, A12, A19, ALTCAT_1:21 .= ((f ! b) * ((F2 . g) * (t ! a))) * (f ! a) by A13, A17, A18, ALTCAT_1:21 .= ((f ! b) * ((t ! b) * (F1 . g))) * (f ! a) by A1, A8, FUNCTOR2:def_7 .= (((f ! b) * (t ! b)) * (F1 . g)) * (f ! a) by A17, A16, A9, ALTCAT_1:21 .= ((((t ! b) ") * (t ! b)) * (F1 . g)) * (f ! a) by A2, A10, FUNCTOR2:def_4 .= ((idm (F1 . b)) * (F1 . g)) * (f ! a) by A11, ALTCAT_3:def_5 .= (F1 . g) * (f ! a) by A9, ALTCAT_1:20 ; ::_thesis: verum end; hence F2 is_naturally_transformable_to F1 by A2, FUNCTOR2:def_6; ::_thesis: ex f being natural_transformation of F2,F1 st for a being object of A holds ( f . a = (t ! a) " & f ! a is iso ) F2 is_naturally_transformable_to F1 by A2, A7, FUNCTOR2:def_6; then reconsider f = f as natural_transformation of F2,F1 by A7, FUNCTOR2:def_7; take f ; ::_thesis: for a being object of A holds ( f . a = (t ! a) " & f ! a is iso ) let a be object of A; ::_thesis: ( f . a = (t ! a) " & f ! a is iso ) consider b being object of A such that A20: b = a and A21: f . a = (t ! b) " by A5; thus f . a = (t ! a) " by A20, A21; ::_thesis: f ! a is iso A22: <^(F1 . a),(F2 . a)^> <> {} by A6, FUNCTOR2:def_1; A23: <^(F2 . a),(F1 . a)^> <> {} by A2, FUNCTOR2:def_1; f ! a = (t ! b) " by A2, A21, FUNCTOR2:def_4; hence f ! a is iso by A3, A20, A22, A23, ALTCAT_4:3; ::_thesis: verum end; definition let A, B be category; let F1, F2 be covariant Functor of A,B; predF1,F2 are_naturally_equivalent means :Def4: :: FUNCTOR3:def 4 ( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ex t being natural_transformation of F1,F2 st for a being object of A holds t ! a is iso ); reflexivity for F1 being covariant Functor of A,B holds ( F1 is_naturally_transformable_to F1 & F1 is_transformable_to F1 & ex t being natural_transformation of F1,F1 st for a being object of A holds t ! a is iso ) proof let F be covariant Functor of A,B; ::_thesis: ( F is_naturally_transformable_to F & F is_transformable_to F & ex t being natural_transformation of F,F st for a being object of A holds t ! a is iso ) thus ( F is_naturally_transformable_to F & F is_transformable_to F ) ; ::_thesis: ex t being natural_transformation of F,F st for a being object of A holds t ! a is iso take idt F ; ::_thesis: for a being object of A holds (idt F) ! a is iso let a be object of A; ::_thesis: (idt F) ! a is iso (idt F) ! a = idm (F . a) by FUNCTOR2:4; hence (idt F) ! a is iso ; ::_thesis: verum end; symmetry for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ex t being natural_transformation of F1,F2 st for a being object of A holds t ! a is iso holds ( F2 is_naturally_transformable_to F1 & F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st for a being object of A holds t ! a is iso ) proof let F1, F2 be covariant Functor of A,B; ::_thesis: ( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ex t being natural_transformation of F1,F2 st for a being object of A holds t ! a is iso implies ( F2 is_naturally_transformable_to F1 & F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st for a being object of A holds t ! a is iso ) ) assume that A1: F1 is_naturally_transformable_to F2 and A2: F2 is_transformable_to F1 ; ::_thesis: ( for t being natural_transformation of F1,F2 holds not for a being object of A holds t ! a is iso or ( F2 is_naturally_transformable_to F1 & F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st for a being object of A holds t ! a is iso ) ) given t being natural_transformation of F1,F2 such that A3: for a being object of A holds t ! a is iso ; ::_thesis: ( F2 is_naturally_transformable_to F1 & F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st for a being object of A holds t ! a is iso ) consider f being natural_transformation of F2,F1 such that A4: for a being object of A holds ( f . a = (t ! a) " & f ! a is iso ) by A1, A2, A3, Th32; thus F2 is_naturally_transformable_to F1 by A1, A2, A3, Th32; ::_thesis: ( F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st for a being object of A holds t ! a is iso ) thus F1 is_transformable_to F2 by A1, FUNCTOR2:def_6; ::_thesis: ex t being natural_transformation of F2,F1 st for a being object of A holds t ! a is iso take f ; ::_thesis: for a being object of A holds f ! a is iso thus for a being object of A holds f ! a is iso by A4; ::_thesis: verum end; end; :: deftheorem Def4 defines are_naturally_equivalent FUNCTOR3:def_4_:_ for A, B being category for F1, F2 being covariant Functor of A,B holds ( F1,F2 are_naturally_equivalent iff ( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ex t being natural_transformation of F1,F2 st for a being object of A holds t ! a is iso ) ); definition let A, B be category; let F1, F2 be covariant Functor of A,B; assume A1: F1,F2 are_naturally_equivalent ; mode natural_equivalence of F1,F2 -> natural_transformation of F1,F2 means :Def5: :: FUNCTOR3:def 5 for a being object of A holds it ! a is iso ; existence ex b1 being natural_transformation of F1,F2 st for a being object of A holds b1 ! a is iso by A1, Def4; end; :: deftheorem Def5 defines natural_equivalence FUNCTOR3:def_5_:_ for A, B being category for F1, F2 being covariant 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 for a being object of A holds b5 ! a is iso ); theorem Th33: :: FUNCTOR3:33 for A, B being category for F1, F2, F3 being covariant Functor of A,B st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds F1,F3 are_naturally_equivalent proof let A, B be category; ::_thesis: for F1, F2, F3 being covariant Functor of A,B st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds F1,F3 are_naturally_equivalent let F1, F2, F3 be covariant Functor of A,B; ::_thesis: ( F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent implies F1,F3 are_naturally_equivalent ) assume that A1: F1 is_naturally_transformable_to F2 and A2: F2 is_transformable_to F1 ; :: according to FUNCTOR3:def_4 ::_thesis: ( for t being natural_transformation of F1,F2 holds not for a being object of A holds t ! a is iso or not F2,F3 are_naturally_equivalent or F1,F3 are_naturally_equivalent ) given t being natural_transformation of F1,F2 such that A3: for a being object of A holds t ! a is iso ; ::_thesis: ( not F2,F3 are_naturally_equivalent or F1,F3 are_naturally_equivalent ) assume that A4: F2 is_naturally_transformable_to F3 and A5: F3 is_transformable_to F2 ; :: according to FUNCTOR3:def_4 ::_thesis: ( for t being natural_transformation of F2,F3 holds not for a being object of A holds t ! a is iso or F1,F3 are_naturally_equivalent ) given t1 being natural_transformation of F2,F3 such that A6: for a being object of A holds t1 ! a is iso ; ::_thesis: F1,F3 are_naturally_equivalent thus ( F1 is_naturally_transformable_to F3 & F3 is_transformable_to F1 ) by A1, A2, A4, A5, FUNCTOR2:2, FUNCTOR2:8; :: according to FUNCTOR3:def_4 ::_thesis: ex t being natural_transformation of F1,F3 st for a being object of A holds t ! a is iso take t1 `*` t ; ::_thesis: for a being object of A holds (t1 `*` t) ! a is iso let a be object of A; ::_thesis: (t1 `*` t) ! a is iso A7: t1 ! a is iso by A6; F3 is_transformable_to F1 by A2, A5, FUNCTOR2:2; then A8: <^(F3 . a),(F1 . a)^> <> {} by FUNCTOR2:def_1; A9: t ! a is iso by A3; A10: F2 is_transformable_to F3 by A4, FUNCTOR2:def_6; then A11: <^(F2 . a),(F3 . a)^> <> {} by FUNCTOR2:def_1; A12: F1 is_transformable_to F2 by A1, FUNCTOR2:def_6; then A13: <^(F1 . a),(F2 . a)^> <> {} by FUNCTOR2:def_1; (t1 `*` t) ! a = (t1 `*` t) ! a by A1, A4, FUNCTOR2:def_8 .= (t1 ! a) * (t ! a) by A12, A10, FUNCTOR2:def_5 ; hence (t1 `*` t) ! a is iso by A13, A11, A8, A7, A9, ALTCAT_3:7; ::_thesis: verum end; theorem Th34: :: FUNCTOR3:34 for A, B being category for F1, F2, F3 being covariant Functor of A,B for e being natural_equivalence of F1,F2 for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds e1 `*` e is natural_equivalence of F1,F3 proof let A, B be category; ::_thesis: for F1, F2, F3 being covariant Functor of A,B for e being natural_equivalence of F1,F2 for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds e1 `*` e is natural_equivalence of F1,F3 let F1, F2, F3 be covariant Functor of A,B; ::_thesis: for e being natural_equivalence of F1,F2 for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds e1 `*` e is natural_equivalence of F1,F3 let e be natural_equivalence of F1,F2; ::_thesis: for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds e1 `*` e is natural_equivalence of F1,F3 let e1 be natural_equivalence of F2,F3; ::_thesis: ( F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent implies e1 `*` e is natural_equivalence of F1,F3 ) assume that A1: F1,F2 are_naturally_equivalent and A2: F2,F3 are_naturally_equivalent ; ::_thesis: e1 `*` e is natural_equivalence of F1,F3 thus A3: F1,F3 are_naturally_equivalent by A1, A2, Th33; :: according to FUNCTOR3:def_5 ::_thesis: for a being object of A holds (e1 `*` e) ! a is iso let a be object of A; ::_thesis: (e1 `*` e) ! a is iso A4: F1 is_transformable_to F2 by A1, Def4; then A5: <^(F1 . a),(F2 . a)^> <> {} by FUNCTOR2:def_1; F3 is_transformable_to F1 by A3, Def4; then A6: <^(F3 . a),(F1 . a)^> <> {} by FUNCTOR2:def_1; A7: F2 is_transformable_to F3 by A2, Def4; then A8: <^(F2 . a),(F3 . a)^> <> {} by FUNCTOR2:def_1; ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 ) by A1, A2, Def4; then A9: (e1 `*` e) ! a = (e1 `*` e) ! a by FUNCTOR2:def_8 .= (e1 ! a) * (e ! a) by A4, A7, FUNCTOR2:def_5 ; ( e1 ! a is iso & e ! a is iso ) by A1, A2, Def5; hence (e1 `*` e) ! a is iso by A9, A5, A8, A6, ALTCAT_3:7; ::_thesis: verum end; theorem Th35: :: FUNCTOR3:35 for C, A, B being category for F1, F2 being covariant Functor of A,B for G1 being covariant Functor of B,C for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds ( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) proof let C, A, B be category; ::_thesis: for F1, F2 being covariant Functor of A,B for G1 being covariant Functor of B,C for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds ( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) let F1, F2 be covariant Functor of A,B; ::_thesis: for G1 being covariant Functor of B,C for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds ( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) let G1 be covariant Functor of B,C; ::_thesis: for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds ( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) let e be natural_equivalence of F1,F2; ::_thesis: ( F1,F2 are_naturally_equivalent implies ( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) ) assume A1: F1,F2 are_naturally_equivalent ; ::_thesis: ( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) then A2: F2 is_transformable_to F1 by Def4; A3: F1 is_naturally_transformable_to F2 by A1, Def4; then reconsider k = G1 * e as natural_transformation of G1 * F1,G1 * F2 by Th28; A4: F1 is_transformable_to F2 by A1, Def4; A5: now__::_thesis:_for_a_being_object_of_A_holds_k_!_a_is_iso let a be object of A; ::_thesis: k ! a is iso A6: ( (G1 * F1) . a = G1 . (F1 . a) & (G1 * F2) . a = G1 . (F2 . a) ) by FUNCTOR0:33; A7: <^(F2 . a),(F1 . a)^> <> {} by A2, FUNCTOR2:def_1; ( k ! a = G1 . (e ! a) & <^(F1 . a),(F2 . a)^> <> {} ) by A4, Th11, FUNCTOR2:def_1; hence k ! a is iso by A1, A6, A7, Def5, ALTCAT_4:20; ::_thesis: verum end; G1 * F1,G1 * F2 are_naturally_equivalent proof thus G1 * F1 is_naturally_transformable_to G1 * F2 by A3, Lm2; :: according to FUNCTOR3:def_4 ::_thesis: ( G1 * F2 is_transformable_to G1 * F1 & ex t being natural_transformation of G1 * F1,G1 * F2 st for a being object of A holds t ! a is iso ) thus G1 * F2 is_transformable_to G1 * F1 by A2, Th10; ::_thesis: ex t being natural_transformation of G1 * F1,G1 * F2 st for a being object of A holds t ! a is iso take k ; ::_thesis: for a being object of A holds k ! a is iso let a be object of A; ::_thesis: k ! a is iso thus k ! a is iso by A5; ::_thesis: verum end; hence ( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) by A5, Def5; ::_thesis: verum end; theorem Th36: :: FUNCTOR3:36 for A, B, C being category for F1 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 ) proof let A, B, C be category; ::_thesis: for F1 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 ) let F1 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 ) let G1, G2 be covariant Functor of B,C; ::_thesis: for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 ) let f be natural_equivalence of G1,G2; ::_thesis: ( G1,G2 are_naturally_equivalent implies ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 ) ) assume A1: G1,G2 are_naturally_equivalent ; ::_thesis: ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 ) then A2: G1 is_naturally_transformable_to G2 by Def4; then reconsider k = f * F1 as natural_transformation of G1 * F1,G2 * F1 by Th29; A3: now__::_thesis:_for_a_being_object_of_A_holds_k_!_a_is_iso let a be object of A; ::_thesis: k ! a is iso G1 is_transformable_to G2 by A1, Def4; then A4: k ! a = f ! (F1 . a) by Th12; ( (G1 * F1) . a = G1 . (F1 . a) & (G2 * F1) . a = G2 . (F1 . a) ) by FUNCTOR0:33; hence k ! a is iso by A1, A4, Def5; ::_thesis: verum end; G1 * F1,G2 * F1 are_naturally_equivalent proof thus G1 * F1 is_naturally_transformable_to G2 * F1 by A2, Lm2; :: according to FUNCTOR3:def_4 ::_thesis: ( G2 * F1 is_transformable_to G1 * F1 & ex t being natural_transformation of G1 * F1,G2 * F1 st for a being object of A holds t ! a is iso ) G2 is_transformable_to G1 by A1, Def4; hence G2 * F1 is_transformable_to G1 * F1 by Th10; ::_thesis: ex t being natural_transformation of G1 * F1,G2 * F1 st for a being object of A holds t ! a is iso take k ; ::_thesis: for a being object of A holds k ! a is iso let a be object of A; ::_thesis: k ! a is iso thus k ! a is iso by A3; ::_thesis: verum end; hence ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 ) by A3, Def5; ::_thesis: verum end; theorem :: FUNCTOR3:37 for A, B, C being category for F1, F2 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for e being natural_equivalence of F1,F2 for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) proof let A, B, C be category; ::_thesis: for F1, F2 being covariant Functor of A,B for G1, G2 being covariant Functor of B,C for e being natural_equivalence of F1,F2 for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) let F1, F2 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C for e being natural_equivalence of F1,F2 for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) let G1, G2 be covariant Functor of B,C; ::_thesis: for e being natural_equivalence of F1,F2 for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) let e be natural_equivalence of F1,F2; ::_thesis: for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) let f be natural_equivalence of G1,G2; ::_thesis: ( F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent implies ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) ) assume that A1: F1,F2 are_naturally_equivalent and A2: G1,G2 are_naturally_equivalent ; ::_thesis: ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) A3: G1 * F1,G1 * F2 are_naturally_equivalent by A1, Th35; then A4: G1 * F1 is_naturally_transformable_to G1 * F2 by Def4; G1 is_naturally_transformable_to G2 by A2, Def4; then reconsider sF2 = f * F2 as natural_transformation of G1 * F2,G2 * F2 by Th29; F1 is_naturally_transformable_to F2 by A1, Def4; then reconsider G1t = G1 * e as natural_transformation of G1 * F1,G1 * F2 by Th28; A5: G1 * F2,G2 * F2 are_naturally_equivalent by A2, Th36; then A6: G1 * F2 is_naturally_transformable_to G2 * F2 by Def4; ( f * F2 is natural_equivalence of G1 * F2,G2 * F2 & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) by A1, A2, Th35, Th36; then sF2 `*` G1t is natural_equivalence of G1 * F1,G2 * F2 by A5, A3, Th34; hence ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) by A5, A3, A6, A4, Th33, FUNCTOR2:def_8; ::_thesis: verum end; definition let A, B be category; let F1, F2 be covariant Functor of A,B; let e be natural_equivalence of F1,F2; assume B1: F1,F2 are_naturally_equivalent ; funce " -> natural_equivalence of F2,F1 means :Def6: :: FUNCTOR3:def 6 for a being object of A holds it . a = (e ! a) " ; existence ex b1 being natural_equivalence of F2,F1 st for a being object of A holds b1 . a = (e ! a) " proof A1: for a being object of A holds e ! a is iso by B1, Def5; ( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 ) by B1, Def4; then consider f being natural_transformation of F2,F1 such that A2: for a being object of A holds ( f . a = (e ! a) " & f ! a is iso ) by A1, Th32; f is natural_equivalence of F2,F1 proof thus F2,F1 are_naturally_equivalent by B1; :: according to FUNCTOR3:def_5 ::_thesis: for a being object of A holds f ! a is iso let a be object of A; ::_thesis: f ! a is iso thus f ! a is iso by A2; ::_thesis: verum end; then reconsider f = f as natural_equivalence of F2,F1 ; take f ; ::_thesis: for a being object of A holds f . a = (e ! a) " let a be object of A; ::_thesis: f . a = (e ! a) " thus f . a = (e ! a) " by A2; ::_thesis: verum end; uniqueness for b1, b2 being natural_equivalence of F2,F1 st ( for a being object of A holds b1 . a = (e ! a) " ) & ( for a being object of A holds b2 . a = (e ! a) " ) holds b1 = b2 proof let P, R be natural_equivalence of F2,F1; ::_thesis: ( ( for a being object of A holds P . a = (e ! a) " ) & ( for a being object of A holds R . a = (e ! a) " ) implies P = R ) assume that A3: for a being object of A holds P . a = (e ! a) " and A4: for a being object of A holds R . a = (e ! a) " ; ::_thesis: P = R A5: F2 is_transformable_to F1 by B1, Def4; now__::_thesis:_for_a_being_object_of_A_holds_P_!_a_=_R_!_a let a be object of A; ::_thesis: P ! a = R ! a thus P ! a = P . a by A5, FUNCTOR2:def_4 .= (e ! a) " by A3 .= R . a by A4 .= R ! a by A5, FUNCTOR2:def_4 ; ::_thesis: verum end; hence P = R by A5, FUNCTOR2:3; ::_thesis: verum end; end; :: deftheorem Def6 defines " FUNCTOR3:def_6_:_ for A, B being category for F1, F2 being covariant Functor of A,B for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds for b6 being natural_equivalence of F2,F1 holds ( b6 = e " iff for a being object of A holds b6 . a = (e ! a) " ); theorem Th38: :: FUNCTOR3:38 for B, A being category for F1, F2 being covariant Functor of A,B for e being natural_equivalence of F1,F2 for o being object of A st F1,F2 are_naturally_equivalent holds (e ") ! o = (e ! o) " proof let B, A be category; ::_thesis: for F1, F2 being covariant Functor of A,B for e being natural_equivalence of F1,F2 for o being object of A st F1,F2 are_naturally_equivalent holds (e ") ! o = (e ! o) " let F1, F2 be covariant Functor of A,B; ::_thesis: for e being natural_equivalence of F1,F2 for o being object of A st F1,F2 are_naturally_equivalent holds (e ") ! o = (e ! o) " let e be natural_equivalence of F1,F2; ::_thesis: for o being object of A st F1,F2 are_naturally_equivalent holds (e ") ! o = (e ! o) " let o be object of A; ::_thesis: ( F1,F2 are_naturally_equivalent implies (e ") ! o = (e ! o) " ) assume A1: F1,F2 are_naturally_equivalent ; ::_thesis: (e ") ! o = (e ! o) " then F2 is_transformable_to F1 by Def4; hence (e ") ! o = (e ") . o by FUNCTOR2:def_4 .= (e ! o) " by A1, Def6 ; ::_thesis: verum end; theorem Th39: :: FUNCTOR3:39 for A, B being category for F1, F2 being covariant Functor of A,B for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds e `*` (e ") = idt F2 proof let A, B be category; ::_thesis: for F1, F2 being covariant Functor of A,B for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds e `*` (e ") = idt F2 let F1, F2 be covariant Functor of A,B; ::_thesis: for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds e `*` (e ") = idt F2 let e be natural_equivalence of F1,F2; ::_thesis: ( F1,F2 are_naturally_equivalent implies e `*` (e ") = idt F2 ) assume A1: F1,F2 are_naturally_equivalent ; ::_thesis: e `*` (e ") = idt F2 then A2: ( F1 is_transformable_to F2 & F2 is_transformable_to F1 ) by Def4; A3: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F1 ) by A1, Def4; now__::_thesis:_for_a_being_object_of_A_holds_(e_`*`_(e_"))_!_a_=_(idt_F2)_!_a let a be object of A; ::_thesis: (e `*` (e ")) ! a = (idt F2) ! a A4: e ! a is iso by A1, Def5; thus (e `*` (e ")) ! a = (e `*` (e ")) ! a by A3, FUNCTOR2:def_8 .= (e ! a) * ((e ") ! a) by A2, FUNCTOR2:def_5 .= (e ! a) * ((e ! a) ") by A1, Th38 .= idm (F2 . a) by A4, ALTCAT_3:def_5 .= (idt F2) ! a by FUNCTOR2:4 ; ::_thesis: verum end; hence e `*` (e ") = idt F2 by FUNCTOR2:3; ::_thesis: verum end; theorem :: FUNCTOR3:40 for A, B being category for F1, F2 being covariant Functor of A,B for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds (e ") `*` e = idt F1 proof let A, B be category; ::_thesis: for F1, F2 being covariant Functor of A,B for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds (e ") `*` e = idt F1 let F1, F2 be covariant Functor of A,B; ::_thesis: for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds (e ") `*` e = idt F1 let e be natural_equivalence of F1,F2; ::_thesis: ( F1,F2 are_naturally_equivalent implies (e ") `*` e = idt F1 ) assume A1: F1,F2 are_naturally_equivalent ; ::_thesis: (e ") `*` e = idt F1 then A2: ( F1 is_transformable_to F2 & F2 is_transformable_to F1 ) by Def4; A3: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F1 ) by A1, Def4; now__::_thesis:_for_a_being_object_of_A_holds_((e_")_`*`_e)_!_a_=_(idt_F1)_!_a let a be object of A; ::_thesis: ((e ") `*` e) ! a = (idt F1) ! a A4: e ! a is iso by A1, Def5; thus ((e ") `*` e) ! a = ((e ") `*` e) ! a by A3, FUNCTOR2:def_8 .= ((e ") ! a) * (e ! a) by A2, FUNCTOR2:def_5 .= ((e ! a) ") * (e ! a) by A1, Th38 .= idm (F1 . a) by A4, ALTCAT_3:def_5 .= (idt F1) ! a by FUNCTOR2:4 ; ::_thesis: verum end; hence (e ") `*` e = idt F1 by FUNCTOR2:3; ::_thesis: verum end; definition let A, B be category; let F be covariant Functor of A,B; :: original: idt redefine func idt F -> natural_equivalence of F,F; coherence idt F is natural_equivalence of F,F proof set e = the natural_equivalence of F,F; the natural_equivalence of F,F `*` ( the natural_equivalence of F,F ") = idt F by Th39; hence idt F is natural_equivalence of F,F by Th34; ::_thesis: verum end; end; theorem :: FUNCTOR3:41 for A, B being category for F1, F2 being covariant Functor of A,B for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds (e ") " = e proof let A, B be category; ::_thesis: for F1, F2 being covariant Functor of A,B for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds (e ") " = e let F1, F2 be covariant Functor of A,B; ::_thesis: for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds (e ") " = e let e be natural_equivalence of F1,F2; ::_thesis: ( F1,F2 are_naturally_equivalent implies (e ") " = e ) assume A1: F1,F2 are_naturally_equivalent ; ::_thesis: (e ") " = e then A2: F1 is_transformable_to F2 by Def4; now__::_thesis:_for_a_being_object_of_A_holds_((e_")_")_!_a_=_e_!_a let a be object of A; ::_thesis: ((e ") ") ! a = e ! a A3: <^(F1 . a),(F2 . a)^> <> {} by A2, FUNCTOR2:def_1; F2 is_transformable_to F1 by A1, Def4; then A4: <^(F2 . a),(F1 . a)^> <> {} by FUNCTOR2:def_1; e ! a is iso by A1, Def5; then A5: ( e ! a is retraction & e ! a is coretraction ) by ALTCAT_3:5; thus ((e ") ") ! a = ((e ") ! a) " by A1, Th38 .= ((e ! a) ") " by A1, Th38 .= e ! a by A3, A4, A5, ALTCAT_3:3 ; ::_thesis: verum end; hence (e ") " = e by A2, FUNCTOR2:3; ::_thesis: verum end; theorem :: FUNCTOR3:42 for A, B being category for F1, F3, F2 being covariant Functor of A,B for e being natural_equivalence of F1,F2 for e1 being natural_equivalence of F2,F3 for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds k " = (e ") `*` (e1 ") proof let A, B be category; ::_thesis: for F1, F3, F2 being covariant Functor of A,B for e being natural_equivalence of F1,F2 for e1 being natural_equivalence of F2,F3 for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds k " = (e ") `*` (e1 ") let F1, F3, F2 be covariant Functor of A,B; ::_thesis: for e being natural_equivalence of F1,F2 for e1 being natural_equivalence of F2,F3 for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds k " = (e ") `*` (e1 ") let e be natural_equivalence of F1,F2; ::_thesis: for e1 being natural_equivalence of F2,F3 for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds k " = (e ") `*` (e1 ") let e1 be natural_equivalence of F2,F3; ::_thesis: for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds k " = (e ") `*` (e1 ") let k be natural_equivalence of F1,F3; ::_thesis: ( k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent implies k " = (e ") `*` (e1 ") ) assume that A1: k = e1 `*` e and A2: F1,F2 are_naturally_equivalent and A3: F2,F3 are_naturally_equivalent ; ::_thesis: k " = (e ") `*` (e1 ") A4: ( F3 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F1 ) by A2, A3, Def4; A5: ( F1 is_transformable_to F2 & F2 is_transformable_to F3 ) by A2, A3, Def4; A6: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 ) by A2, A3, Def4; A7: ( F3 is_transformable_to F2 & F2 is_transformable_to F1 ) by A2, A3, Def4; then A8: F3 is_transformable_to F1 by FUNCTOR2:2; now__::_thesis:_for_a_being_object_of_A_holds_(k_")_!_a_=_((e_")_`*`_(e1_"))_!_a let a be object of A; ::_thesis: (k ") ! a = ((e ") `*` (e1 ")) ! a A9: ( <^(F1 . a),(F2 . a)^> <> {} & <^(F2 . a),(F3 . a)^> <> {} ) by A5, FUNCTOR2:def_1; A10: <^(F3 . a),(F1 . a)^> <> {} by A8, FUNCTOR2:def_1; A11: ( e ! a is iso & e1 ! a is iso ) by A2, A3, Def5; thus (k ") ! a = ((e1 `*` e) ! a) " by A1, A2, A3, Th33, Th38 .= ((e1 `*` e) ! a) " by A6, FUNCTOR2:def_8 .= ((e1 ! a) * (e ! a)) " by A5, FUNCTOR2:def_5 .= ((e ! a) ") * ((e1 ! a) ") by A11, A9, A10, ALTCAT_3:7 .= ((e ! a) ") * ((e1 ") ! a) by A3, Th38 .= ((e ") ! a) * ((e1 ") ! a) by A2, Th38 .= ((e ") `*` (e1 ")) ! a by A7, FUNCTOR2:def_5 .= ((e ") `*` (e1 ")) ! a by A4, FUNCTOR2:def_8 ; ::_thesis: verum end; hence k " = (e ") `*` (e1 ") by A7, FUNCTOR2:2, FUNCTOR2:3; ::_thesis: verum end; theorem :: FUNCTOR3:43 for A, B being category for F1 being covariant Functor of A,B holds (idt F1) " = idt F1 proof let A, B be category; ::_thesis: for F1 being covariant Functor of A,B holds (idt F1) " = idt F1 let F1 be covariant Functor of A,B; ::_thesis: (idt F1) " = idt F1 now__::_thesis:_for_a_being_object_of_A_holds_((idt_F1)_")_!_a_=_(idt_F1)_!_a let a be object of A; ::_thesis: ((idt F1) ") ! a = (idt F1) ! a thus ((idt F1) ") ! a = ((idt F1) ! a) " by Th38 .= (idm (F1 . a)) " by FUNCTOR2:4 .= idm (F1 . a) by ALTCAT_3:4 .= (idt F1) ! a by FUNCTOR2:4 ; ::_thesis: verum end; hence (idt F1) " = idt F1 by FUNCTOR2:3; ::_thesis: verum end;