:: FUNCTOR0 semantic presentation begin scheme :: FUNCTOR0:sch 1 ValOnPair{ F1() -> non empty set , F2() -> Function, F3() -> Element of F1(), F4() -> Element of F1(), F5( set , set ) -> set , P1[ set , set ] } : F2() . (F3(),F4()) = F5(F3(),F4()) provided A1: F2() = { [[o,o9],F5(o,o9)] where o, o9 is Element of F1() : P1[o,o9] } and A2: P1[F3(),F4()] proof defpred S1[ set ] means P1[$1 `1 ,$1 `2 ]; deffunc H1( set ) -> set = F5(($1 `1),($1 `2)); A3: F2() = { [o,H1(o)] where o is Element of [:F1(),F1():] : S1[o] } proof thus F2() c= { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] } :: according to XBOOLE_0:def_10 ::_thesis: { [o,H1(o)] where o is Element of [:F1(),F1():] : S1[o] } c= F2() proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F2() or y in { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] } ) assume y in F2() ; ::_thesis: y in { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] } then consider o1, o2 being Element of F1() such that A4: y = [[o1,o2],F5(o1,o2)] and A5: P1[o1,o2] by A1; reconsider p = [o1,o2] as Element of [:F1(),F1():] by ZFMISC_1:87; A6: p `1 = o1 by MCART_1:7; p `2 = o2 by MCART_1:7; hence y in { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] } by A4, A5, A6; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { [o,H1(o)] where o is Element of [:F1(),F1():] : S1[o] } or y in F2() ) assume y in { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] } ; ::_thesis: y in F2() then consider o being Element of [:F1(),F1():] such that A7: y = [o,F5((o `1),(o `2))] and A8: P1[o `1 ,o `2 ] ; reconsider o1 = o `1 , o2 = o `2 as Element of F1() by MCART_1:10; o = [o1,o2] by MCART_1:21; hence y in F2() by A1, A7, A8; ::_thesis: verum end; reconsider x = [F3(),F4()] as Element of [:F1(),F1():] by ZFMISC_1:87; A9: x `1 = F3() by MCART_1:7; then A10: S1[x] by A2, MCART_1:7; thus F2() . (F3(),F4()) = F2() . x .= H1(x) from ALTCAT_2:sch_3(A3, A10) .= F5(F3(),F4()) by A9, MCART_1:7 ; ::_thesis: verum end; theorem Th1: :: FUNCTOR0:1 for A being set holds {} is Function of A,{} proof let A be set ; ::_thesis: {} is Function of A,{} percases ( A = {} or A <> {} ) ; suppose A = {} ; ::_thesis: {} is Function of A,{} hence {} is Function of A,{} by RELSET_1:12; ::_thesis: verum end; suppose A <> {} ; ::_thesis: {} is Function of A,{} thus {} is Function of A,{} by FUNCT_2:def_1, RELSET_1:12; ::_thesis: verum end; end; end; theorem Th2: :: FUNCTOR0:2 for I being set for M being ManySortedSet of I holds M * (id I) = M proof let I be set ; ::_thesis: for M being ManySortedSet of I holds M * (id I) = M let M be ManySortedSet of I; ::_thesis: M * (id I) = M I = dom M by PARTFUN1:def_2; hence M * (id I) = M by RELAT_1:52; ::_thesis: verum end; registration let f be empty Function; cluster ~ f -> empty ; coherence ~ f is empty proof rng f = {} ; then rng (~ f) = {} by FUNCT_4:41, XBOOLE_1:3; hence ~ f is empty ; ::_thesis: verum end; let g be Function; cluster[:f,g:] -> empty ; coherence [:f,g:] is empty proof dom f = {} ; then dom [:f,g:] = [:{},(dom g):] by FUNCT_3:def_8; hence [:f,g:] is empty by ZFMISC_1:90; ::_thesis: verum end; cluster[:g,f:] -> empty ; coherence [:g,f:] is empty proof dom f = {} ; then dom [:g,f:] = [:(dom g),{}:] by FUNCT_3:def_8; hence [:g,f:] is empty by ZFMISC_1:90; ::_thesis: verum end; end; theorem Th3: :: FUNCTOR0:3 for A being set for f being Function holds f .: (id A) = (~ f) .: (id A) proof let A be set ; ::_thesis: for f being Function holds f .: (id A) = (~ f) .: (id A) let f be Function; ::_thesis: f .: (id A) = (~ f) .: (id A) thus f .: (id A) c= (~ f) .: (id A) :: according to XBOOLE_0:def_10 ::_thesis: (~ f) .: (id A) c= f .: (id A) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (id A) or y in (~ f) .: (id A) ) assume y in f .: (id A) ; ::_thesis: y in (~ f) .: (id A) then consider x being set such that A1: x in dom f and A2: x in id A and A3: y = f . x by FUNCT_1:def_6; consider x1, x2 being set such that A4: x = [x1,x2] by A2, RELAT_1:def_1; A5: x1 = x2 by A2, A4, RELAT_1:def_10; then A6: x in dom (~ f) by A1, A4, FUNCT_4:42; then f . (x1,x2) = (~ f) . (x1,x2) by A4, A5, FUNCT_4:43; hence y in (~ f) .: (id A) by A2, A3, A4, A6, FUNCT_1:def_6; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (~ f) .: (id A) or y in f .: (id A) ) assume y in (~ f) .: (id A) ; ::_thesis: y in f .: (id A) then consider x being set such that A7: x in dom (~ f) and A8: x in id A and A9: y = (~ f) . x by FUNCT_1:def_6; consider x1, x2 being set such that A10: x = [x1,x2] by A8, RELAT_1:def_1; A11: x1 = x2 by A8, A10, RELAT_1:def_10; then A12: x in dom f by A7, A10, FUNCT_4:42; then (~ f) . (x1,x2) = f . (x1,x2) by A10, A11, FUNCT_4:def_2; hence y in f .: (id A) by A8, A9, A10, A12, FUNCT_1:def_6; ::_thesis: verum end; theorem Th4: :: FUNCTOR0:4 for X, Y being set for f being Function of X,Y holds ( f is onto iff [:f,f:] is onto ) proof let X, Y be set ; ::_thesis: for f being Function of X,Y holds ( f is onto iff [:f,f:] is onto ) let f be Function of X,Y; ::_thesis: ( f is onto iff [:f,f:] is onto ) rng [:f,f:] = [:(rng f),(rng f):] by FUNCT_3:67; then ( rng f = Y iff rng [:f,f:] = [:Y,Y:] ) by ZFMISC_1:92; hence ( f is onto iff [:f,f:] is onto ) by FUNCT_2:def_3; ::_thesis: verum end; registration let f be Function-yielding Function; cluster ~ f -> Function-yielding ; coherence ~ f is Function-yielding ; end; theorem Th5: :: FUNCTOR0:5 for A, B, a being set holds ~ ([:A,B:] --> a) = [:B,A:] --> a proof let A, B be set ; ::_thesis: for a being set holds ~ ([:A,B:] --> a) = [:B,A:] --> a let a be set ; ::_thesis: ~ ([:A,B:] --> a) = [:B,A:] --> a A1: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_([:B,A:]_-->_a)_implies_ex_y,_z_being_set_st_ (_x_=_[z,y]_&_[y,z]_in_dom_([:A,B:]_-->_a)_)_)_&_(_ex_y,_z_being_set_st_ (_x_=_[z,y]_&_[y,z]_in_dom_([:A,B:]_-->_a)_)_implies_x_in_dom_([:B,A:]_-->_a)_)_) let x be set ; ::_thesis: ( ( x in dom ([:B,A:] --> a) implies ex y, z being set st ( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) ) & ( ex y, z being set st ( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) implies x in dom ([:B,A:] --> a) ) ) hereby ::_thesis: ( ex y, z being set st ( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) implies x in dom ([:B,A:] --> a) ) assume x in dom ([:B,A:] --> a) ; ::_thesis: ex y, z being set st ( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) then consider z, y being set such that A2: z in B and A3: y in A and A4: x = [z,y] by ZFMISC_1:def_2; take y = y; ::_thesis: ex z being set st ( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) take z = z; ::_thesis: ( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) thus x = [z,y] by A4; ::_thesis: [y,z] in dom ([:A,B:] --> a) [y,z] in [:A,B:] by A2, A3, ZFMISC_1:87; hence [y,z] in dom ([:A,B:] --> a) by FUNCOP_1:13; ::_thesis: verum end; given y, z being set such that A5: x = [z,y] and A6: [y,z] in dom ([:A,B:] --> a) ; ::_thesis: x in dom ([:B,A:] --> a) A7: y in A by A6, ZFMISC_1:87; z in B by A6, ZFMISC_1:87; then x in [:B,A:] by A5, A7, ZFMISC_1:87; hence x in dom ([:B,A:] --> a) by FUNCOP_1:13; ::_thesis: verum end; now__::_thesis:_for_y,_z_being_set_st_[y,z]_in_dom_([:A,B:]_-->_a)_holds_ ([:B,A:]_-->_a)_._(z,y)_=_([:A,B:]_-->_a)_._(y,z) let y, z be set ; ::_thesis: ( [y,z] in dom ([:A,B:] --> a) implies ([:B,A:] --> a) . (z,y) = ([:A,B:] --> a) . (y,z) ) assume A8: [y,z] in dom ([:A,B:] --> a) ; ::_thesis: ([:B,A:] --> a) . (z,y) = ([:A,B:] --> a) . (y,z) then A9: y in A by ZFMISC_1:87; z in B by A8, ZFMISC_1:87; hence ([:B,A:] --> a) . (z,y) = a by A9, FUNCOP_1:7, ZFMISC_1:87 .= ([:A,B:] --> a) . (y,z) by A8, FUNCOP_1:7 ; ::_thesis: verum end; hence ~ ([:A,B:] --> a) = [:B,A:] --> a by A1, FUNCT_4:def_2; ::_thesis: verum end; theorem Th6: :: FUNCTOR0:6 for f, g being Function st f is one-to-one & g is one-to-one holds [:f,g:] " = [:(f "),(g "):] proof let f, g be Function; ::_thesis: ( f is one-to-one & g is one-to-one implies [:f,g:] " = [:(f "),(g "):] ) assume that A1: f is one-to-one and A2: g is one-to-one ; ::_thesis: [:f,g:] " = [:(f "),(g "):] A3: [:f,g:] is one-to-one by A1, A2; A4: dom (f ") = rng f by A1, FUNCT_1:33; A5: dom (g ") = rng g by A2, FUNCT_1:33; A6: dom ([:f,g:] ") = rng [:f,g:] by A3, FUNCT_1:33 .= [:(dom (f ")),(dom (g ")):] by A4, A5, FUNCT_3:67 ; for x, y being set st x in dom (f ") & y in dom (g ") holds ([:f,g:] ") . (x,y) = [((f ") . x),((g ") . y)] proof let x, y be set ; ::_thesis: ( x in dom (f ") & y in dom (g ") implies ([:f,g:] ") . (x,y) = [((f ") . x),((g ") . y)] ) assume that A7: x in dom (f ") and A8: y in dom (g ") ; ::_thesis: ([:f,g:] ") . (x,y) = [((f ") . x),((g ") . y)] A9: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def_8; A10: (f ") . x in rng (f ") by A7, FUNCT_1:def_3; A11: (g ") . y in rng (g ") by A8, FUNCT_1:def_3; A12: (f ") . x in dom f by A1, A10, FUNCT_1:33; (g ") . y in dom g by A2, A11, FUNCT_1:33; then A13: [((f ") . x),((g ") . y)] in dom [:f,g:] by A9, A12, ZFMISC_1:87; A14: f . ((f ") . x) = (f * (f ")) . x by A7, FUNCT_1:13 .= (((f ") ") * (f ")) . x by A1, FUNCT_1:43 .= (id (dom (f "))) . x by A1, FUNCT_1:39 .= x by A7, FUNCT_1:18 ; g . ((g ") . y) = (g * (g ")) . y by A8, FUNCT_1:13 .= (((g ") ") * (g ")) . y by A2, FUNCT_1:43 .= (id (dom (g "))) . y by A2, FUNCT_1:39 .= y by A8, FUNCT_1:18 ; then [:f,g:] . (((f ") . x),((g ") . y)) = [x,y] by A9, A13, A14, FUNCT_3:65; hence ([:f,g:] ") . (x,y) = [((f ") . x),((g ") . y)] by A1, A2, A13, FUNCT_1:32; ::_thesis: verum end; hence [:f,g:] " = [:(f "),(g "):] by A6, FUNCT_3:def_8; ::_thesis: verum end; theorem Th7: :: FUNCTOR0:7 for f being Function st [:f,f:] is one-to-one holds f is one-to-one proof let f be Function; ::_thesis: ( [:f,f:] is one-to-one implies f is one-to-one ) assume A1: [:f,f:] is one-to-one ; ::_thesis: f is one-to-one let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 ) assume that A2: x1 in dom f and A3: x2 in dom f and A4: f . x1 = f . x2 ; ::_thesis: x1 = x2 A5: dom [:f,f:] = [:(dom f),(dom f):] by FUNCT_3:def_8; then A6: [x1,x1] in dom [:f,f:] by A2, ZFMISC_1:87; A7: [x2,x2] in dom [:f,f:] by A3, A5, ZFMISC_1:87; [:f,f:] . (x1,x1) = [(f . x2),(f . x2)] by A4, A5, A6, FUNCT_3:65 .= [:f,f:] . (x2,x2) by A5, A7, FUNCT_3:65 ; then [x1,x1] = [x2,x2] by A1, A6, A7, FUNCT_1:def_4; hence x1 = x2 by XTUPLE_0:1; ::_thesis: verum end; theorem Th8: :: FUNCTOR0:8 for f being Function st f is one-to-one holds ~ f is one-to-one proof let f be Function; ::_thesis: ( f is one-to-one implies ~ f is one-to-one ) assume A1: f is one-to-one ; ::_thesis: ~ f is one-to-one let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 (~ f) or not x2 in proj1 (~ f) or not (~ f) . x1 = (~ f) . x2 or x1 = x2 ) consider X, Y being set such that A2: dom (~ f) c= [:X,Y:] by FUNCT_4:44; assume A3: x1 in dom (~ f) ; ::_thesis: ( not x2 in proj1 (~ f) or not (~ f) . x1 = (~ f) . x2 or x1 = x2 ) then consider x11, x12 being set such that x11 in X and x12 in Y and A4: x1 = [x11,x12] by A2, ZFMISC_1:84; assume A5: x2 in dom (~ f) ; ::_thesis: ( not (~ f) . x1 = (~ f) . x2 or x1 = x2 ) then consider x21, x22 being set such that x21 in X and x22 in Y and A6: x2 = [x21,x22] by A2, ZFMISC_1:84; assume A7: (~ f) . x1 = (~ f) . x2 ; ::_thesis: x1 = x2 A8: [x12,x11] in dom f by A3, A4, FUNCT_4:42; A9: [x22,x21] in dom f by A5, A6, FUNCT_4:42; f . (x12,x11) = (~ f) . (x11,x12) by A3, A4, FUNCT_4:43 .= (~ f) . (x21,x22) by A4, A6, A7 .= f . (x22,x21) by A5, A6, FUNCT_4:43 ; then A10: [x12,x11] = [x22,x21] by A1, A8, A9, FUNCT_1:def_4; then x12 = x22 by XTUPLE_0:1; hence x1 = x2 by A4, A6, A10, XTUPLE_0:1; ::_thesis: verum end; theorem Th9: :: FUNCTOR0:9 for f, g being Function st ~ [:f,g:] is one-to-one holds [:g,f:] is one-to-one proof let f, g be Function; ::_thesis: ( ~ [:f,g:] is one-to-one implies [:g,f:] is one-to-one ) assume A1: ~ [:f,g:] is one-to-one ; ::_thesis: [:g,f:] is one-to-one let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 [:g,f:] or not x2 in proj1 [:g,f:] or not [:g,f:] . x1 = [:g,f:] . x2 or x1 = x2 ) A2: dom [:g,f:] = [:(dom g),(dom f):] by FUNCT_3:def_8; A3: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def_8; assume x1 in dom [:g,f:] ; ::_thesis: ( not x2 in proj1 [:g,f:] or not [:g,f:] . x1 = [:g,f:] . x2 or x1 = x2 ) then consider x11, x12 being set such that A4: x11 in dom g and A5: x12 in dom f and A6: x1 = [x11,x12] by A2, ZFMISC_1:84; assume x2 in dom [:g,f:] ; ::_thesis: ( not [:g,f:] . x1 = [:g,f:] . x2 or x1 = x2 ) then consider x21, x22 being set such that A7: x21 in dom g and A8: x22 in dom f and A9: x2 = [x21,x22] by A2, ZFMISC_1:84; x1 in dom [:g,f:] by A2, A4, A5, A6, ZFMISC_1:87; then A10: x1 in dom (~ [:f,g:]) by A2, A3, FUNCT_4:46; x2 in dom [:g,f:] by A2, A7, A8, A9, ZFMISC_1:87; then A11: x2 in dom (~ [:f,g:]) by A2, A3, FUNCT_4:46; assume A12: [:g,f:] . x1 = [:g,f:] . x2 ; ::_thesis: x1 = x2 A13: [:g,f:] . (x11,x12) = [(g . x11),(f . x12)] by A4, A5, FUNCT_3:def_8; A14: [:g,f:] . (x21,x22) = [(g . x21),(f . x22)] by A7, A8, FUNCT_3:def_8; then A15: f . x22 = f . x12 by A6, A9, A12, A13, XTUPLE_0:1; A16: g . x11 = g . x21 by A6, A9, A12, A13, A14, XTUPLE_0:1; (~ [:f,g:]) . [x11,x12] = (~ [:f,g:]) . (x11,x12) .= [:f,g:] . (x12,x11) by A6, A10, FUNCT_4:43 .= [(f . x22),(g . x21)] by A4, A5, A15, A16, FUNCT_3:def_8 .= [:f,g:] . (x22,x21) by A7, A8, FUNCT_3:def_8 .= (~ [:f,g:]) . (x21,x22) by A9, A11, FUNCT_4:43 .= (~ [:f,g:]) . [x21,x22] ; hence x1 = x2 by A1, A6, A9, A10, A11, FUNCT_1:def_4; ::_thesis: verum end; theorem Th10: :: FUNCTOR0:10 for f, g being Function st f is one-to-one & g is one-to-one holds (~ [:f,g:]) " = ~ ([:g,f:] ") proof let f, g be Function; ::_thesis: ( f is one-to-one & g is one-to-one implies (~ [:f,g:]) " = ~ ([:g,f:] ") ) assume that A1: f is one-to-one and A2: g is one-to-one ; ::_thesis: (~ [:f,g:]) " = ~ ([:g,f:] ") A3: [:g,f:] " = [:(g "),(f "):] by A1, A2, Th6; then A4: dom ([:g,f:] ") = [:(dom (g ")),(dom (f ")):] by FUNCT_3:def_8; A5: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def_8; A6: dom [:g,f:] = [:(dom g),(dom f):] by FUNCT_3:def_8; A7: [:g,f:] is one-to-one by A1, A2; A8: ~ [:f,g:] is one-to-one by Th8, A1, A2; A9: [:f,g:] " = [:(f "),(g "):] by A1, A2, Th6; A10: dom (~ ([:g,f:] ")) = [:(dom (f ")),(dom (g ")):] by A4, FUNCT_4:46 .= dom [:(f "),(g "):] by FUNCT_3:def_8 .= rng [:f,g:] by A1, A2, A9, FUNCT_1:32 .= rng (~ [:f,g:]) by A5, FUNCT_4:47 ; now__::_thesis:_for_y,_x_being_set_holds_ (_(_y_in_rng_(~_[:f,g:])_&_x_=_(~_([:g,f:]_"))_._y_implies_(_x_in_dom_(~_[:f,g:])_&_(~_[:f,g:])_._x_=_y_)_)_&_(_x_in_dom_(~_[:f,g:])_&_(~_[:f,g:])_._x_=_y_implies_(_y_in_rng_(~_[:f,g:])_&_x_=_(~_([:g,f:]_"))_._y_)_)_) let y, x be set ; ::_thesis: ( ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y implies ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y ) ) & ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y implies ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y ) ) ) hereby ::_thesis: ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y implies ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y ) ) assume that A11: y in rng (~ [:f,g:]) and A12: x = (~ ([:g,f:] ")) . y ; ::_thesis: ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y ) y in rng [:f,g:] by A5, A11, FUNCT_4:47; then y in [:(rng f),(rng g):] by FUNCT_3:67; then consider y1, y2 being set such that A13: y1 in rng f and A14: y2 in rng g and A15: y = [y1,y2] by ZFMISC_1:84; set x1 = (f ") . y1; set x2 = (g ") . y2; A16: y2 in dom (g ") by A2, A14, FUNCT_1:32; A17: y1 in dom (f ") by A1, A13, FUNCT_1:32; then [y2,y1] in dom ([:g,f:] ") by A4, A16, ZFMISC_1:87; then A18: (~ ([:g,f:] ")) . (y1,y2) = [:(g "),(f "):] . (y2,y1) by A3, FUNCT_4:def_2 .= [((g ") . y2),((f ") . y1)] by A16, A17, FUNCT_3:def_8 ; A19: y1 in dom (f ") by A1, A13, FUNCT_1:32; A20: y2 in dom (g ") by A2, A14, FUNCT_1:32; A21: (f ") . y1 in rng (f ") by A19, FUNCT_1:def_3; A22: (g ") . y2 in rng (g ") by A20, FUNCT_1:def_3; A23: (f ") . y1 in dom f by A1, A21, FUNCT_1:33; A24: (g ") . y2 in dom g by A2, A22, FUNCT_1:33; then A25: [((g ") . y2),((f ") . y1)] in dom [:g,f:] by A6, A23, ZFMISC_1:87; then A26: [((g ") . y2),((f ") . y1)] in dom (~ [:f,g:]) by A5, A6, FUNCT_4:46; thus x in dom (~ [:f,g:]) by A5, A6, A12, A15, A18, A25, FUNCT_4:46; ::_thesis: (~ [:f,g:]) . x = y A27: f . ((f ") . y1) = y1 by A1, A13, FUNCT_1:32; A28: g . ((g ") . y2) = y2 by A2, A14, FUNCT_1:32; thus (~ [:f,g:]) . x = (~ [:f,g:]) . (((g ") . y2),((f ") . y1)) by A12, A15, A18 .= [:f,g:] . (((f ") . y1),((g ") . y2)) by A26, FUNCT_4:43 .= y by A15, A23, A24, A27, A28, FUNCT_3:def_8 ; ::_thesis: verum end; assume that A29: x in dom (~ [:f,g:]) and A30: (~ [:f,g:]) . x = y ; ::_thesis: ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y ) thus y in rng (~ [:f,g:]) by A29, A30, FUNCT_1:def_3; ::_thesis: x = (~ ([:g,f:] ")) . y x in dom [:g,f:] by A5, A6, A29, FUNCT_4:46; then consider x1, x2 being set such that A31: x1 in dom g and A32: x2 in dom f and A33: x = [x1,x2] by A6, ZFMISC_1:84; A34: (~ [:f,g:]) . (x1,x2) = [:f,g:] . (x2,x1) by A29, A33, FUNCT_4:43 .= [(f . x2),(g . x1)] by A31, A32, FUNCT_3:def_8 ; A35: g . x1 in rng g by A31, FUNCT_1:def_3; f . x2 in rng f by A32, FUNCT_1:def_3; then [(g . x1),(f . x2)] in [:(rng g),(rng f):] by A35, ZFMISC_1:87; then [(g . x1),(f . x2)] in rng [:g,f:] by FUNCT_3:67; then A36: [(g . x1),(f . x2)] in dom ([:g,f:] ") by A7, FUNCT_1:33; [x1,x2] in dom [:g,f:] by A6, A31, A32, ZFMISC_1:87; hence x = ([:g,f:] ") . ([:g,f:] . (x1,x2)) by A1, A2, A33, FUNCT_1:34 .= ([:g,f:] ") . ((g . x1),(f . x2)) by A31, A32, FUNCT_3:def_8 .= (~ ([:g,f:] ")) . ((f . x2),(g . x1)) by A36, FUNCT_4:def_2 .= (~ ([:g,f:] ")) . y by A30, A33, A34 ; ::_thesis: verum end; hence (~ [:f,g:]) " = ~ ([:g,f:] ") by A8, A10, FUNCT_1:32; ::_thesis: verum end; theorem Th11: :: FUNCTOR0:11 for A, B being set for f being Function of A,B st f is onto holds id B c= [:f,f:] .: (id A) proof let A, B be set ; ::_thesis: for f being Function of A,B st f is onto holds id B c= [:f,f:] .: (id A) let f be Function of A,B; ::_thesis: ( f is onto implies id B c= [:f,f:] .: (id A) ) assume f is onto ; ::_thesis: id B c= [:f,f:] .: (id A) then A1: rng f = B by FUNCT_2:def_3; let xx be set ; :: according to TARSKI:def_3 ::_thesis: ( not xx in id B or xx in [:f,f:] .: (id A) ) assume A2: xx in id B ; ::_thesis: xx in [:f,f:] .: (id A) then consider x, x9 being set such that A3: xx = [x,x9] by RELAT_1:def_1; A4: x = x9 by A2, A3, RELAT_1:def_10; A5: x in B by A2, A3, RELAT_1:def_10; then consider y being set such that A6: y in A and A7: f . y = x by A1, FUNCT_2:11; A8: dom f = A by A5, FUNCT_2:def_1; A9: [y,y] in id A by A6, RELAT_1:def_10; [:f,f:] . (y,y) = xx by A3, A4, A6, A7, A8, FUNCT_3:def_8; hence xx in [:f,f:] .: (id A) by A2, A9, FUNCT_2:35; ::_thesis: verum end; theorem Th12: :: FUNCTOR0:12 for F, G being Function-yielding Function for f being Function holds (G ** F) * f = (G * f) ** (F * f) proof let F, G be Function-yielding Function; ::_thesis: for f being Function holds (G ** F) * f = (G * f) ** (F * f) let f be Function; ::_thesis: (G ** F) * f = (G * f) ** (F * f) A1: dom ((G ** F) * f) = f " (dom (G ** F)) by RELAT_1:147 .= f " ((dom G) /\ (dom F)) by PBOOLE:def_19 .= (f " (dom F)) /\ (f " (dom G)) by FUNCT_1:68 .= (f " (dom F)) /\ (dom (G * f)) by RELAT_1:147 .= (dom (F * f)) /\ (dom (G * f)) by RELAT_1:147 ; now__::_thesis:_for_i_being_set_st_i_in_dom_((G_**_F)_*_f)_holds_ ((G_**_F)_*_f)_._i_=_((G_*_f)_._i)_*_((F_*_f)_._i) let i be set ; ::_thesis: ( i in dom ((G ** F) * f) implies ((G ** F) * f) . i = ((G * f) . i) * ((F * f) . i) ) assume A2: i in dom ((G ** F) * f) ; ::_thesis: ((G ** F) * f) . i = ((G * f) . i) * ((F * f) . i) then A3: i in dom f by FUNCT_1:11; A4: f . i in dom (G ** F) by A2, FUNCT_1:11; thus ((G ** F) * f) . i = (G ** F) . (f . i) by A2, FUNCT_1:12 .= (G . (f . i)) * (F . (f . i)) by A4, PBOOLE:def_19 .= ((G * f) . i) * (F . (f . i)) by A3, FUNCT_1:13 .= ((G * f) . i) * ((F * f) . i) by A3, FUNCT_1:13 ; ::_thesis: verum end; hence (G ** F) * f = (G * f) ** (F * f) by A1, PBOOLE:def_19; ::_thesis: verum end; definition let A, B, C be set ; let f be Function of [:A,B:],C; :: original: ~ redefine func ~ f -> Function of [:B,A:],C; coherence ~ f is Function of [:B,A:],C proof percases ( C = {} or C <> {} ) ; supposeA1: C = {} ; ::_thesis: ~ f is Function of [:B,A:],C then reconsider f = f as empty set ; ~ f = {} ; hence ~ f is Function of [:B,A:],C by A1, Th1; ::_thesis: verum end; suppose C <> {} ; ::_thesis: ~ f is Function of [:B,A:],C hence ~ f is Function of [:B,A:],C by FUNCT_4:49; ::_thesis: verum end; end; end; end; theorem Th13: :: FUNCTOR0:13 for A, B, C being set for f being Function of [:A,B:],C st ~ f is onto holds f is onto proof let A, B, C be set ; ::_thesis: for f being Function of [:A,B:],C st ~ f is onto holds f is onto let f be Function of [:A,B:],C; ::_thesis: ( ~ f is onto implies f is onto ) A1: rng (~ f) c= rng f by FUNCT_4:41; assume ~ f is onto ; ::_thesis: f is onto then rng (~ f) = C by FUNCT_2:def_3; hence rng f = C by A1, XBOOLE_0:def_10; :: according to FUNCT_2:def_3 ::_thesis: verum end; theorem Th14: :: FUNCTOR0:14 for A being set for B being non empty set for f being Function of A,B holds [:f,f:] .: (id A) c= id B proof let A be set ; ::_thesis: for B being non empty set for f being Function of A,B holds [:f,f:] .: (id A) c= id B let B be non empty set ; ::_thesis: for f being Function of A,B holds [:f,f:] .: (id A) c= id B let f be Function of A,B; ::_thesis: [:f,f:] .: (id A) c= id B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:f,f:] .: (id A) or x in id B ) assume x in [:f,f:] .: (id A) ; ::_thesis: x in id B then consider yy being set such that A1: yy in [:A,A:] and A2: yy in id A and A3: [:f,f:] . yy = x by FUNCT_2:64; consider y, y9 being set such that A4: y in A and y9 in A and A5: yy = [y,y9] by A1, ZFMISC_1:84; A6: y = y9 by A2, A5, RELAT_1:def_10; reconsider y = y as Element of A by A4; A7: f . y in B by A4, FUNCT_2:5; A8: y in dom f by A4, FUNCT_2:def_1; x = [:f,f:] . (y,y9) by A3, A5 .= [(f . y),(f . y)] by A6, A8, FUNCT_3:def_8 ; hence x in id B by A7, RELAT_1:def_10; ::_thesis: verum end; begin definition let A, B be set ; mode bifunction of A,B is Function of [:A,A:],[:B,B:]; end; definition let A, B be set ; let f be bifunction of A,B; attrf is Covariant means :Def1: :: FUNCTOR0:def 1 ex g being Function of A,B st f = [:g,g:]; attrf is Contravariant means :Def2: :: FUNCTOR0:def 2 ex g being Function of A,B st f = ~ [:g,g:]; end; :: deftheorem Def1 defines Covariant FUNCTOR0:def_1_:_ for A, B being set for f being bifunction of A,B holds ( f is Covariant iff ex g being Function of A,B st f = [:g,g:] ); :: deftheorem Def2 defines Contravariant FUNCTOR0:def_2_:_ for A, B being set for f being bifunction of A,B holds ( f is Contravariant iff ex g being Function of A,B st f = ~ [:g,g:] ); theorem Th15: :: FUNCTOR0:15 for A being set for B being non empty set for b being Element of B for f being bifunction of A,B st f = [:A,A:] --> [b,b] holds ( f is Covariant & f is Contravariant ) proof let A be set ; ::_thesis: for B being non empty set for b being Element of B for f being bifunction of A,B st f = [:A,A:] --> [b,b] holds ( f is Covariant & f is Contravariant ) let B be non empty set ; ::_thesis: for b being Element of B for f being bifunction of A,B st f = [:A,A:] --> [b,b] holds ( f is Covariant & f is Contravariant ) let b be Element of B; ::_thesis: for f being bifunction of A,B st f = [:A,A:] --> [b,b] holds ( f is Covariant & f is Contravariant ) let f be bifunction of A,B; ::_thesis: ( f = [:A,A:] --> [b,b] implies ( f is Covariant & f is Contravariant ) ) assume A1: f = [:A,A:] --> [b,b] ; ::_thesis: ( f is Covariant & f is Contravariant ) reconsider g = A --> b as Function of A,B ; thus f is Covariant ::_thesis: f is Contravariant proof take g ; :: according to FUNCTOR0:def_1 ::_thesis: f = [:g,g:] thus f = [:g,g:] by A1, ALTCAT_2:1; ::_thesis: verum end; take g ; :: according to FUNCTOR0:def_2 ::_thesis: f = ~ [:g,g:] [:A,A:] --> [b,b] = ~ ([:A,A:] --> [b,b]) by Th5; hence f = ~ [:g,g:] by A1, ALTCAT_2:1; ::_thesis: verum end; registration let A, B be set ; cluster Relation-like [:A,A:] -defined [:B,B:] -valued Function-like quasi_total Covariant Contravariant for Element of bool [:[:A,A:],[:B,B:]:]; existence ex b1 being bifunction of A,B st ( b1 is Covariant & b1 is Contravariant ) proof percases ( B = {} or B <> {} ) ; supposeA1: B = {} ; ::_thesis: ex b1 being bifunction of A,B st ( b1 is Covariant & b1 is Contravariant ) then [:B,B:] = {} by ZFMISC_1:90; then reconsider f = {} as bifunction of A,B by Th1; take f ; ::_thesis: ( f is Covariant & f is Contravariant ) reconsider g = {} as Function of A,B by A1, Th1; reconsider h = g as empty Function ; thus f is Covariant ::_thesis: f is Contravariant proof take g ; :: according to FUNCTOR0:def_1 ::_thesis: f = [:g,g:] thus f = [:h,h:] .= [:g,g:] ; ::_thesis: verum end; take g ; :: according to FUNCTOR0:def_2 ::_thesis: f = ~ [:g,g:] thus f = ~ [:h,h:] .= ~ [:g,g:] ; ::_thesis: verum end; supposeA2: B <> {} ; ::_thesis: ex b1 being bifunction of A,B st ( b1 is Covariant & b1 is Contravariant ) set b = the Element of B; set f = [:A,A:] --> [ the Element of B, the Element of B]; [ the Element of B, the Element of B] in [:B,B:] by A2, ZFMISC_1:87; then reconsider f = [:A,A:] --> [ the Element of B, the Element of B] as bifunction of A,B by FUNCOP_1:45; take f ; ::_thesis: ( f is Covariant & f is Contravariant ) thus ( f is Covariant & f is Contravariant ) by A2, Th15; ::_thesis: verum end; end; end; end; theorem :: FUNCTOR0:16 for A, B being non empty set for f being Covariant Contravariant bifunction of A,B ex b being Element of B st f = [:A,A:] --> [b,b] proof let A, B be non empty set ; ::_thesis: for f being Covariant Contravariant bifunction of A,B ex b being Element of B st f = [:A,A:] --> [b,b] let f be Covariant Contravariant bifunction of A,B; ::_thesis: ex b being Element of B st f = [:A,A:] --> [b,b] consider g1 being Function of A,B such that A1: f = [:g1,g1:] by Def1; consider g2 being Function of A,B such that A2: f = ~ [:g2,g2:] by Def2; set a = the Element of A; take b = g1 . the Element of A; ::_thesis: f = [:A,A:] --> [b,b] A3: dom f = [:A,A:] by FUNCT_2:def_1; now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_ f_._z_=_[b,b] let z be set ; ::_thesis: ( z in dom f implies f . z = [b,b] ) assume z in dom f ; ::_thesis: f . z = [b,b] then consider a1, a2 being Element of A such that A4: z = [a1,a2] by DOMAIN_1:1; A5: dom g2 = A by FUNCT_2:def_1; A6: dom g1 = A by FUNCT_2:def_1; A7: dom [:g2,g2:] = [:(dom g2),(dom g2):] by FUNCT_3:def_8; then A8: [a1, the Element of A] in dom [:g2,g2:] by A5, ZFMISC_1:87; A9: dom g2 = A by FUNCT_2:def_1; [b,(g1 . a1)] = f . ( the Element of A,a1) by A1, A6, FUNCT_3:def_8 .= [:g2,g2:] . (a1, the Element of A) by A2, A8, FUNCT_4:def_2 .= [(g2 . a1),(g2 . the Element of A)] by A9, FUNCT_3:def_8 ; then A10: g2 . a1 = b by XTUPLE_0:1; A11: [a2, the Element of A] in dom [:g2,g2:] by A5, A7, ZFMISC_1:87; [b,(g1 . a2)] = f . ( the Element of A,a2) by A1, A6, FUNCT_3:def_8 .= [:g2,g2:] . (a2, the Element of A) by A2, A11, FUNCT_4:def_2 .= [(g2 . a2),(g2 . the Element of A)] by A9, FUNCT_3:def_8 ; then A12: g2 . a2 = b by XTUPLE_0:1; A13: [a2,a1] in dom [:g2,g2:] by A5, A7, ZFMISC_1:87; thus f . z = [:g1,g1:] . (a1,a2) by A1, A4 .= [:g2,g2:] . (a2,a1) by A1, A2, A13, FUNCT_4:def_2 .= [b,b] by A9, A10, A12, FUNCT_3:def_8 ; ::_thesis: verum end; hence f = [:A,A:] --> [b,b] by A3, FUNCOP_1:11; ::_thesis: verum end; begin definition let I1, I2 be set ; let f be Function of I1,I2; let A be ManySortedSet of I1; let B be ManySortedSet of I2; mode MSUnTrans of f,A,B -> ManySortedSet of I1 means :Def3: :: FUNCTOR0:def 3 ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st ( f = f9 & B = B9 & it is ManySortedFunction of A,B9 * f9 ) if I2 <> {} otherwise it = [[0]] I1; existence ( ( I2 <> {} implies ex b1 being ManySortedSet of I1 ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st ( f = f9 & B = B9 & b1 is ManySortedFunction of A,B9 * f9 ) ) & ( not I2 <> {} implies ex b1 being ManySortedSet of I1 st b1 = [[0]] I1 ) ) proof hereby ::_thesis: ( not I2 <> {} implies ex b1 being ManySortedSet of I1 st b1 = [[0]] I1 ) assume I2 <> {} ; ::_thesis: ex IT9 being ManySortedSet of I1 ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st ( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 ) then reconsider I29 = I2 as non empty set ; reconsider f9 = f as Function of I1,I29 ; reconsider B9 = B as ManySortedSet of I29 ; set IT = the ManySortedFunction of A,B9 * f9; reconsider IT9 = the ManySortedFunction of A,B9 * f9 as ManySortedSet of I1 ; take IT9 = IT9; ::_thesis: ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st ( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 ) take I29 = I29; ::_thesis: ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st ( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 ) reconsider f9 = f as Function of I1,I29 ; reconsider B9 = B as ManySortedSet of I29 ; take B9 = B9; ::_thesis: ex f9 being Function of I1,I29 st ( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 ) take f9 = f9; ::_thesis: ( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 ) thus ( f = f9 & B = B9 ) ; ::_thesis: IT9 is ManySortedFunction of A,B9 * f9 thus IT9 is ManySortedFunction of A,B9 * f9 ; ::_thesis: verum end; thus ( not I2 <> {} implies ex b1 being ManySortedSet of I1 st b1 = [[0]] I1 ) ; ::_thesis: verum end; consistency for b1 being ManySortedSet of I1 holds verum ; end; :: deftheorem Def3 defines MSUnTrans FUNCTOR0:def_3_:_ for I1, I2 being set for f being Function of I1,I2 for A being ManySortedSet of I1 for B being ManySortedSet of I2 for b6 being ManySortedSet of I1 holds ( ( I2 <> {} implies ( b6 is MSUnTrans of f,A,B iff ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st ( f = f9 & B = B9 & b6 is ManySortedFunction of A,B9 * f9 ) ) ) & ( not I2 <> {} implies ( b6 is MSUnTrans of f,A,B iff b6 = [[0]] I1 ) ) ); definition let I1 be set ; let I2 be non empty set ; let f be Function of I1,I2; let A be ManySortedSet of I1; let B be ManySortedSet of I2; redefine mode MSUnTrans of f,A,B means :Def4: :: FUNCTOR0:def 4 it is ManySortedFunction of A,B * f; compatibility for b1 being ManySortedSet of I1 holds ( b1 is MSUnTrans of f,A,B iff b1 is ManySortedFunction of A,B * f ) proof let M be ManySortedSet of I1; ::_thesis: ( M is MSUnTrans of f,A,B iff M is ManySortedFunction of A,B * f ) hereby ::_thesis: ( M is ManySortedFunction of A,B * f implies M is MSUnTrans of f,A,B ) assume M is MSUnTrans of f,A,B ; ::_thesis: M is ManySortedFunction of A,B * f then ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st ( f = f9 & B = B9 & M is ManySortedFunction of A,B9 * f9 ) by Def3; hence M is ManySortedFunction of A,B * f ; ::_thesis: verum end; thus ( M is ManySortedFunction of A,B * f implies M is MSUnTrans of f,A,B ) by Def3; ::_thesis: verum end; end; :: deftheorem Def4 defines MSUnTrans FUNCTOR0:def_4_:_ 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 b6 being ManySortedSet of I1 holds ( b6 is MSUnTrans of f,A,B iff b6 is ManySortedFunction of A,B * f ); registration let I1, I2 be set ; let f be Function of I1,I2; let A be ManySortedSet of I1; let B be ManySortedSet of I2; cluster -> Function-yielding for MSUnTrans of f,A,B; coherence for b1 being MSUnTrans of f,A,B holds b1 is Function-yielding proof let M be MSUnTrans of f,A,B; ::_thesis: M is Function-yielding percases ( I2 <> {} or I2 = {} ) ; suppose I2 <> {} ; ::_thesis: M is Function-yielding then ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st ( f = f9 & B = B9 & M is ManySortedFunction of A,B9 * f9 ) by Def3; hence M is Function-yielding ; ::_thesis: verum end; suppose I2 = {} ; ::_thesis: M is Function-yielding then M = [[0]] I1 by Def3; hence M is Function-yielding ; ::_thesis: verum end; end; end; end; theorem Th17: :: FUNCTOR0:17 for I1 being set for I2, I3 being non empty set for f being Function of I1,I2 for g being Function of I2,I3 for B being ManySortedSet of I2 for C being ManySortedSet of I3 for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C proof let I1 be set ; ::_thesis: for I2, I3 being non empty set for f being Function of I1,I2 for g being Function of I2,I3 for B being ManySortedSet of I2 for C being ManySortedSet of I3 for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C let I2, I3 be non empty set ; ::_thesis: for f being Function of I1,I2 for g being Function of I2,I3 for B being ManySortedSet of I2 for C being ManySortedSet of I3 for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C let f be Function of I1,I2; ::_thesis: for g being Function of I2,I3 for B being ManySortedSet of I2 for C being ManySortedSet of I3 for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C let g be Function of I2,I3; ::_thesis: for B being ManySortedSet of I2 for C being ManySortedSet of I3 for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C let B be ManySortedSet of I2; ::_thesis: for C being ManySortedSet of I3 for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C let C be ManySortedSet of I3; ::_thesis: for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C let G be MSUnTrans of g,B,C; ::_thesis: G * f is MSUnTrans of g * f,B * f,C A1: C * (g * f) = (C * g) * f by RELAT_1:36; G is ManySortedFunction of B,C * g by Def4; hence G * f is ManySortedFunction of B * f,C * (g * f) by A1, ALTCAT_2:5; :: according to FUNCTOR0:def_4 ::_thesis: verum end; definition let I1 be set ; let I2 be non empty set ; let f be Function of I1,I2; let A be ManySortedSet of [:I1,I1:]; let B be ManySortedSet of [:I2,I2:]; let F be MSUnTrans of [:f,f:],A,B; :: original: ~ redefine func ~ F -> MSUnTrans of [:f,f:], ~ A, ~ B; coherence ~ F is MSUnTrans of [:f,f:], ~ A, ~ B proof reconsider G = F as ManySortedFunction of A,B * [:f,f:] by Def4; ~ G is ManySortedFunction of ~ A,(~ B) * [:f,f:] by ALTCAT_2:3; hence ~ F is MSUnTrans of [:f,f:], ~ A, ~ B by Def4; ::_thesis: verum end; end; theorem Th18: :: FUNCTOR0:18 for I1, I2 being non empty set for A being ManySortedSet of I1 for B being ManySortedSet of I2 for o being Element of I2 st B . o <> {} holds for m being Element of B . o for f being Function of I1,I2 st f = I1 --> o holds { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B proof let I1, I2 be non empty set ; ::_thesis: for A being ManySortedSet of I1 for B being ManySortedSet of I2 for o being Element of I2 st B . o <> {} holds for m being Element of B . o for f being Function of I1,I2 st f = I1 --> o holds { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B let A be ManySortedSet of I1; ::_thesis: for B being ManySortedSet of I2 for o being Element of I2 st B . o <> {} holds for m being Element of B . o for f being Function of I1,I2 st f = I1 --> o holds { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B let B be ManySortedSet of I2; ::_thesis: for o being Element of I2 st B . o <> {} holds for m being Element of B . o for f being Function of I1,I2 st f = I1 --> o holds { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B let o be Element of I2; ::_thesis: ( B . o <> {} implies for m being Element of B . o for f being Function of I1,I2 st f = I1 --> o holds { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B ) assume A1: B . o <> {} ; ::_thesis: for m being Element of B . o for f being Function of I1,I2 st f = I1 --> o holds { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B let m be Element of B . o; ::_thesis: for f being Function of I1,I2 st f = I1 --> o holds { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B let f be Function of I1,I2; ::_thesis: ( f = I1 --> o implies { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B ) assume A2: f = I1 --> o ; ::_thesis: { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B defpred S1[ set ] means verum; deffunc H1( set ) -> Element of bool [:(A . $1),{m}:] = (A . $1) --> m; reconsider Xm = { [o9,H1(o9)] where o9 is Element of I1 : S1[o9] } as Function from ALTCAT_2:sch_1(); A3: Xm = { [o9,H1(o9)] where o9 is Element of I1 : S1[o9] } ; dom Xm = { o9 where o9 is Element of I1 : S1[o9] } from ALTCAT_2:sch_2(A3) .= I1 by DOMAIN_1:18 ; then reconsider Xm = Xm as ManySortedSet of I1 by PARTFUN1:def_2, RELAT_1:def_18; deffunc H2( set ) -> Element of bool [:(A . $1),{m}:] = (A . $1) --> m; A4: Xm = { [o9,H2(o9)] where o9 is Element of I1 : S1[o9] } ; now__::_thesis:_for_i_being_set_st_i_in_I1_holds_ Xm_._i_is_Function_of_(A_._i),((B_*_f)_._i) let i be set ; ::_thesis: ( i in I1 implies Xm . i is Function of (A . i),((B * f) . i) ) assume A5: i in I1 ; ::_thesis: Xm . i is Function of (A . i),((B * f) . i) then reconsider o9 = i as Element of I1 ; A6: S1[o9] ; A7: i in dom f by A2, A5, FUNCOP_1:13; f . i = o by A2, A5, FUNCOP_1:7; then m in B . (f . i) by A1; then A8: m in (B * f) . i by A7, FUNCT_1:13; Xm . o9 = H2(o9) from ALTCAT_2:sch_3(A4, A6); hence Xm . i is Function of (A . i),((B * f) . i) by A8, FUNCOP_1:45; ::_thesis: verum end; then Xm is ManySortedFunction of A,B * f by PBOOLE:def_15; hence { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B by Def4; ::_thesis: verum end; theorem Th19: :: FUNCTOR0:19 for I1 being set for I2, I3 being non empty set for f being Function of I1,I2 for g being Function of I2,I3 for A being ManySortedSet of I1 for B being ManySortedSet of I2 for C being ManySortedSet of I3 for F being MSUnTrans of f,A,B for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds (C * (g * f)) . ii = {} ) holds G ** F is MSUnTrans of g * f,A,C proof let I1 be set ; ::_thesis: for I2, I3 being non empty set for f being Function of I1,I2 for g being Function of I2,I3 for A being ManySortedSet of I1 for B being ManySortedSet of I2 for C being ManySortedSet of I3 for F being MSUnTrans of f,A,B for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds (C * (g * f)) . ii = {} ) holds G ** F is MSUnTrans of g * f,A,C let I2, I3 be non empty set ; ::_thesis: for f being Function of I1,I2 for g being Function of I2,I3 for A being ManySortedSet of I1 for B being ManySortedSet of I2 for C being ManySortedSet of I3 for F being MSUnTrans of f,A,B for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds (C * (g * f)) . ii = {} ) holds G ** F is MSUnTrans of g * f,A,C let f be Function of I1,I2; ::_thesis: for g being Function of I2,I3 for A being ManySortedSet of I1 for B being ManySortedSet of I2 for C being ManySortedSet of I3 for F being MSUnTrans of f,A,B for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds (C * (g * f)) . ii = {} ) holds G ** F is MSUnTrans of g * f,A,C let g be Function of I2,I3; ::_thesis: for A being ManySortedSet of I1 for B being ManySortedSet of I2 for C being ManySortedSet of I3 for F being MSUnTrans of f,A,B for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds (C * (g * f)) . ii = {} ) holds G ** F is MSUnTrans of g * f,A,C let A be ManySortedSet of I1; ::_thesis: for B being ManySortedSet of I2 for C being ManySortedSet of I3 for F being MSUnTrans of f,A,B for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds (C * (g * f)) . ii = {} ) holds G ** F is MSUnTrans of g * f,A,C let B be ManySortedSet of I2; ::_thesis: for C being ManySortedSet of I3 for F being MSUnTrans of f,A,B for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds (C * (g * f)) . ii = {} ) holds G ** F is MSUnTrans of g * f,A,C let C be ManySortedSet of I3; ::_thesis: for F being MSUnTrans of f,A,B for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds (C * (g * f)) . ii = {} ) holds G ** F is MSUnTrans of g * f,A,C let F be MSUnTrans of f,A,B; ::_thesis: for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds (C * (g * f)) . ii = {} ) holds G ** F is MSUnTrans of g * f,A,C let G be MSUnTrans of g * f,B * f,C; ::_thesis: ( ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds (C * (g * f)) . ii = {} ) implies G ** F is MSUnTrans of g * f,A,C ) assume A1: for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds (C * (g * f)) . ii = {} ; ::_thesis: G ** F is MSUnTrans of g * f,A,C reconsider G = G as ManySortedFunction of B * f,C * (g * f) by Def4; reconsider F = F as ManySortedFunction of A,B * f by Def4; A2: dom G = I1 by PARTFUN1:def_2; A3: dom F = I1 by PARTFUN1:def_2; A4: dom (G ** F) = (dom G) /\ (dom F) by PBOOLE:def_19 .= I1 by A2, A3 ; reconsider GF = G ** F as ManySortedSet of I1 ; GF is ManySortedFunction of A,C * (g * f) proof let ii be set ; :: according to PBOOLE:def_15 ::_thesis: ( not ii in I1 or GF . ii is Element of bool [:(A . ii),((C * (g * f)) . ii):] ) assume A5: ii in I1 ; ::_thesis: GF . ii is Element of bool [:(A . ii),((C * (g * f)) . ii):] then reconsider Fi = F . ii as Function of (A . ii),((B * f) . ii) by PBOOLE:def_15; reconsider Gi = G . ii as Function of ((B * f) . ii),((C * (g * f)) . ii) by A5, PBOOLE:def_15; ( not (B * f) . ii = {} or A . ii = {} or (C * (g * f)) . ii = {} ) by A1, A5; then Gi * Fi is Function of (A . ii),((C * (g * f)) . ii) by FUNCT_2:13; hence GF . ii is Element of bool [:(A . ii),((C * (g * f)) . ii):] by A4, A5, PBOOLE:def_19; ::_thesis: verum end; hence G ** F is MSUnTrans of g * f,A,C by Def4; ::_thesis: verum end; begin definition let C1, C2 be 1-sorted ; attrc3 is strict ; struct BimapStr over C1,C2 -> ; aggrBimapStr(# ObjectMap #) -> BimapStr over C1,C2; sel ObjectMap c3 -> bifunction of the carrier of C1, the carrier of C2; end; definition let C1, C2 be non empty AltGraph ; let F be BimapStr over C1,C2; let o be object of C1; funcF . o -> object of C2 equals :: FUNCTOR0:def 5 ( the ObjectMap of F . (o,o)) `1 ; coherence ( the ObjectMap of F . (o,o)) `1 is object of C2 by MCART_1:10; end; :: deftheorem defines . FUNCTOR0:def_5_:_ for C1, C2 being non empty AltGraph for F being BimapStr over C1,C2 for o being object of C1 holds F . o = ( the ObjectMap of F . (o,o)) `1 ; definition let A, B be 1-sorted ; let F be BimapStr over A,B; attrF is one-to-one means :Def6: :: FUNCTOR0:def 6 the ObjectMap of F is one-to-one ; attrF is onto means :Def7: :: FUNCTOR0:def 7 the ObjectMap of F is onto ; attrF is reflexive means :Def8: :: FUNCTOR0:def 8 the ObjectMap of F .: (id the carrier of A) c= id the carrier of B; attrF is coreflexive means :Def9: :: FUNCTOR0:def 9 id the carrier of B c= the ObjectMap of F .: (id the carrier of A); end; :: deftheorem Def6 defines one-to-one FUNCTOR0:def_6_:_ for A, B being 1-sorted for F being BimapStr over A,B holds ( F is one-to-one iff the ObjectMap of F is one-to-one ); :: deftheorem Def7 defines onto FUNCTOR0:def_7_:_ for A, B being 1-sorted for F being BimapStr over A,B holds ( F is onto iff the ObjectMap of F is onto ); :: deftheorem Def8 defines reflexive FUNCTOR0:def_8_:_ for A, B being 1-sorted for F being BimapStr over A,B holds ( F is reflexive iff the ObjectMap of F .: (id the carrier of A) c= id the carrier of B ); :: deftheorem Def9 defines coreflexive FUNCTOR0:def_9_:_ for A, B being 1-sorted for F being BimapStr over A,B holds ( F is coreflexive iff id the carrier of B c= the ObjectMap of F .: (id the carrier of A) ); definition let A, B be non empty AltGraph ; let F be BimapStr over A,B; redefine attr F is reflexive means :Def10: :: FUNCTOR0:def 10 for o being object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)]; compatibility ( F is reflexive iff for o being object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] ) proof hereby ::_thesis: ( ( for o being object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] ) implies F is reflexive ) assume F is reflexive ; ::_thesis: for o being object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] then A1: the ObjectMap of F .: (id the carrier of A) c= id the carrier of B by Def8; let o be object of A; ::_thesis: the ObjectMap of F . (o,o) = [(F . o),(F . o)] [o,o] in id the carrier of A by RELAT_1:def_10; then A2: the ObjectMap of F . (o,o) in the ObjectMap of F .: (id the carrier of A) by FUNCT_2:35; consider p, p9 being set such that A3: the ObjectMap of F . (o,o) = [p,p9] by RELAT_1:def_1; F . o = p by A3, MCART_1:7; hence the ObjectMap of F . (o,o) = [(F . o),(F . o)] by A1, A2, A3, RELAT_1:def_10; ::_thesis: verum end; assume A4: for o being object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] ; ::_thesis: F is reflexive let x be set ; :: according to TARSKI:def_3,FUNCTOR0:def_8 ::_thesis: ( not x in the ObjectMap of F .: (id the carrier of A) or x in id the carrier of B ) assume x in the ObjectMap of F .: (id the carrier of A) ; ::_thesis: x in id the carrier of B then consider y being set such that A5: y in [: the carrier of A, the carrier of A:] and A6: y in id the carrier of A and A7: x = the ObjectMap of F . y by FUNCT_2:64; consider o, o9 being Element of A such that A8: y = [o,o9] by A5, DOMAIN_1:1; reconsider o = o as object of A ; o = o9 by A6, A8, RELAT_1:def_10; then x = [(F . o),(F . o)] by A4, A7, A8; hence x in id the carrier of B by RELAT_1:def_10; ::_thesis: verum end; end; :: deftheorem Def10 defines reflexive FUNCTOR0:def_10_:_ for A, B being non empty AltGraph for F being BimapStr over A,B holds ( F is reflexive iff for o being object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] ); theorem Th20: :: FUNCTOR0:20 for A, B being non empty reflexive AltGraph for F being BimapStr over A,B st F is coreflexive holds for o being object of B ex o9 being object of A st F . o9 = o proof let A, B be non empty reflexive AltGraph ; ::_thesis: for F being BimapStr over A,B st F is coreflexive holds for o being object of B ex o9 being object of A st F . o9 = o let F be BimapStr over A,B; ::_thesis: ( F is coreflexive implies for o being object of B ex o9 being object of A st F . o9 = o ) assume F is coreflexive ; ::_thesis: for o being object of B ex o9 being object of A st F . o9 = o then A1: id the carrier of B c= the ObjectMap of F .: (id the carrier of A) by Def9; let o be object of B; ::_thesis: ex o9 being object of A st F . o9 = o reconsider oo = [o,o] as Element of [: the carrier of B, the carrier of B:] by ZFMISC_1:87; [o,o] in id the carrier of B by RELAT_1:def_10; then consider pp being Element of [: the carrier of A, the carrier of A:] such that A2: pp in id the carrier of A and A3: the ObjectMap of F . pp = oo by A1, FUNCT_2:65; consider p, p9 being set such that A4: pp = [p,p9] by RELAT_1:def_1; A5: p = p9 by A2, A4, RELAT_1:def_10; reconsider p = p as object of A by A2, A4, RELAT_1:def_10; take p ; ::_thesis: F . p = o thus F . p = o by A3, A4, A5, MCART_1:7; ::_thesis: verum end; definition let C1, C2 be non empty AltGraph ; let F be BimapStr over C1,C2; attrF is feasible means :Def11: :: FUNCTOR0:def 11 for o1, o2 being object of C1 st <^o1,o2^> <> {} holds the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} ; end; :: deftheorem Def11 defines feasible FUNCTOR0:def_11_:_ for C1, C2 being non empty AltGraph for F being BimapStr over C1,C2 holds ( F is feasible iff for o1, o2 being object of C1 st <^o1,o2^> <> {} holds the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} ); definition let C1, C2 be AltGraph ; attrc3 is strict ; struct FunctorStr over C1,C2 -> BimapStr over C1,C2; aggrFunctorStr(# ObjectMap, MorphMap #) -> FunctorStr over C1,C2; sel MorphMap c3 -> MSUnTrans of the ObjectMap of c3, the Arrows of C1, the Arrows of C2; end; definition let C1, C2 be 1-sorted ; let IT be BimapStr over C1,C2; attrIT is Covariant means :Def12: :: FUNCTOR0:def 12 the ObjectMap of IT is Covariant ; attrIT is Contravariant means :Def13: :: FUNCTOR0:def 13 the ObjectMap of IT is Contravariant ; end; :: deftheorem Def12 defines Covariant FUNCTOR0:def_12_:_ for C1, C2 being 1-sorted for IT being BimapStr over C1,C2 holds ( IT is Covariant iff the ObjectMap of IT is Covariant ); :: deftheorem Def13 defines Contravariant FUNCTOR0:def_13_:_ for C1, C2 being 1-sorted for IT being BimapStr over C1,C2 holds ( IT is Contravariant iff the ObjectMap of IT is Contravariant ); registration let C1, C2 be AltGraph ; cluster Covariant for FunctorStr over C1,C2; existence ex b1 being FunctorStr over C1,C2 st b1 is Covariant proof set f = the Covariant bifunction of the carrier of C1, the carrier of C2; set M = the MSUnTrans of the Covariant bifunction of the carrier of C1, the carrier of C2, the Arrows of C1, the Arrows of C2; take F = FunctorStr(# the Covariant bifunction of the carrier of C1, the carrier of C2, the MSUnTrans of the Covariant bifunction of the carrier of C1, the carrier of C2, the Arrows of C1, the Arrows of C2 #); ::_thesis: F is Covariant thus the ObjectMap of F is Covariant ; :: according to FUNCTOR0:def_12 ::_thesis: verum end; cluster Contravariant for FunctorStr over C1,C2; existence ex b1 being FunctorStr over C1,C2 st b1 is Contravariant proof set f = the Contravariant bifunction of the carrier of C1, the carrier of C2; set M = the MSUnTrans of the Contravariant bifunction of the carrier of C1, the carrier of C2, the Arrows of C1, the Arrows of C2; take F = FunctorStr(# the Contravariant bifunction of the carrier of C1, the carrier of C2, the MSUnTrans of the Contravariant bifunction of the carrier of C1, the carrier of C2, the Arrows of C1, the Arrows of C2 #); ::_thesis: F is Contravariant thus the ObjectMap of F is Contravariant ; :: according to FUNCTOR0:def_13 ::_thesis: verum end; end; definition let C1, C2 be AltGraph ; let F be FunctorStr over C1,C2; let o1, o2 be object of C1; func Morph-Map (F,o1,o2) -> set equals :: FUNCTOR0:def 14 the MorphMap of F . (o1,o2); correctness coherence the MorphMap of F . (o1,o2) is set ; ; end; :: deftheorem defines Morph-Map FUNCTOR0:def_14_:_ for C1, C2 being AltGraph for F being FunctorStr over C1,C2 for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) = the MorphMap of F . (o1,o2); registration let C1, C2 be AltGraph ; let F be FunctorStr over C1,C2; let o1, o2 be object of C1; cluster Morph-Map (F,o1,o2) -> Relation-like Function-like ; coherence ( Morph-Map (F,o1,o2) is Relation-like & Morph-Map (F,o1,o2) is Function-like ) ; end; definition let C1, C2 be non empty AltGraph ; let F be Covariant FunctorStr over C1,C2; let o1, o2 be object of C1; :: original: Morph-Map redefine func Morph-Map (F,o1,o2) -> Function of <^o1,o2^>,<^(F . o1),(F . o2)^>; coherence Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o1),(F . o2)^> proof consider I29 being non empty set , B9 being ManySortedSet of I29, f9 being Function of [: the carrier of C1, the carrier of C1:],I29 such that A1: the ObjectMap of F = f9 and A2: the Arrows of C2 = B9 and A3: the MorphMap of F is ManySortedFunction of the Arrows of C1,B9 * f9 by Def3; A4: the Arrows of C1 . [o1,o2] = the Arrows of C1 . (o1,o2) .= <^o1,o2^> by ALTCAT_1:def_1 ; A5: [o1,o2] in [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87; the ObjectMap of F is Covariant by Def12; then consider g being Function of the carrier of C1, the carrier of C2 such that A6: the ObjectMap of F = [:g,g:] by Def1; A7: F . o1 = [(g . o1),(g . o1)] `1 by A6, FUNCT_3:75 .= g . o1 ; A8: F . o2 = [(g . o2),(g . o2)] `1 by A6, FUNCT_3:75 .= g . o2 ; dom f9 = [: the carrier of C1, the carrier of C1:] by FUNCT_2:def_1; then (B9 * f9) . [o1,o2] = B9 . (f9 . (o1,o2)) by A5, FUNCT_1:13 .= the Arrows of C2 . ((F . o1),(F . o2)) by A1, A2, A6, A7, A8, FUNCT_3:75 .= <^(F . o1),(F . o2)^> by ALTCAT_1:def_1 ; hence Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o1),(F . o2)^> by A3, A4, A5, PBOOLE:def_15; ::_thesis: verum end; end; definition let C1, C2 be non empty AltGraph ; let F be Covariant FunctorStr over C1,C2; let o1, o2 be object of C1; assume that A1: <^o1,o2^> <> {} and A2: <^(F . o1),(F . o2)^> <> {} ; let m be Morphism of o1,o2; funcF . m -> Morphism of (F . o1),(F . o2) equals :Def15: :: FUNCTOR0:def 15 (Morph-Map (F,o1,o2)) . m; coherence (Morph-Map (F,o1,o2)) . m is Morphism of (F . o1),(F . o2) proof reconsider A = <^o1,o2^>, B = <^(F . o1),(F . o2)^> as non empty set by A1, A2; reconsider M = Morph-Map (F,o1,o2) as Function of A,B ; reconsider m = m as Element of A ; M . m is Element of B ; hence (Morph-Map (F,o1,o2)) . m is Morphism of (F . o1),(F . o2) ; ::_thesis: verum end; end; :: deftheorem Def15 defines . FUNCTOR0:def_15_:_ for C1, C2 being non empty AltGraph for F being Covariant FunctorStr over C1,C2 for o1, o2 being object of C1 st <^o1,o2^> <> {} & <^(F . o1),(F . o2)^> <> {} holds for m being Morphism of o1,o2 holds F . m = (Morph-Map (F,o1,o2)) . m; definition let C1, C2 be non empty AltGraph ; let F be Contravariant FunctorStr over C1,C2; let o1, o2 be object of C1; :: original: Morph-Map redefine func Morph-Map (F,o1,o2) -> Function of <^o1,o2^>,<^(F . o2),(F . o1)^>; coherence Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o2),(F . o1)^> proof consider I29 being non empty set , B9 being ManySortedSet of I29, f9 being Function of [: the carrier of C1, the carrier of C1:],I29 such that A1: the ObjectMap of F = f9 and A2: the Arrows of C2 = B9 and A3: the MorphMap of F is ManySortedFunction of the Arrows of C1,B9 * f9 by Def3; A4: the Arrows of C1 . [o1,o2] = the Arrows of C1 . (o1,o2) .= <^o1,o2^> by ALTCAT_1:def_1 ; A5: [o1,o2] in [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87; the ObjectMap of F is Contravariant by Def13; then consider g being Function of the carrier of C1, the carrier of C2 such that A6: the ObjectMap of F = ~ [:g,g:] by Def2; A7: dom f9 = [: the carrier of C1, the carrier of C1:] by FUNCT_2:def_1; then [o1,o1] in dom (~ [:g,g:]) by A1, A6, ZFMISC_1:87; then [o1,o1] in dom [:g,g:] by FUNCT_4:42; then A8: F . o1 = ([:g,g:] . (o1,o1)) `1 by A6, FUNCT_4:def_2 .= [(g . o1),(g . o1)] `1 by FUNCT_3:75 .= g . o1 ; [o2,o2] in dom (~ [:g,g:]) by A1, A6, A7, ZFMISC_1:87; then [o2,o2] in dom [:g,g:] by FUNCT_4:42; then A9: F . o2 = ([:g,g:] . (o2,o2)) `1 by A6, FUNCT_4:def_2 .= [(g . o2),(g . o2)] `1 by FUNCT_3:75 .= g . o2 ; [o1,o2] in dom (~ [:g,g:]) by A1, A6, A7, ZFMISC_1:87; then A10: [o2,o1] in dom [:g,g:] by FUNCT_4:42; (B9 * f9) . [o1,o2] = B9 . (f9 . (o1,o2)) by A5, A7, FUNCT_1:13 .= B9 . ([:g,g:] . (o2,o1)) by A1, A6, A10, FUNCT_4:def_2 .= the Arrows of C2 . ((F . o2),(F . o1)) by A2, A8, A9, FUNCT_3:75 .= <^(F . o2),(F . o1)^> by ALTCAT_1:def_1 ; hence Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o2),(F . o1)^> by A3, A4, A5, PBOOLE:def_15; ::_thesis: verum end; end; definition let C1, C2 be non empty AltGraph ; let F be Contravariant FunctorStr over C1,C2; let o1, o2 be object of C1; assume that A1: <^o1,o2^> <> {} and A2: <^(F . o2),(F . o1)^> <> {} ; let m be Morphism of o1,o2; funcF . m -> Morphism of (F . o2),(F . o1) equals :Def16: :: FUNCTOR0:def 16 (Morph-Map (F,o1,o2)) . m; coherence (Morph-Map (F,o1,o2)) . m is Morphism of (F . o2),(F . o1) proof reconsider A = <^o1,o2^>, B = <^(F . o2),(F . o1)^> as non empty set by A1, A2; reconsider M = Morph-Map (F,o1,o2) as Function of A,B ; reconsider m = m as Element of A ; M . m is Element of B ; hence (Morph-Map (F,o1,o2)) . m is Morphism of (F . o2),(F . o1) ; ::_thesis: verum end; end; :: deftheorem Def16 defines . FUNCTOR0:def_16_:_ for C1, C2 being non empty AltGraph for F being Contravariant FunctorStr over C1,C2 for o1, o2 being object of C1 st <^o1,o2^> <> {} & <^(F . o2),(F . o1)^> <> {} holds for m being Morphism of o1,o2 holds F . m = (Morph-Map (F,o1,o2)) . m; definition let C1, C2 be non empty AltGraph ; let o be object of C2; assume B1: <^o,o^> <> {} ; let m be Morphism of o,o; funcC1 --> m -> strict FunctorStr over C1,C2 means :Def17: :: FUNCTOR0:def 17 ( the ObjectMap of it = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of it = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ); existence ex b1 being strict FunctorStr over C1,C2 st ( the ObjectMap of b1 = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b1 = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ) proof set I1 = [: the carrier of C1, the carrier of C1:]; set I2 = [: the carrier of C2, the carrier of C2:]; set A = the Arrows of C1; set B = the Arrows of C2; reconsider oo = [o,o] as Element of [: the carrier of C2, the carrier of C2:] by ZFMISC_1:87; the Arrows of C2 . oo = the Arrows of C2 . (o,o) .= <^o,o^> by ALTCAT_1:def_1 ; then reconsider m = m as Element of the Arrows of C2 . oo ; reconsider f = [: the carrier of C1, the carrier of C1:] --> oo as Function of [: the carrier of C1, the carrier of C1:],[: the carrier of C2, the carrier of C2:] ; reconsider f = f as bifunction of the carrier of C1, the carrier of C2 ; set M = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ; A1: { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } = { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } proof thus { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } c= { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } :: according to XBOOLE_0:def_10 ::_thesis: { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } c= { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } or x in { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } ) assume x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ; ::_thesis: x in { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } then consider o3, o4 being object of C1 such that A2: x = [[o3,o4],(<^o3,o4^> --> m)] ; reconsider oo = [o3,o4] as Element of [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87; x = [oo,(( the Arrows of C1 . (o3,o4)) --> m)] by A2, ALTCAT_1:def_1 .= [oo,(( the Arrows of C1 . oo) --> m)] ; hence x in { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } or x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ) assume x in { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } ; ::_thesis: x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } then consider o9 being Element of [: the carrier of C1, the carrier of C1:] such that A3: x = [o9,(( the Arrows of C1 . o9) --> m)] ; reconsider o1 = o9 `1 , o2 = o9 `2 as Element of C1 by MCART_1:10; reconsider o1 = o1, o2 = o2 as object of C1 ; o9 = [o1,o2] by MCART_1:21; then x = [[o1,o2],(( the Arrows of C1 . (o1,o2)) --> m)] by A3 .= [[o1,o2],(<^o1,o2^> --> m)] by ALTCAT_1:def_1 ; hence x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ; ::_thesis: verum end; the Arrows of C2 . (o,o) <> {} by B1, ALTCAT_1:def_1; then reconsider M = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } as MSUnTrans of f, the Arrows of C1, the Arrows of C2 by A1, Th18; take FunctorStr(# f,M #) ; ::_thesis: ( the ObjectMap of FunctorStr(# f,M #) = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of FunctorStr(# f,M #) = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ) thus ( the ObjectMap of FunctorStr(# f,M #) = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of FunctorStr(# f,M #) = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict FunctorStr over C1,C2 st the ObjectMap of b1 = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b1 = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } & the ObjectMap of b2 = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b2 = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } holds b1 = b2 ; end; :: deftheorem Def17 defines --> FUNCTOR0:def_17_:_ for C1, C2 being non empty AltGraph for o being object of C2 st <^o,o^> <> {} holds for m being Morphism of o,o for b5 being strict FunctorStr over C1,C2 holds ( b5 = C1 --> m iff ( the ObjectMap of b5 = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b5 = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ) ); theorem Th21: :: FUNCTOR0:21 for C1, C2 being non empty AltGraph for o2 being object of C2 st <^o2,o2^> <> {} holds for m being Morphism of o2,o2 for o1 being object of C1 holds (C1 --> m) . o1 = o2 proof let C1, C2 be non empty AltGraph ; ::_thesis: for o2 being object of C2 st <^o2,o2^> <> {} holds for m being Morphism of o2,o2 for o1 being object of C1 holds (C1 --> m) . o1 = o2 let o2 be object of C2; ::_thesis: ( <^o2,o2^> <> {} implies for m being Morphism of o2,o2 for o1 being object of C1 holds (C1 --> m) . o1 = o2 ) assume A1: <^o2,o2^> <> {} ; ::_thesis: for m being Morphism of o2,o2 for o1 being object of C1 holds (C1 --> m) . o1 = o2 let m be Morphism of o2,o2; ::_thesis: for o1 being object of C1 holds (C1 --> m) . o1 = o2 let o1 be object of C1; ::_thesis: (C1 --> m) . o1 = o2 A2: [o1,o1] in [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87; thus (C1 --> m) . o1 = (([: the carrier of C1, the carrier of C1:] --> [o2,o2]) . (o1,o1)) `1 by A1, Def17 .= [o2,o2] `1 by A2, FUNCOP_1:7 .= o2 ; ::_thesis: verum end; registration let C1 be non empty AltGraph ; let C2 be non empty reflexive AltGraph ; let o be object of C2; let m be Morphism of o,o; clusterC1 --> m -> feasible strict Covariant Contravariant ; coherence ( C1 --> m is Covariant & C1 --> m is Contravariant & C1 --> m is feasible ) proof <^o,o^> <> {} by ALTCAT_2:def_7; then A1: the ObjectMap of (C1 --> m) = [: the carrier of C1, the carrier of C1:] --> [o,o] by Def17; hence ( the ObjectMap of (C1 --> m) is Covariant & the ObjectMap of (C1 --> m) is Contravariant ) by Th15; :: according to FUNCTOR0:def_12,FUNCTOR0:def_13 ::_thesis: C1 --> m is feasible let o1, o2 be object of C1; :: according to FUNCTOR0:def_11 ::_thesis: ( <^o1,o2^> <> {} implies the Arrows of C2 . ( the ObjectMap of (C1 --> m) . (o1,o2)) <> {} ) assume <^o1,o2^> <> {} ; ::_thesis: the Arrows of C2 . ( the ObjectMap of (C1 --> m) . (o1,o2)) <> {} [o1,o2] in [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87; then the Arrows of C2 . ( the ObjectMap of (C1 --> m) . (o1,o2)) = the Arrows of C2 . (o,o) by A1, FUNCOP_1:7; hence the Arrows of C2 . ( the ObjectMap of (C1 --> m) . (o1,o2)) <> {} by ALTCAT_2:def_6; ::_thesis: verum end; end; registration let C1 be non empty AltGraph ; let C2 be non empty reflexive AltGraph ; cluster feasible Covariant Contravariant for FunctorStr over C1,C2; existence ex b1 being FunctorStr over C1,C2 st ( b1 is feasible & b1 is Covariant & b1 is Contravariant ) proof set o = the object of C2; set m = the Morphism of the object of C2, the object of C2; take C1 --> the Morphism of the object of C2, the object of C2 ; ::_thesis: ( C1 --> the Morphism of the object of C2, the object of C2 is feasible & C1 --> the Morphism of the object of C2, the object of C2 is Covariant & C1 --> the Morphism of the object of C2, the object of C2 is Contravariant ) thus ( C1 --> the Morphism of the object of C2, the object of C2 is feasible & C1 --> the Morphism of the object of C2, the object of C2 is Covariant & C1 --> the Morphism of the object of C2, the object of C2 is Contravariant ) ; ::_thesis: verum end; end; theorem Th22: :: FUNCTOR0:22 for C1, C2 being non empty AltGraph for F being Covariant FunctorStr over C1,C2 for o1, o2 being object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)] proof let C1, C2 be non empty AltGraph ; ::_thesis: for F being Covariant FunctorStr over C1,C2 for o1, o2 being object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)] let F be Covariant FunctorStr over C1,C2; ::_thesis: for o1, o2 being object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)] let o1, o2 be object of C1; ::_thesis: the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)] the ObjectMap of F is Covariant by Def12; then consider f being Function of the carrier of C1, the carrier of C2 such that A1: the ObjectMap of F = [:f,f:] by Def1; A2: F . o1 = [(f . o1),(f . o1)] `1 by A1, FUNCT_3:75 .= f . o1 ; F . o2 = [(f . o2),(f . o2)] `1 by A1, FUNCT_3:75 .= f . o2 ; hence the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)] by A1, A2, FUNCT_3:75; ::_thesis: verum end; definition let C1, C2 be non empty AltGraph ; let F be Covariant FunctorStr over C1,C2; redefine attr F is feasible means :Def18: :: FUNCTOR0:def 18 for o1, o2 being object of C1 st <^o1,o2^> <> {} holds <^(F . o1),(F . o2)^> <> {} ; compatibility ( F is feasible iff for o1, o2 being object of C1 st <^o1,o2^> <> {} holds <^(F . o1),(F . o2)^> <> {} ) proof hereby ::_thesis: ( ( for o1, o2 being object of C1 st <^o1,o2^> <> {} holds <^(F . o1),(F . o2)^> <> {} ) implies F is feasible ) assume A1: F is feasible ; ::_thesis: for o1, o2 being object of C1 st <^o1,o2^> <> {} holds <^(F . o1),(F . o2)^> <> {} let o1, o2 be object of C1; ::_thesis: ( <^o1,o2^> <> {} implies <^(F . o1),(F . o2)^> <> {} ) assume A2: <^o1,o2^> <> {} ; ::_thesis: <^(F . o1),(F . o2)^> <> {} <^(F . o1),(F . o2)^> = the Arrows of C2 . ((F . o1),(F . o2)) by ALTCAT_1:def_1 .= the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) by Th22 ; hence <^(F . o1),(F . o2)^> <> {} by A1, A2, Def11; ::_thesis: verum end; assume A3: for o1, o2 being object of C1 st <^o1,o2^> <> {} holds <^(F . o1),(F . o2)^> <> {} ; ::_thesis: F is feasible let o1, o2 be object of C1; :: according to FUNCTOR0:def_11 ::_thesis: ( <^o1,o2^> <> {} implies the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} ) assume A4: <^o1,o2^> <> {} ; ::_thesis: the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} <^(F . o1),(F . o2)^> = the Arrows of C2 . ((F . o1),(F . o2)) by ALTCAT_1:def_1 .= the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) by Th22 ; hence the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} by A3, A4; ::_thesis: verum end; end; :: deftheorem Def18 defines feasible FUNCTOR0:def_18_:_ for C1, C2 being non empty AltGraph for F being Covariant FunctorStr over C1,C2 holds ( F is feasible iff for o1, o2 being object of C1 st <^o1,o2^> <> {} holds <^(F . o1),(F . o2)^> <> {} ); theorem Th23: :: FUNCTOR0:23 for C1, C2 being non empty AltGraph for F being Contravariant FunctorStr over C1,C2 for o1, o2 being object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o2),(F . o1)] proof let C1, C2 be non empty AltGraph ; ::_thesis: for F being Contravariant FunctorStr over C1,C2 for o1, o2 being object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o2),(F . o1)] let F be Contravariant FunctorStr over C1,C2; ::_thesis: for o1, o2 being object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o2),(F . o1)] let o1, o2 be object of C1; ::_thesis: the ObjectMap of F . (o1,o2) = [(F . o2),(F . o1)] the ObjectMap of F is Contravariant by Def13; then consider f being Function of the carrier of C1, the carrier of C2 such that A1: the ObjectMap of F = ~ [:f,f:] by Def2; A2: dom [:f,f:] = [: the carrier of C1, the carrier of C1:] by FUNCT_2:def_1; then [o1,o1] in dom [:f,f:] by ZFMISC_1:87; then A3: F . o1 = ([:f,f:] . (o1,o1)) `1 by A1, FUNCT_4:def_2 .= [(f . o1),(f . o1)] `1 by FUNCT_3:75 .= f . o1 ; [o2,o2] in dom [:f,f:] by A2, ZFMISC_1:87; then A4: F . o2 = ([:f,f:] . (o2,o2)) `1 by A1, FUNCT_4:def_2 .= [(f . o2),(f . o2)] `1 by FUNCT_3:75 .= f . o2 ; [o2,o1] in dom [:f,f:] by A2, ZFMISC_1:87; hence the ObjectMap of F . (o1,o2) = [:f,f:] . (o2,o1) by A1, FUNCT_4:def_2 .= [(F . o2),(F . o1)] by A3, A4, FUNCT_3:75 ; ::_thesis: verum end; definition let C1, C2 be non empty AltGraph ; let F be Contravariant FunctorStr over C1,C2; redefine attr F is feasible means :Def19: :: FUNCTOR0:def 19 for o1, o2 being object of C1 st <^o1,o2^> <> {} holds <^(F . o2),(F . o1)^> <> {} ; compatibility ( F is feasible iff for o1, o2 being object of C1 st <^o1,o2^> <> {} holds <^(F . o2),(F . o1)^> <> {} ) proof hereby ::_thesis: ( ( for o1, o2 being object of C1 st <^o1,o2^> <> {} holds <^(F . o2),(F . o1)^> <> {} ) implies F is feasible ) assume A1: F is feasible ; ::_thesis: for o1, o2 being object of C1 st <^o1,o2^> <> {} holds <^(F . o2),(F . o1)^> <> {} let o1, o2 be object of C1; ::_thesis: ( <^o1,o2^> <> {} implies <^(F . o2),(F . o1)^> <> {} ) assume A2: <^o1,o2^> <> {} ; ::_thesis: <^(F . o2),(F . o1)^> <> {} <^(F . o2),(F . o1)^> = the Arrows of C2 . ((F . o2),(F . o1)) by ALTCAT_1:def_1 .= the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) by Th23 ; hence <^(F . o2),(F . o1)^> <> {} by A1, A2, Def11; ::_thesis: verum end; assume A3: for o1, o2 being object of C1 st <^o1,o2^> <> {} holds <^(F . o2),(F . o1)^> <> {} ; ::_thesis: F is feasible let o1, o2 be object of C1; :: according to FUNCTOR0:def_11 ::_thesis: ( <^o1,o2^> <> {} implies the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} ) assume A4: <^o1,o2^> <> {} ; ::_thesis: the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} <^(F . o2),(F . o1)^> = the Arrows of C2 . ((F . o2),(F . o1)) by ALTCAT_1:def_1 .= the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) by Th23 ; hence the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} by A3, A4; ::_thesis: verum end; end; :: deftheorem Def19 defines feasible FUNCTOR0:def_19_:_ for C1, C2 being non empty AltGraph for F being Contravariant FunctorStr over C1,C2 holds ( F is feasible iff for o1, o2 being object of C1 st <^o1,o2^> <> {} holds <^(F . o2),(F . o1)^> <> {} ); registration let C1, C2 be AltGraph ; let F be FunctorStr over C1,C2; cluster the MorphMap of F -> Function-yielding ; coherence the MorphMap of F is Function-yielding ; end; registration cluster non empty reflexive for AltCatStr ; existence ex b1 being AltCatStr st ( not b1 is empty & b1 is reflexive ) proof set C = the category; take the category ; ::_thesis: ( not the category is empty & the category is reflexive ) thus ( not the category is empty & the category is reflexive ) ; ::_thesis: verum end; end; definition let C1, C2 be non empty with_units AltCatStr ; let F be FunctorStr over C1,C2; attrF is id-preserving means :Def20: :: FUNCTOR0:def 20 for o being object of C1 holds (Morph-Map (F,o,o)) . (idm o) = idm (F . o); end; :: deftheorem Def20 defines id-preserving FUNCTOR0:def_20_:_ for C1, C2 being non empty with_units AltCatStr for F being FunctorStr over C1,C2 holds ( F is id-preserving iff for o being object of C1 holds (Morph-Map (F,o,o)) . (idm o) = idm (F . o) ); theorem Th24: :: FUNCTOR0:24 for C1, C2 being non empty AltGraph for o2 being object of C2 st <^o2,o2^> <> {} holds for m being Morphism of o2,o2 for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds (Morph-Map ((C1 --> m),o,o9)) . f = m proof let C1, C2 be non empty AltGraph ; ::_thesis: for o2 being object of C2 st <^o2,o2^> <> {} holds for m being Morphism of o2,o2 for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds (Morph-Map ((C1 --> m),o,o9)) . f = m let o2 be object of C2; ::_thesis: ( <^o2,o2^> <> {} implies for m being Morphism of o2,o2 for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds (Morph-Map ((C1 --> m),o,o9)) . f = m ) assume A1: <^o2,o2^> <> {} ; ::_thesis: for m being Morphism of o2,o2 for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds (Morph-Map ((C1 --> m),o,o9)) . f = m let m be Morphism of o2,o2; ::_thesis: for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds (Morph-Map ((C1 --> m),o,o9)) . f = m let o, o9 be object of C1; ::_thesis: for f being Morphism of o,o9 st <^o,o9^> <> {} holds (Morph-Map ((C1 --> m),o,o9)) . f = m let f be Morphism of o,o9; ::_thesis: ( <^o,o9^> <> {} implies (Morph-Map ((C1 --> m),o,o9)) . f = m ) assume A2: <^o,o9^> <> {} ; ::_thesis: (Morph-Map ((C1 --> m),o,o9)) . f = m set X = { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } ; set Y = { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } ; A3: { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } c= { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } or e in { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } ) assume e in { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } ; ::_thesis: e in { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } then consider o1, o19 being object of C1 such that A4: e = [[o1,o19],(<^o1,o19^> --> m)] ; e = [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] by A4, ALTCAT_1:def_1; hence e in { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } ; ::_thesis: verum end; A5: { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } c= { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } or e in { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } ) assume e in { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } ; ::_thesis: e in { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } then consider o1, o19 being Element of C1 such that A6: e = [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] ; reconsider o1 = o1, o19 = o19 as object of C1 ; e = [[o1,o19],(<^o1,o19^> --> m)] by A6, ALTCAT_1:def_1; hence e in { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } ; ::_thesis: verum end; defpred S1[ set , set ] means verum; deffunc H1( Element of C1, Element of C1) -> Element of bool [:( the Arrows of C1 . ($1,$2)),{m}:] = ( the Arrows of C1 . ($1,$2)) --> m; the MorphMap of (C1 --> m) = { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } by A1, Def17; then A7: the MorphMap of (C1 --> m) = { [[o1,o19],H1(o1,o19)] where o1, o19 is Element of C1 : S1[o1,o19] } by A3, A5, XBOOLE_0:def_10; A8: S1[o,o9] ; Morph-Map ((C1 --> m),o,o9) = the MorphMap of (C1 --> m) . (o,o9) .= H1(o,o9) from FUNCTOR0:sch_1(A7, A8) ; hence (Morph-Map ((C1 --> m),o,o9)) . f = (<^o,o9^> --> m) . f by ALTCAT_1:def_1 .= m by A2, FUNCOP_1:7 ; ::_thesis: verum end; registration cluster non empty with_units -> non empty reflexive for AltCatStr ; coherence for b1 being non empty AltCatStr st b1 is with_units holds b1 is reflexive ; end; registration let C1, C2 be non empty with_units AltCatStr ; let o2 be object of C2; clusterC1 --> (idm o2) -> strict id-preserving ; coherence C1 --> (idm o2) is id-preserving proof let o1 be object of C1; :: according to FUNCTOR0:def_20 ::_thesis: (Morph-Map ((C1 --> (idm o2)),o1,o1)) . (idm o1) = idm ((C1 --> (idm o2)) . o1) A1: <^o2,o2^> <> {} by ALTCAT_2:def_7; <^o1,o1^> <> {} by ALTCAT_2:def_7; hence (Morph-Map ((C1 --> (idm o2)),o1,o1)) . (idm o1) = idm o2 by A1, Th24 .= idm ((C1 --> (idm o2)) . o1) by A1, Th21 ; ::_thesis: verum end; end; registration let C1 be non empty AltGraph ; let C2 be non empty reflexive AltGraph ; let o2 be object of C2; let m be Morphism of o2,o2; clusterC1 --> m -> reflexive strict ; coherence C1 --> m is reflexive proof let o be object of C1; :: according to FUNCTOR0:def_10 ::_thesis: the ObjectMap of (C1 --> m) . (o,o) = [((C1 --> m) . o),((C1 --> m) . o)] A1: [o,o] in [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87; <^o2,o2^> <> {} by ALTCAT_2:def_7; then A2: the ObjectMap of (C1 --> m) . (o,o) = ([: the carrier of C1, the carrier of C1:] --> [o2,o2]) . [o,o] by Def17 .= [o2,o2] by A1, FUNCOP_1:7 ; then (C1 --> m) . o = o2 by MCART_1:7; hence the ObjectMap of (C1 --> m) . (o,o) = [((C1 --> m) . o),((C1 --> m) . o)] by A2; ::_thesis: verum end; end; registration let C1 be non empty AltGraph ; let C2 be non empty reflexive AltGraph ; cluster reflexive feasible for FunctorStr over C1,C2; existence ex b1 being FunctorStr over C1,C2 st ( b1 is feasible & b1 is reflexive ) proof set o2 = the object of C2; set m = the Morphism of the object of C2, the object of C2; take C1 --> the Morphism of the object of C2, the object of C2 ; ::_thesis: ( C1 --> the Morphism of the object of C2, the object of C2 is feasible & C1 --> the Morphism of the object of C2, the object of C2 is reflexive ) thus ( C1 --> the Morphism of the object of C2, the object of C2 is feasible & C1 --> the Morphism of the object of C2, the object of C2 is reflexive ) ; ::_thesis: verum end; end; registration let C1, C2 be non empty with_units AltCatStr ; cluster reflexive feasible strict id-preserving for FunctorStr over C1,C2; existence ex b1 being FunctorStr over C1,C2 st ( b1 is id-preserving & b1 is feasible & b1 is reflexive & b1 is strict ) proof set o2 = the object of C2; take C1 --> (idm the object of C2) ; ::_thesis: ( C1 --> (idm the object of C2) is id-preserving & C1 --> (idm the object of C2) is feasible & C1 --> (idm the object of C2) is reflexive & C1 --> (idm the object of C2) is strict ) thus ( C1 --> (idm the object of C2) is id-preserving & C1 --> (idm the object of C2) is feasible & C1 --> (idm the object of C2) is reflexive & C1 --> (idm the object of C2) is strict ) ; ::_thesis: verum end; end; definition let C1, C2 be non empty AltCatStr ; let F be FunctorStr over C1,C2; attrF is comp-preserving means :Def21: :: FUNCTOR0:def 21 for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ); end; :: deftheorem Def21 defines comp-preserving FUNCTOR0:def_21_:_ for C1, C2 being non empty AltCatStr for F being FunctorStr over C1,C2 holds ( F is comp-preserving iff for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ) ); definition let C1, C2 be non empty AltCatStr ; let F be FunctorStr over C1,C2; attrF is comp-reversing means :Def22: :: FUNCTOR0:def 22 for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex g9 being Morphism of (F . o3),(F . o2) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 ); end; :: deftheorem Def22 defines comp-reversing FUNCTOR0:def_22_:_ for C1, C2 being non empty AltCatStr for F being FunctorStr over C1,C2 holds ( F is comp-reversing iff for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex g9 being Morphism of (F . o3),(F . o2) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 ) ); definition let C1 be non empty transitive AltCatStr ; let C2 be non empty reflexive AltCatStr ; let F be feasible Covariant FunctorStr over C1,C2; redefine attr F is comp-preserving means :: FUNCTOR0:def 23 for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f); compatibility ( F is comp-preserving iff for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) ) proof hereby ::_thesis: ( ( for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) ) implies F is comp-preserving ) assume A1: F is comp-preserving ; ::_thesis: for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) let o1, o2, o3 be object of C1; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) ) assume that A2: <^o1,o2^> <> {} and A3: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) let g be Morphism of o2,o3; ::_thesis: F . (g * f) = (F . g) * (F . f) consider f9 being Morphism of (F . o1),(F . o2), g9 being Morphism of (F . o2),(F . o3) such that A4: f9 = (Morph-Map (F,o1,o2)) . f and A5: g9 = (Morph-Map (F,o2,o3)) . g and A6: (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 by A1, A2, A3, Def21; A7: <^(F . o1),(F . o2)^> <> {} by A2, Def18; A8: <^(F . o2),(F . o3)^> <> {} by A3, Def18; A9: f9 = F . f by A2, A4, A7, Def15; A10: g9 = F . g by A3, A5, A8, Def15; A11: <^o1,o3^> <> {} by A2, A3, ALTCAT_1:def_2; then <^(F . o1),(F . o3)^> <> {} by Def18; hence F . (g * f) = (F . g) * (F . f) by A6, A9, A10, A11, Def15; ::_thesis: verum end; assume A12: for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) ; ::_thesis: F is comp-preserving let o1, o2, o3 be object of C1; :: according to FUNCTOR0:def_21 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ) ) assume that A13: <^o1,o2^> <> {} and A14: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ) let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ) let g be Morphism of o2,o3; ::_thesis: ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ) A15: <^(F . o1),(F . o2)^> <> {} by A13, Def18; then reconsider f9 = (Morph-Map (F,o1,o2)) . f as Morphism of (F . o1),(F . o2) by A13, FUNCT_2:5; A16: <^(F . o2),(F . o3)^> <> {} by A14, Def18; then reconsider g9 = (Morph-Map (F,o2,o3)) . g as Morphism of (F . o2),(F . o3) by A14, FUNCT_2:5; take f9 ; ::_thesis: ex g9 being Morphism of (F . o2),(F . o3) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ) take g9 ; ::_thesis: ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ) thus ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g ) ; ::_thesis: (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 A17: f9 = F . f by A13, A15, Def15; A18: g9 = F . g by A14, A16, Def15; A19: <^o1,o3^> <> {} by A13, A14, ALTCAT_1:def_2; then <^(F . o1),(F . o3)^> <> {} by Def18; hence (Morph-Map (F,o1,o3)) . (g * f) = F . (g * f) by A19, Def15 .= g9 * f9 by A12, A13, A14, A17, A18 ; ::_thesis: verum end; end; :: deftheorem defines comp-preserving FUNCTOR0:def_23_:_ for C1 being non empty transitive AltCatStr for C2 being non empty reflexive AltCatStr for F being feasible Covariant FunctorStr over C1,C2 holds ( F is comp-preserving iff for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) ); definition let C1 be non empty transitive AltCatStr ; let C2 be non empty reflexive AltCatStr ; let F be feasible Contravariant FunctorStr over C1,C2; redefine attr F is comp-reversing means :: FUNCTOR0:def 24 for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g); compatibility ( F is comp-reversing iff for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) ) proof hereby ::_thesis: ( ( for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) ) implies F is comp-reversing ) assume A1: F is comp-reversing ; ::_thesis: for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) let o1, o2, o3 be object of C1; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) ) assume that A2: <^o1,o2^> <> {} and A3: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) let g be Morphism of o2,o3; ::_thesis: F . (g * f) = (F . f) * (F . g) consider f9 being Morphism of (F . o2),(F . o1), g9 being Morphism of (F . o3),(F . o2) such that A4: f9 = (Morph-Map (F,o1,o2)) . f and A5: g9 = (Morph-Map (F,o2,o3)) . g and A6: (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 by A1, A2, A3, Def22; A7: <^(F . o2),(F . o1)^> <> {} by A2, Def19; A8: <^(F . o3),(F . o2)^> <> {} by A3, Def19; A9: f9 = F . f by A2, A4, A7, Def16; A10: g9 = F . g by A3, A5, A8, Def16; A11: <^o1,o3^> <> {} by A2, A3, ALTCAT_1:def_2; then <^(F . o3),(F . o1)^> <> {} by Def19; hence F . (g * f) = (F . f) * (F . g) by A6, A9, A10, A11, Def16; ::_thesis: verum end; assume A12: for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) ; ::_thesis: F is comp-reversing let o1, o2, o3 be object of C1; :: according to FUNCTOR0:def_22 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex g9 being Morphism of (F . o3),(F . o2) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 ) ) assume that A13: <^o1,o2^> <> {} and A14: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex g9 being Morphism of (F . o3),(F . o2) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 ) let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex g9 being Morphism of (F . o3),(F . o2) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 ) let g be Morphism of o2,o3; ::_thesis: ex f9 being Morphism of (F . o2),(F . o1) ex g9 being Morphism of (F . o3),(F . o2) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 ) A15: <^(F . o2),(F . o1)^> <> {} by A13, Def19; then reconsider f9 = (Morph-Map (F,o1,o2)) . f as Morphism of (F . o2),(F . o1) by A13, FUNCT_2:5; A16: <^(F . o3),(F . o2)^> <> {} by A14, Def19; then reconsider g9 = (Morph-Map (F,o2,o3)) . g as Morphism of (F . o3),(F . o2) by A14, FUNCT_2:5; take f9 ; ::_thesis: ex g9 being Morphism of (F . o3),(F . o2) st ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 ) take g9 ; ::_thesis: ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 ) thus ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g ) ; ::_thesis: (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 A17: f9 = F . f by A13, A15, Def16; A18: g9 = F . g by A14, A16, Def16; A19: <^o1,o3^> <> {} by A13, A14, ALTCAT_1:def_2; then <^(F . o3),(F . o1)^> <> {} by Def19; hence (Morph-Map (F,o1,o3)) . (g * f) = F . (g * f) by A19, Def16 .= f9 * g9 by A12, A13, A14, A17, A18 ; ::_thesis: verum end; end; :: deftheorem defines comp-reversing FUNCTOR0:def_24_:_ for C1 being non empty transitive AltCatStr for C2 being non empty reflexive AltCatStr for F being feasible Contravariant FunctorStr over C1,C2 holds ( F is comp-reversing iff for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) ); theorem Th25: :: FUNCTOR0:25 for C1 being non empty AltGraph for C2 being non empty reflexive AltGraph for o2 being object of C2 for m being Morphism of o2,o2 for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds F . f = m proof let C1 be non empty AltGraph ; ::_thesis: for C2 being non empty reflexive AltGraph for o2 being object of C2 for m being Morphism of o2,o2 for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds F . f = m let C2 be non empty reflexive AltGraph ; ::_thesis: for o2 being object of C2 for m being Morphism of o2,o2 for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds F . f = m let o2 be object of C2; ::_thesis: for m being Morphism of o2,o2 for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds F . f = m A1: <^o2,o2^> <> {} by ALTCAT_2:def_7; let m be Morphism of o2,o2; ::_thesis: for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds F . f = m let F be feasible Covariant FunctorStr over C1,C2; ::_thesis: ( F = C1 --> m implies for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds F . f = m ) assume A2: F = C1 --> m ; ::_thesis: for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds F . f = m let o, o9 be object of C1; ::_thesis: for f being Morphism of o,o9 st <^o,o9^> <> {} holds F . f = m let f be Morphism of o,o9; ::_thesis: ( <^o,o9^> <> {} implies F . f = m ) assume A3: <^o,o9^> <> {} ; ::_thesis: F . f = m then <^(F . o),(F . o9)^> <> {} by Def18; hence F . f = (Morph-Map (F,o,o9)) . f by A3, Def15 .= m by A1, A2, A3, Th24 ; ::_thesis: verum end; theorem Th26: :: FUNCTOR0:26 for C1 being non empty AltGraph for C2 being non empty reflexive AltGraph for o2 being object of C2 for m being Morphism of o2,o2 for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds (C1 --> m) . f = m proof let C1 be non empty AltGraph ; ::_thesis: for C2 being non empty reflexive AltGraph for o2 being object of C2 for m being Morphism of o2,o2 for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds (C1 --> m) . f = m let C2 be non empty reflexive AltGraph ; ::_thesis: for o2 being object of C2 for m being Morphism of o2,o2 for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds (C1 --> m) . f = m let o2 be object of C2; ::_thesis: for m being Morphism of o2,o2 for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds (C1 --> m) . f = m A1: <^o2,o2^> <> {} by ALTCAT_2:def_7; let m be Morphism of o2,o2; ::_thesis: for o, o9 being object of C1 for f being Morphism of o,o9 st <^o,o9^> <> {} holds (C1 --> m) . f = m set F = C1 --> m; let o, o9 be object of C1; ::_thesis: for f being Morphism of o,o9 st <^o,o9^> <> {} holds (C1 --> m) . f = m let f be Morphism of o,o9; ::_thesis: ( <^o,o9^> <> {} implies (C1 --> m) . f = m ) assume A2: <^o,o9^> <> {} ; ::_thesis: (C1 --> m) . f = m then <^((C1 --> m) . o9),((C1 --> m) . o)^> <> {} by Def19; hence (C1 --> m) . f = (Morph-Map ((C1 --> m),o,o9)) . f by A2, Def16 .= m by A1, A2, Th24 ; ::_thesis: verum end; registration let C1 be non empty transitive AltCatStr ; let C2 be non empty with_units AltCatStr ; let o be object of C2; clusterC1 --> (idm o) -> strict comp-preserving comp-reversing ; coherence ( C1 --> (idm o) is comp-preserving & C1 --> (idm o) is comp-reversing ) proof set F = C1 --> (idm o); reconsider G = C1 --> (idm o) as feasible Covariant FunctorStr over C1,C2 ; A1: <^o,o^> <> {} by ALTCAT_2:def_7; G is comp-preserving proof let o1, o2, o3 be object of C1; :: according to FUNCTOR0:def_23 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds G . (g * f) = (G . g) * (G . f) ) assume that A2: <^o1,o2^> <> {} and A3: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds G . (g * f) = (G . g) * (G . f) A4: <^o1,o3^> <> {} by A2, A3, ALTCAT_1:def_2; let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 holds G . (g * f) = (G . g) * (G . f) let g be Morphism of o2,o3; ::_thesis: G . (g * f) = (G . g) * (G . f) A5: G . g = idm o by A3, Th25; A6: G . f = idm o by A2, Th25; A7: G . o1 = o by A1, Th21; A8: G . o2 = o by A1, Th21; A9: G . o3 = o by A1, Th21; thus G . (g * f) = idm o by A4, Th25 .= (G . g) * (G . f) by A1, A5, A6, A7, A8, A9, ALTCAT_1:20 ; ::_thesis: verum end; hence C1 --> (idm o) is comp-preserving ; ::_thesis: C1 --> (idm o) is comp-reversing let o1, o2, o3 be object of C1; :: according to FUNCTOR0:def_24 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds (C1 --> (idm o)) . (g * f) = ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g) ) assume that A10: <^o1,o2^> <> {} and A11: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds (C1 --> (idm o)) . (g * f) = ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g) A12: <^o1,o3^> <> {} by A10, A11, ALTCAT_1:def_2; let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 holds (C1 --> (idm o)) . (g * f) = ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g) let g be Morphism of o2,o3; ::_thesis: (C1 --> (idm o)) . (g * f) = ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g) A13: (C1 --> (idm o)) . g = idm o by A11, Th26; A14: (C1 --> (idm o)) . f = idm o by A10, Th26; A15: (C1 --> (idm o)) . o1 = o by A1, Th21; A16: (C1 --> (idm o)) . o2 = o by A1, Th21; A17: (C1 --> (idm o)) . o3 = o by A1, Th21; thus (C1 --> (idm o)) . (g * f) = idm o by A12, Th26 .= ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g) by A1, A13, A14, A15, A16, A17, ALTCAT_1:20 ; ::_thesis: verum end; end; definition let C1 be non empty transitive with_units AltCatStr ; let C2 be non empty with_units AltCatStr ; mode Functor of C1,C2 -> FunctorStr over C1,C2 means :Def25: :: FUNCTOR0:def 25 ( it is feasible & it is id-preserving & ( ( it is Covariant & it is comp-preserving ) or ( it is Contravariant & it is comp-reversing ) ) ); existence ex b1 being FunctorStr over C1,C2 st ( b1 is feasible & b1 is id-preserving & ( ( b1 is Covariant & b1 is comp-preserving ) or ( b1 is Contravariant & b1 is comp-reversing ) ) ) proof set o = the object of C2; take C1 --> (idm the object of C2) ; ::_thesis: ( C1 --> (idm the object of C2) is feasible & C1 --> (idm the object of C2) is id-preserving & ( ( C1 --> (idm the object of C2) is Covariant & C1 --> (idm the object of C2) is comp-preserving ) or ( C1 --> (idm the object of C2) is Contravariant & C1 --> (idm the object of C2) is comp-reversing ) ) ) thus ( C1 --> (idm the object of C2) is feasible & C1 --> (idm the object of C2) is id-preserving & ( ( C1 --> (idm the object of C2) is Covariant & C1 --> (idm the object of C2) is comp-preserving ) or ( C1 --> (idm the object of C2) is Contravariant & C1 --> (idm the object of C2) is comp-reversing ) ) ) ; ::_thesis: verum end; end; :: deftheorem Def25 defines Functor FUNCTOR0:def_25_:_ for C1 being non empty transitive with_units AltCatStr for C2 being non empty with_units AltCatStr for b3 being FunctorStr over C1,C2 holds ( b3 is Functor of C1,C2 iff ( b3 is feasible & b3 is id-preserving & ( ( b3 is Covariant & b3 is comp-preserving ) or ( b3 is Contravariant & b3 is comp-reversing ) ) ) ); definition let C1 be non empty transitive with_units AltCatStr ; let C2 be non empty with_units AltCatStr ; let F be Functor of C1,C2; attrF is covariant means :Def26: :: FUNCTOR0:def 26 ( F is Covariant & F is comp-preserving ); attrF is contravariant means :Def27: :: FUNCTOR0:def 27 ( F is Contravariant & F is comp-reversing ); end; :: deftheorem Def26 defines covariant FUNCTOR0:def_26_:_ for C1 being non empty transitive with_units AltCatStr for C2 being non empty with_units AltCatStr for F being Functor of C1,C2 holds ( F is covariant iff ( F is Covariant & F is comp-preserving ) ); :: deftheorem Def27 defines contravariant FUNCTOR0:def_27_:_ for C1 being non empty transitive with_units AltCatStr for C2 being non empty with_units AltCatStr for F being Functor of C1,C2 holds ( F is contravariant iff ( F is Contravariant & F is comp-reversing ) ); definition let A be AltCatStr ; let B be SubCatStr of A; func incl B -> strict FunctorStr over B,A means :Def28: :: FUNCTOR0:def 28 ( the ObjectMap of it = id [: the carrier of B, the carrier of B:] & the MorphMap of it = id the Arrows of B ); existence ex b1 being strict FunctorStr over B,A st ( the ObjectMap of b1 = id [: the carrier of B, the carrier of B:] & the MorphMap of b1 = id the Arrows of B ) proof the carrier of B c= the carrier of A by ALTCAT_2:def_11; then reconsider CC = [: the carrier of B, the carrier of B:] as Subset of [: the carrier of A, the carrier of A:] by ZFMISC_1:96; set OM = id [: the carrier of B, the carrier of B:]; id [: the carrier of B, the carrier of B:] = incl CC ; then reconsider OM = id [: the carrier of B, the carrier of B:] as bifunction of the carrier of B, the carrier of A ; set MM = id the Arrows of B; id the Arrows of B is MSUnTrans of OM, the Arrows of B, the Arrows of A proof percases ( [: the carrier of A, the carrier of A:] <> {} or [: the carrier of A, the carrier of A:] = {} ) ; :: according to FUNCTOR0:def_3 case [: the carrier of A, the carrier of A:] <> {} ; ::_thesis: ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of B, the carrier of B:],I29 st ( OM = f9 & the Arrows of A = B9 & id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 ) then reconsider I29 = [: the carrier of A, the carrier of A:] as non empty set ; reconsider B9 = the Arrows of A as ManySortedSet of I29 ; reconsider f9 = OM as Function of [: the carrier of B, the carrier of B:],I29 ; take I29 ; ::_thesis: ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of B, the carrier of B:],I29 st ( OM = f9 & the Arrows of A = B9 & id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 ) take B9 ; ::_thesis: ex f9 being Function of [: the carrier of B, the carrier of B:],I29 st ( OM = f9 & the Arrows of A = B9 & id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 ) take f9 ; ::_thesis: ( OM = f9 & the Arrows of A = B9 & id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 ) thus ( OM = f9 & the Arrows of A = B9 ) ; ::_thesis: id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 thus id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 ::_thesis: verum proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in [: the carrier of B, the carrier of B:] or (id the Arrows of B) . i is Element of bool [:( the Arrows of B . i),((B9 * f9) . i):] ) assume A1: i in [: the carrier of B, the carrier of B:] ; ::_thesis: (id the Arrows of B) . i is Element of bool [:( the Arrows of B . i),((B9 * f9) . i):] then A2: (id the Arrows of B) . i is Function of ( the Arrows of B . i),( the Arrows of B . i) by PBOOLE:def_15; A3: the Arrows of B cc= the Arrows of A by ALTCAT_2:def_11; (B9 * f9) . i = B9 . (f9 . i) by A1, FUNCT_2:15 .= the Arrows of A . i by A1, FUNCT_1:18 ; then the Arrows of B . i c= (B9 * f9) . i by A1, A3, ALTCAT_2:def_2; hence (id the Arrows of B) . i is Element of bool [:( the Arrows of B . i),((B9 * f9) . i):] by A2, FUNCT_2:7; ::_thesis: verum end; end; case [: the carrier of A, the carrier of A:] = {} ; ::_thesis: id the Arrows of B = [[0]] [: the carrier of B, the carrier of B:] then CC = {} ; hence id the Arrows of B = [[0]] [: the carrier of B, the carrier of B:] ; ::_thesis: verum end; end; end; then reconsider MM = id the Arrows of B as MSUnTrans of OM, the Arrows of B, the Arrows of A ; take FunctorStr(# OM,MM #) ; ::_thesis: ( the ObjectMap of FunctorStr(# OM,MM #) = id [: the carrier of B, the carrier of B:] & the MorphMap of FunctorStr(# OM,MM #) = id the Arrows of B ) thus ( the ObjectMap of FunctorStr(# OM,MM #) = id [: the carrier of B, the carrier of B:] & the MorphMap of FunctorStr(# OM,MM #) = id the Arrows of B ) ; ::_thesis: verum end; correctness uniqueness for b1, b2 being strict FunctorStr over B,A st the ObjectMap of b1 = id [: the carrier of B, the carrier of B:] & the MorphMap of b1 = id the Arrows of B & the ObjectMap of b2 = id [: the carrier of B, the carrier of B:] & the MorphMap of b2 = id the Arrows of B holds b1 = b2; ; end; :: deftheorem Def28 defines incl FUNCTOR0:def_28_:_ for A being AltCatStr for B being SubCatStr of A for b3 being strict FunctorStr over B,A holds ( b3 = incl B iff ( the ObjectMap of b3 = id [: the carrier of B, the carrier of B:] & the MorphMap of b3 = id the Arrows of B ) ); definition let A be AltGraph ; func id A -> strict FunctorStr over A,A means :Def29: :: FUNCTOR0:def 29 ( the ObjectMap of it = id [: the carrier of A, the carrier of A:] & the MorphMap of it = id the Arrows of A ); existence ex b1 being strict FunctorStr over A,A st ( the ObjectMap of b1 = id [: the carrier of A, the carrier of A:] & the MorphMap of b1 = id the Arrows of A ) proof reconsider OM = id [: the carrier of A, the carrier of A:] as bifunction of the carrier of A, the carrier of A ; set MM = id the Arrows of A; id the Arrows of A is MSUnTrans of OM, the Arrows of A, the Arrows of A proof percases ( [: the carrier of A, the carrier of A:] <> {} or [: the carrier of A, the carrier of A:] = {} ) ; :: according to FUNCTOR0:def_3 case [: the carrier of A, the carrier of A:] <> {} ; ::_thesis: ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of A, the carrier of A:],I29 st ( OM = f9 & the Arrows of A = B9 & id the Arrows of A is ManySortedFunction of the Arrows of A,B9 * f9 ) then reconsider I29 = [: the carrier of A, the carrier of A:] as non empty set ; reconsider A9 = the Arrows of A as ManySortedSet of I29 ; reconsider f9 = OM as Function of [: the carrier of A, the carrier of A:],I29 ; take I29 ; ::_thesis: ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of A, the carrier of A:],I29 st ( OM = f9 & the Arrows of A = B9 & id the Arrows of A is ManySortedFunction of the Arrows of A,B9 * f9 ) take A9 ; ::_thesis: ex f9 being Function of [: the carrier of A, the carrier of A:],I29 st ( OM = f9 & the Arrows of A = A9 & id the Arrows of A is ManySortedFunction of the Arrows of A,A9 * f9 ) take f9 ; ::_thesis: ( OM = f9 & the Arrows of A = A9 & id the Arrows of A is ManySortedFunction of the Arrows of A,A9 * f9 ) thus ( OM = f9 & the Arrows of A = A9 ) ; ::_thesis: id the Arrows of A is ManySortedFunction of the Arrows of A,A9 * f9 thus id the Arrows of A is ManySortedFunction of the Arrows of A,A9 * f9 ::_thesis: verum proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in [: the carrier of A, the carrier of A:] or (id the Arrows of A) . i is Element of bool [:( the Arrows of A . i),((A9 * f9) . i):] ) assume A1: i in [: the carrier of A, the carrier of A:] ; ::_thesis: (id the Arrows of A) . i is Element of bool [:( the Arrows of A . i),((A9 * f9) . i):] then (A9 * f9) . i = A9 . (f9 . i) by FUNCT_2:15 .= the Arrows of A . i by A1, FUNCT_1:18 ; hence (id the Arrows of A) . i is Element of bool [:( the Arrows of A . i),((A9 * f9) . i):] by A1, PBOOLE:def_15; ::_thesis: verum end; end; case [: the carrier of A, the carrier of A:] = {} ; ::_thesis: id the Arrows of A = [[0]] [: the carrier of A, the carrier of A:] hence id the Arrows of A = [[0]] [: the carrier of A, the carrier of A:] ; ::_thesis: verum end; end; end; then reconsider MM = id the Arrows of A as MSUnTrans of OM, the Arrows of A, the Arrows of A ; take FunctorStr(# OM,MM #) ; ::_thesis: ( the ObjectMap of FunctorStr(# OM,MM #) = id [: the carrier of A, the carrier of A:] & the MorphMap of FunctorStr(# OM,MM #) = id the Arrows of A ) thus ( the ObjectMap of FunctorStr(# OM,MM #) = id [: the carrier of A, the carrier of A:] & the MorphMap of FunctorStr(# OM,MM #) = id the Arrows of A ) ; ::_thesis: verum end; correctness uniqueness for b1, b2 being strict FunctorStr over A,A st the ObjectMap of b1 = id [: the carrier of A, the carrier of A:] & the MorphMap of b1 = id the Arrows of A & the ObjectMap of b2 = id [: the carrier of A, the carrier of A:] & the MorphMap of b2 = id the Arrows of A holds b1 = b2; ; end; :: deftheorem Def29 defines id FUNCTOR0:def_29_:_ for A being AltGraph for b2 being strict FunctorStr over A,A holds ( b2 = id A iff ( the ObjectMap of b2 = id [: the carrier of A, the carrier of A:] & the MorphMap of b2 = id the Arrows of A ) ); registration let A be AltCatStr ; let B be SubCatStr of A; cluster incl B -> strict Covariant ; coherence incl B is Covariant proof reconsider b = the carrier of B as Subset of A by ALTCAT_2:def_11; incl b = id b ; then reconsider f = id the carrier of B as Function of the carrier of B, the carrier of A ; take f ; :: according to FUNCTOR0:def_1,FUNCTOR0:def_12 ::_thesis: the ObjectMap of (incl B) = [:f,f:] thus the ObjectMap of (incl B) = id [: the carrier of B, the carrier of B:] by Def28 .= [:f,f:] by FUNCT_3:69 ; ::_thesis: verum end; end; theorem Th27: :: FUNCTOR0:27 for A being non empty AltCatStr for B being non empty SubCatStr of A for o being object of B holds (incl B) . o = o proof let A be non empty AltCatStr ; ::_thesis: for B being non empty SubCatStr of A for o being object of B holds (incl B) . o = o let B be non empty SubCatStr of A; ::_thesis: for o being object of B holds (incl B) . o = o let o be object of B; ::_thesis: (incl B) . o = o A1: [o,o] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; thus (incl B) . o = ((id [: the carrier of B, the carrier of B:]) . [o,o]) `1 by Def28 .= [o,o] `1 by A1, FUNCT_1:18 .= o ; ::_thesis: verum end; theorem Th28: :: FUNCTOR0:28 for A being non empty AltCatStr for B being non empty SubCatStr of A for o1, o2 being object of B holds <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^> proof let A be non empty AltCatStr ; ::_thesis: for B being non empty SubCatStr of A for o1, o2 being object of B holds <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^> let B be non empty SubCatStr of A; ::_thesis: for o1, o2 being object of B holds <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^> let o1, o2 be object of B; ::_thesis: <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^> A1: [o1,o2] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; A2: <^o1,o2^> = the Arrows of B . (o1,o2) by ALTCAT_1:def_1 .= the Arrows of B . [o1,o2] ; A3: (incl B) . o1 = o1 by Th27; (incl B) . o2 = o2 by Th27; then A4: <^((incl B) . o1),((incl B) . o2)^> = the Arrows of A . (o1,o2) by A3, ALTCAT_1:def_1 .= the Arrows of A . [o1,o2] ; the Arrows of B cc= the Arrows of A by ALTCAT_2:def_11; hence <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^> by A1, A2, A4, ALTCAT_2:def_2; ::_thesis: verum end; registration let A be non empty AltCatStr ; let B be non empty SubCatStr of A; cluster incl B -> feasible strict ; coherence incl B is feasible proof let o1, o2 be object of B; :: according to FUNCTOR0:def_18 ::_thesis: ( <^o1,o2^> <> {} implies <^((incl B) . o1),((incl B) . o2)^> <> {} ) thus ( <^o1,o2^> <> {} implies <^((incl B) . o1),((incl B) . o2)^> <> {} ) by Th28, XBOOLE_1:3; ::_thesis: verum end; end; definition let A, B be AltGraph ; let F be FunctorStr over A,B; attrF is faithful means :Def30: :: FUNCTOR0:def 30 the MorphMap of F is "1-1" ; end; :: deftheorem Def30 defines faithful FUNCTOR0:def_30_:_ for A, B being AltGraph for F being FunctorStr over A,B holds ( F is faithful iff the MorphMap of F is "1-1" ); definition let A, B be AltGraph ; let F be FunctorStr over A,B; attrF is full means :Def31: :: FUNCTOR0:def 31 ex B9 being ManySortedSet of [: the carrier of A, the carrier of A:] ex f being ManySortedFunction of the Arrows of A,B9 st ( B9 = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" ); end; :: deftheorem Def31 defines full FUNCTOR0:def_31_:_ for A, B being AltGraph for F being FunctorStr over A,B holds ( F is full iff ex B9 being ManySortedSet of [: the carrier of A, the carrier of A:] ex f being ManySortedFunction of the Arrows of A,B9 st ( B9 = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" ) ); definition let A be AltGraph ; let B be non empty AltGraph ; let F be FunctorStr over A,B; redefine attr F is full means :Def32: :: FUNCTOR0:def 32 ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & f is "onto" ); compatibility ( F is full iff ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & f is "onto" ) ) proof hereby ::_thesis: ( ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & f is "onto" ) implies F is full ) assume F is full ; ::_thesis: ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & f is "onto" ) then consider B9 being ManySortedSet of [: the carrier of A, the carrier of A:], f being ManySortedFunction of the Arrows of A,B9 such that A1: B9 = the Arrows of B * the ObjectMap of F and A2: f = the MorphMap of F and A3: f is "onto" by Def31; reconsider f = f as ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F by A1; take f = f; ::_thesis: ( f = the MorphMap of F & f is "onto" ) thus f = the MorphMap of F by A2; ::_thesis: f is "onto" thus f is "onto" by A1, A3; ::_thesis: verum end; given f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A4: f = the MorphMap of F and A5: f is "onto" ; ::_thesis: F is full take the Arrows of B * the ObjectMap of F ; :: according to FUNCTOR0:def_31 ::_thesis: ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( the Arrows of B * the ObjectMap of F = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" ) thus ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( the Arrows of B * the ObjectMap of F = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" ) by A4, A5; ::_thesis: verum end; end; :: deftheorem Def32 defines full FUNCTOR0:def_32_:_ for A being AltGraph for B being non empty AltGraph for F being FunctorStr over A,B holds ( F is full iff ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & f is "onto" ) ); definition let A, B be AltGraph ; let F be FunctorStr over A,B; attrF is injective means :Def33: :: FUNCTOR0:def 33 ( F is one-to-one & F is faithful ); attrF is surjective means :Def34: :: FUNCTOR0:def 34 ( F is full & F is onto ); end; :: deftheorem Def33 defines injective FUNCTOR0:def_33_:_ for A, B being AltGraph for F being FunctorStr over A,B holds ( F is injective iff ( F is one-to-one & F is faithful ) ); :: deftheorem Def34 defines surjective FUNCTOR0:def_34_:_ for A, B being AltGraph for F being FunctorStr over A,B holds ( F is surjective iff ( F is full & F is onto ) ); definition let A, B be AltGraph ; let F be FunctorStr over A,B; attrF is bijective means :Def35: :: FUNCTOR0:def 35 ( F is injective & F is surjective ); end; :: deftheorem Def35 defines bijective FUNCTOR0:def_35_:_ for A, B being AltGraph for F being FunctorStr over A,B holds ( F is bijective iff ( F is injective & F is surjective ) ); registration let A, B be non empty transitive with_units AltCatStr ; cluster feasible strict covariant contravariant for Functor of A,B; existence ex b1 being Functor of A,B st ( b1 is strict & b1 is covariant & b1 is contravariant & b1 is feasible ) proof set o = the object of B; reconsider F = A --> (idm the object of B) as Functor of A,B by Def25; take F ; ::_thesis: ( F is strict & F is covariant & F is contravariant & F is feasible ) thus ( F is strict & F is covariant & F is contravariant & F is feasible ) by Def26, Def27; ::_thesis: verum end; end; theorem Th29: :: FUNCTOR0:29 for A being non empty AltGraph for o being object of A holds (id A) . o = o proof let A be non empty AltGraph ; ::_thesis: for o being object of A holds (id A) . o = o let o be object of A; ::_thesis: (id A) . o = o A1: [o,o] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87; thus (id A) . o = ((id [: the carrier of A, the carrier of A:]) . [o,o]) `1 by Def29 .= [o,o] `1 by A1, FUNCT_1:18 .= o ; ::_thesis: verum end; theorem Th30: :: FUNCTOR0:30 for A being non empty AltGraph for o1, o2 being object of A st <^o1,o2^> <> {} holds for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m proof let A be non empty AltGraph ; ::_thesis: for o1, o2 being object of A st <^o1,o2^> <> {} holds for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m let o1, o2 be object of A; ::_thesis: ( <^o1,o2^> <> {} implies for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m ) assume A1: <^o1,o2^> <> {} ; ::_thesis: for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m let m be Morphism of o1,o2; ::_thesis: (Morph-Map ((id A),o1,o2)) . m = m A2: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87; Morph-Map ((id A),o1,o2) = (id the Arrows of A) . [o1,o2] by Def29; hence (Morph-Map ((id A),o1,o2)) . m = (id ( the Arrows of A . (o1,o2))) . m by A2, MSUALG_3:def_1 .= (id <^o1,o2^>) . m by ALTCAT_1:def_1 .= m by A1, FUNCT_1:18 ; ::_thesis: verum end; registration let A be non empty AltGraph ; cluster id A -> feasible strict Covariant ; coherence ( id A is feasible & id A is Covariant ) proof thus id A is feasible ::_thesis: id A is Covariant proof let o1, o2 be object of A; :: according to FUNCTOR0:def_11 ::_thesis: ( <^o1,o2^> <> {} implies the Arrows of A . ( the ObjectMap of (id A) . (o1,o2)) <> {} ) A1: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87; the ObjectMap of (id A) . (o1,o2) = (id [: the carrier of A, the carrier of A:]) . [o1,o2] by Def29 .= [o1,o2] by A1, FUNCT_1:18 ; then the Arrows of A . ( the ObjectMap of (id A) . (o1,o2)) = the Arrows of A . (o1,o2) .= <^o1,o2^> by ALTCAT_1:def_1 ; hence ( <^o1,o2^> <> {} implies the Arrows of A . ( the ObjectMap of (id A) . (o1,o2)) <> {} ) ; ::_thesis: verum end; thus id A is Covariant ::_thesis: verum proof take I = id the carrier of A; :: according to FUNCTOR0:def_1,FUNCTOR0:def_12 ::_thesis: the ObjectMap of (id A) = [:I,I:] thus the ObjectMap of (id A) = id [: the carrier of A, the carrier of A:] by Def29 .= [:I,I:] by FUNCT_3:69 ; ::_thesis: verum end; end; end; registration let A be non empty AltGraph ; cluster feasible Covariant for FunctorStr over A,A; existence ex b1 being FunctorStr over A,A st ( b1 is Covariant & b1 is feasible ) proof take id A ; ::_thesis: ( id A is Covariant & id A is feasible ) thus ( id A is Covariant & id A is feasible ) ; ::_thesis: verum end; end; theorem Th31: :: FUNCTOR0:31 for A being non empty AltGraph for o1, o2 being object of A st <^o1,o2^> <> {} holds for F being feasible Covariant FunctorStr over A,A st F = id A holds for m being Morphism of o1,o2 holds F . m = m proof let A be non empty AltGraph ; ::_thesis: for o1, o2 being object of A st <^o1,o2^> <> {} holds for F being feasible Covariant FunctorStr over A,A st F = id A holds for m being Morphism of o1,o2 holds F . m = m let o1, o2 be object of A; ::_thesis: ( <^o1,o2^> <> {} implies for F being feasible Covariant FunctorStr over A,A st F = id A holds for m being Morphism of o1,o2 holds F . m = m ) assume A1: <^o1,o2^> <> {} ; ::_thesis: for F being feasible Covariant FunctorStr over A,A st F = id A holds for m being Morphism of o1,o2 holds F . m = m let F be feasible Covariant FunctorStr over A,A; ::_thesis: ( F = id A implies for m being Morphism of o1,o2 holds F . m = m ) assume A2: F = id A ; ::_thesis: for m being Morphism of o1,o2 holds F . m = m let m be Morphism of o1,o2; ::_thesis: F . m = m <^(F . o1),(F . o2)^> <> {} by A1, Def18; hence F . m = (Morph-Map (F,o1,o2)) . m by A1, Def15 .= m by A1, A2, Th30 ; ::_thesis: verum end; registration let A be non empty transitive with_units AltCatStr ; cluster id A -> strict id-preserving comp-preserving ; coherence ( id A is id-preserving & id A is comp-preserving ) proof thus id A is id-preserving ::_thesis: id A is comp-preserving proof let o be object of A; :: according to FUNCTOR0:def_20 ::_thesis: (Morph-Map ((id A),o,o)) . (idm o) = idm ((id A) . o) <^o,o^> <> {} by ALTCAT_2:def_7; hence (Morph-Map ((id A),o,o)) . (idm o) = idm o by Th30 .= idm ((id A) . o) by Th29 ; ::_thesis: verum end; set F = id A; id A is comp-preserving proof let o1, o2, o3 be object of A; :: according to FUNCTOR0:def_23 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds (id A) . (g * f) = ((id A) . g) * ((id A) . f) ) assume that A1: <^o1,o2^> <> {} and A2: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds (id A) . (g * f) = ((id A) . g) * ((id A) . f) let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 holds (id A) . (g * f) = ((id A) . g) * ((id A) . f) let g be Morphism of o2,o3; ::_thesis: (id A) . (g * f) = ((id A) . g) * ((id A) . f) A3: <^o1,o3^> <> {} by A1, A2, ALTCAT_1:def_2; A4: (id A) . o1 = o1 by Th29; A5: (id A) . o2 = o2 by Th29; A6: (id A) . o3 = o3 by Th29; A7: (id A) . g = g by A2, Th31; (id A) . f = f by A1, Th31; hence (id A) . (g * f) = ((id A) . g) * ((id A) . f) by A3, A4, A5, A6, A7, Th31; ::_thesis: verum end; hence id A is comp-preserving ; ::_thesis: verum end; end; definition let A be non empty transitive with_units AltCatStr ; :: original: id redefine func id A -> strict covariant Functor of A,A; coherence id A is strict covariant Functor of A,A by Def25, Def26; end; registration let A be AltGraph ; cluster id A -> strict bijective ; coherence id A is bijective proof set CC = [: the carrier of A, the carrier of A:]; A1: the ObjectMap of (id A) = id [: the carrier of A, the carrier of A:] by Def29; hence id A is one-to-one by Def6; :: according to FUNCTOR0:def_33,FUNCTOR0:def_35 ::_thesis: ( id A is faithful & id A is surjective ) thus id A is faithful ::_thesis: id A is surjective proof percases ( the carrier of A <> {} or the carrier of A = {} ) ; supposeA2: the carrier of A <> {} ; ::_thesis: id A is faithful let i be set ; :: according to MSUALG_3:def_2,FUNCTOR0:def_30 ::_thesis: for b1 being set holds ( not i in proj1 the MorphMap of (id A) or not the MorphMap of (id A) . i = b1 or b1 is one-to-one ) let f be Function; ::_thesis: ( not i in proj1 the MorphMap of (id A) or not the MorphMap of (id A) . i = f or f is one-to-one ) assume that A3: i in dom the MorphMap of (id A) and A4: the MorphMap of (id A) . i = f ; ::_thesis: f is one-to-one consider o1, o2 being Element of A such that A5: i = [o1,o2] by A2, A3, DOMAIN_1:1; reconsider o1 = o1, o2 = o2 as object of A ; A6: [o1,o2] in [: the carrier of A, the carrier of A:] by A2, ZFMISC_1:87; f = (id the Arrows of A) . (o1,o2) by A4, A5, Def29 .= id ( the Arrows of A . [o1,o2]) by A6, MSUALG_3:def_1 ; hence f is one-to-one ; ::_thesis: verum end; supposeA7: the carrier of A = {} ; ::_thesis: id A is faithful let i be set ; :: according to MSUALG_3:def_2,FUNCTOR0:def_30 ::_thesis: for b1 being set holds ( not i in proj1 the MorphMap of (id A) or not the MorphMap of (id A) . i = b1 or b1 is one-to-one ) let f be Function; ::_thesis: ( not i in proj1 the MorphMap of (id A) or not the MorphMap of (id A) . i = f or f is one-to-one ) assume that A8: i in dom the MorphMap of (id A) and the MorphMap of (id A) . i = f ; ::_thesis: f is one-to-one dom the MorphMap of (id A) = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2 .= {} by A7, ZFMISC_1:90 ; hence f is one-to-one by A8; ::_thesis: verum end; end; end; thus id A is full :: according to FUNCTOR0:def_34 ::_thesis: id A is onto proof percases ( not A is empty or A is empty ) ; suppose not A is empty ; ::_thesis: id A is full then reconsider A = A as non empty AltGraph ; id A is full proof reconsider f = the MorphMap of (id A) as ManySortedFunction of the Arrows of A, the Arrows of A * the ObjectMap of (id A) by Def4; take f ; :: according to FUNCTOR0:def_32 ::_thesis: ( f = the MorphMap of (id A) & f is "onto" ) thus f = the MorphMap of (id A) ; ::_thesis: f is "onto" let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in [: the carrier of A, the carrier of A:] or proj2 (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i ) assume A9: i in [: the carrier of A, the carrier of A:] ; ::_thesis: proj2 (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i then consider o1, o2 being Element of A such that A10: i = [o1,o2] by DOMAIN_1:1; reconsider o1 = o1, o2 = o2 as object of A ; A11: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87; A12: dom the ObjectMap of (id A) = [: the carrier of A, the carrier of A:] by A1, RELAT_1:45; f . i = (id the Arrows of A) . (o1,o2) by A10, Def29 .= id ( the Arrows of A . [o1,o2]) by A11, MSUALG_3:def_1 ; hence rng (f . i) = the Arrows of A . [o1,o2] by RELAT_1:45 .= the Arrows of A . ( the ObjectMap of (id A) . i) by A1, A9, A10, FUNCT_1:18 .= ( the Arrows of A * the ObjectMap of (id A)) . i by A9, A12, FUNCT_1:13 ; ::_thesis: verum end; hence id A is full ; ::_thesis: verum end; suppose A is empty ; ::_thesis: id A is full then A13: the carrier of A = {} ; the ObjectMap of (id A) = id [: the carrier of A, the carrier of A:] by Def29; then reconsider B = the Arrows of A * the ObjectMap of (id A) as ManySortedSet of [: the carrier of A, the carrier of A:] by Th2; reconsider f = the MorphMap of (id A) as ManySortedSet of [: the carrier of A, the carrier of A:] ; f is ManySortedFunction of the Arrows of A,B proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in [: the carrier of A, the carrier of A:] or f . i is Element of bool [:( the Arrows of A . i),(B . i):] ) thus ( not i in [: the carrier of A, the carrier of A:] or f . i is Element of bool [:( the Arrows of A . i),(B . i):] ) by A13, ZFMISC_1:90; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the Arrows of A,B ; take B ; :: according to FUNCTOR0:def_31 ::_thesis: ex f being ManySortedFunction of the Arrows of A,B st ( B = the Arrows of A * the ObjectMap of (id A) & f = the MorphMap of (id A) & f is "onto" ) take f ; ::_thesis: ( B = the Arrows of A * the ObjectMap of (id A) & f = the MorphMap of (id A) & f is "onto" ) thus ( B = the Arrows of A * the ObjectMap of (id A) & f = the MorphMap of (id A) ) ; ::_thesis: f is "onto" let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in [: the carrier of A, the carrier of A:] or proj2 (f . i) = B . i ) thus ( not i in [: the carrier of A, the carrier of A:] or proj2 (f . i) = B . i ) by A13, ZFMISC_1:90; ::_thesis: verum end; end; end; rng (id [: the carrier of A, the carrier of A:]) = [: the carrier of A, the carrier of A:] ; then the ObjectMap of (id A) is onto by A1, FUNCT_2:def_3; hence id A is onto by Def7; ::_thesis: verum end; end; begin definition let C1 be non empty AltGraph ; let C2, C3 be non empty reflexive AltGraph ; let F be feasible FunctorStr over C1,C2; let G be FunctorStr over C2,C3; funcG * F -> strict FunctorStr over C1,C3 means :Def36: :: FUNCTOR0:def 36 ( the ObjectMap of it = the ObjectMap of G * the ObjectMap of F & the MorphMap of it = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F ); existence ex b1 being strict FunctorStr over C1,C3 st ( the ObjectMap of b1 = the ObjectMap of G * the ObjectMap of F & the MorphMap of b1 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F ) proof reconsider O = the ObjectMap of G * the ObjectMap of F as bifunction of the carrier of C1, the carrier of C3 ; set I1 = [: the carrier of C1, the carrier of C1:]; reconsider H = the MorphMap of G * the ObjectMap of F as MSUnTrans of O, the Arrows of C2 * the ObjectMap of F, the Arrows of C3 by Th17; for ii being set st ii in [: the carrier of C1, the carrier of C1:] & ( the Arrows of C2 * the ObjectMap of F) . ii = {} & not the Arrows of C1 . ii = {} holds ( the Arrows of C3 * O) . ii = {} proof let ii be set ; ::_thesis: ( ii in [: the carrier of C1, the carrier of C1:] & ( the Arrows of C2 * the ObjectMap of F) . ii = {} & not the Arrows of C1 . ii = {} implies ( the Arrows of C3 * O) . ii = {} ) assume that A1: ii in [: the carrier of C1, the carrier of C1:] and A2: ( the Arrows of C2 * the ObjectMap of F) . ii = {} ; ::_thesis: ( the Arrows of C1 . ii = {} or ( the Arrows of C3 * O) . ii = {} ) A3: dom the ObjectMap of F = [: the carrier of C1, the carrier of C1:] by FUNCT_2:def_1; reconsider o1 = ii `1 , o2 = ii `2 as object of C1 by A1, MCART_1:10; ii = [o1,o2] by A1, MCART_1:21; then A4: the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) = {} by A1, A2, A3, FUNCT_1:13; the Arrows of C1 . ii = the Arrows of C1 . (o1,o2) by A1, MCART_1:21 .= <^o1,o2^> by ALTCAT_1:def_1 .= {} by A4, Def11 ; hence ( the Arrows of C1 . ii = {} or ( the Arrows of C3 * O) . ii = {} ) ; ::_thesis: verum end; then reconsider M = H ** the MorphMap of F as MSUnTrans of O, the Arrows of C1, the Arrows of C3 by Th19; take FunctorStr(# O,M #) ; ::_thesis: ( the ObjectMap of FunctorStr(# O,M #) = the ObjectMap of G * the ObjectMap of F & the MorphMap of FunctorStr(# O,M #) = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F ) thus ( the ObjectMap of FunctorStr(# O,M #) = the ObjectMap of G * the ObjectMap of F & the MorphMap of FunctorStr(# O,M #) = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F ) ; ::_thesis: verum end; correctness uniqueness for b1, b2 being strict FunctorStr over C1,C3 st the ObjectMap of b1 = the ObjectMap of G * the ObjectMap of F & the MorphMap of b1 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F & the ObjectMap of b2 = the ObjectMap of G * the ObjectMap of F & the MorphMap of b2 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F holds b1 = b2; ; end; :: deftheorem Def36 defines * FUNCTOR0:def_36_:_ for C1 being non empty AltGraph for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 for b6 being strict FunctorStr over C1,C3 holds ( b6 = G * F iff ( the ObjectMap of b6 = the ObjectMap of G * the ObjectMap of F & the MorphMap of b6 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F ) ); registration let C1 be non empty AltGraph ; let C2, C3 be non empty reflexive AltGraph ; let F be feasible Covariant FunctorStr over C1,C2; let G be Covariant FunctorStr over C2,C3; clusterG * F -> strict Covariant ; correctness coherence G * F is Covariant ; proof the ObjectMap of F is Covariant by Def12; then consider f being Function of the carrier of C1, the carrier of C2 such that A1: the ObjectMap of F = [:f,f:] by Def1; the ObjectMap of G is Covariant by Def12; then consider g being Function of the carrier of C2, the carrier of C3 such that A2: the ObjectMap of G = [:g,g:] by Def1; take g * f ; :: according to FUNCTOR0:def_1,FUNCTOR0:def_12 ::_thesis: the ObjectMap of (G * F) = [:(g * f),(g * f):] thus the ObjectMap of (G * F) = the ObjectMap of G * the ObjectMap of F by Def36 .= [:(g * f),(g * f):] by A1, A2, FUNCT_3:71 ; ::_thesis: verum end; end; registration let C1 be non empty AltGraph ; let C2, C3 be non empty reflexive AltGraph ; let F be feasible Contravariant FunctorStr over C1,C2; let G be Covariant FunctorStr over C2,C3; clusterG * F -> strict Contravariant ; correctness coherence G * F is Contravariant ; proof the ObjectMap of F is Contravariant by Def13; then consider f being Function of the carrier of C1, the carrier of C2 such that A1: the ObjectMap of F = ~ [:f,f:] by Def2; the ObjectMap of G is Covariant by Def12; then consider g being Function of the carrier of C2, the carrier of C3 such that A2: the ObjectMap of G = [:g,g:] by Def1; take g * f ; :: according to FUNCTOR0:def_2,FUNCTOR0:def_13 ::_thesis: the ObjectMap of (G * F) = ~ [:(g * f),(g * f):] thus the ObjectMap of (G * F) = the ObjectMap of G * the ObjectMap of F by Def36 .= ~ ([:g,g:] * [:f,f:]) by A1, A2, ALTCAT_2:2 .= ~ [:(g * f),(g * f):] by FUNCT_3:71 ; ::_thesis: verum end; end; registration let C1 be non empty AltGraph ; let C2, C3 be non empty reflexive AltGraph ; let F be feasible Covariant FunctorStr over C1,C2; let G be Contravariant FunctorStr over C2,C3; clusterG * F -> strict Contravariant ; correctness coherence G * F is Contravariant ; proof the ObjectMap of F is Covariant by Def12; then consider f being Function of the carrier of C1, the carrier of C2 such that A1: the ObjectMap of F = [:f,f:] by Def1; the ObjectMap of G is Contravariant by Def13; then consider g being Function of the carrier of C2, the carrier of C3 such that A2: the ObjectMap of G = ~ [:g,g:] by Def2; take g * f ; :: according to FUNCTOR0:def_2,FUNCTOR0:def_13 ::_thesis: the ObjectMap of (G * F) = ~ [:(g * f),(g * f):] thus the ObjectMap of (G * F) = the ObjectMap of G * the ObjectMap of F by Def36 .= ~ ([:g,g:] * [:f,f:]) by A1, A2, ALTCAT_2:3 .= ~ [:(g * f),(g * f):] by FUNCT_3:71 ; ::_thesis: verum end; end; registration let C1 be non empty AltGraph ; let C2, C3 be non empty reflexive AltGraph ; let F be feasible Contravariant FunctorStr over C1,C2; let G be Contravariant FunctorStr over C2,C3; clusterG * F -> strict Covariant ; correctness coherence G * F is Covariant ; proof the ObjectMap of F is Contravariant by Def13; then consider f being Function of the carrier of C1, the carrier of C2 such that A1: the ObjectMap of F = ~ [:f,f:] by Def2; the ObjectMap of G is Contravariant by Def13; then consider g being Function of the carrier of C2, the carrier of C3 such that A2: the ObjectMap of G = ~ [:g,g:] by Def2; take g * f ; :: according to FUNCTOR0:def_1,FUNCTOR0:def_12 ::_thesis: the ObjectMap of (G * F) = [:(g * f),(g * f):] thus the ObjectMap of (G * F) = the ObjectMap of G * the ObjectMap of F by Def36 .= ~ ((~ [:g,g:]) * [:f,f:]) by A1, A2, ALTCAT_2:2 .= ~ (~ ([:g,g:] * [:f,f:])) by ALTCAT_2:3 .= [:g,g:] * [:f,f:] by FUNCT_4:53 .= [:(g * f),(g * f):] by FUNCT_3:71 ; ::_thesis: verum end; end; registration let C1 be non empty AltGraph ; let C2, C3 be non empty reflexive AltGraph ; let F be feasible FunctorStr over C1,C2; let G be feasible FunctorStr over C2,C3; clusterG * F -> feasible strict ; coherence G * F is feasible proof let o1, o2 be object of C1; :: according to FUNCTOR0:def_11 ::_thesis: ( <^o1,o2^> <> {} implies the Arrows of C3 . ( the ObjectMap of (G * F) . (o1,o2)) <> {} ) assume A1: <^o1,o2^> <> {} ; ::_thesis: the Arrows of C3 . ( the ObjectMap of (G * F) . (o1,o2)) <> {} reconsider p1 = ( the ObjectMap of F . (o1,o2)) `1 , p2 = ( the ObjectMap of F . (o1,o2)) `2 as Element of C2 by MCART_1:10; reconsider p1 = p1, p2 = p2 as object of C2 ; [o1,o2] in [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87; then A2: [o1,o2] in dom the ObjectMap of F by FUNCT_2:def_1; A3: the ObjectMap of F . (o1,o2) = [p1,p2] by MCART_1:21; A4: the ObjectMap of (G * F) . (o1,o2) = ( the ObjectMap of G * the ObjectMap of F) . [o1,o2] by Def36 .= the ObjectMap of G . (p1,p2) by A2, A3, FUNCT_1:13 ; <^p1,p2^> = the Arrows of C2 . (p1,p2) by ALTCAT_1:def_1 .= the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) by MCART_1:21 ; then <^p1,p2^> <> {} by A1, Def11; hence the Arrows of C3 . ( the ObjectMap of (G * F) . (o1,o2)) <> {} by A4, Def11; ::_thesis: verum end; end; theorem :: FUNCTOR0:32 for C1 being non empty AltGraph for C2, C3, C4 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being feasible FunctorStr over C2,C3 for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F) proof let C1 be non empty AltGraph ; ::_thesis: for C2, C3, C4 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being feasible FunctorStr over C2,C3 for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F) let C2, C3, C4 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2 for G being feasible FunctorStr over C2,C3 for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F) let F be feasible FunctorStr over C1,C2; ::_thesis: for G being feasible FunctorStr over C2,C3 for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F) let G be feasible FunctorStr over C2,C3; ::_thesis: for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F) let H be FunctorStr over C3,C4; ::_thesis: (H * G) * F = H * (G * F) A1: the ObjectMap of ((H * G) * F) = the ObjectMap of (H * G) * the ObjectMap of F by Def36 .= ( the ObjectMap of H * the ObjectMap of G) * the ObjectMap of F by Def36 .= the ObjectMap of H * ( the ObjectMap of G * the ObjectMap of F) by RELAT_1:36 .= the ObjectMap of H * the ObjectMap of (G * F) by Def36 .= the ObjectMap of (H * (G * F)) by Def36 ; the MorphMap of ((H * G) * F) = ( the MorphMap of (H * G) * the ObjectMap of F) ** the MorphMap of F by Def36 .= ((( the MorphMap of H * the ObjectMap of G) ** the MorphMap of G) * the ObjectMap of F) ** the MorphMap of F by Def36 .= ((( the MorphMap of H * the ObjectMap of G) * the ObjectMap of F) ** ( the MorphMap of G * the ObjectMap of F)) ** the MorphMap of F by Th12 .= (( the MorphMap of H * ( the ObjectMap of G * the ObjectMap of F)) ** ( the MorphMap of G * the ObjectMap of F)) ** the MorphMap of F by RELAT_1:36 .= (( the MorphMap of H * the ObjectMap of (G * F)) ** ( the MorphMap of G * the ObjectMap of F)) ** the MorphMap of F by Def36 .= ( the MorphMap of H * the ObjectMap of (G * F)) ** (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) by PBOOLE:140 .= ( the MorphMap of H * the ObjectMap of (G * F)) ** the MorphMap of (G * F) by Def36 .= the MorphMap of (H * (G * F)) by Def36 ; hence (H * G) * F = H * (G * F) by A1; ::_thesis: verum end; theorem Th33: :: FUNCTOR0:33 for C1 being non empty AltCatStr for C2, C3 being non empty reflexive AltCatStr for F being reflexive feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 for o being object of C1 holds (G * F) . o = G . (F . o) proof let C1 be non empty AltCatStr ; ::_thesis: for C2, C3 being non empty reflexive AltCatStr for F being reflexive feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 for o being object of C1 holds (G * F) . o = G . (F . o) let C2, C3 be non empty reflexive AltCatStr ; ::_thesis: for F being reflexive feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 for o being object of C1 holds (G * F) . o = G . (F . o) let F be reflexive feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 for o being object of C1 holds (G * F) . o = G . (F . o) let G be FunctorStr over C2,C3; ::_thesis: for o being object of C1 holds (G * F) . o = G . (F . o) let o be object of C1; ::_thesis: (G * F) . o = G . (F . o) dom the ObjectMap of F = [: the carrier of C1, the carrier of C1:] by FUNCT_2:def_1; then A1: [o,o] in dom the ObjectMap of F by ZFMISC_1:87; thus (G * F) . o = (( the ObjectMap of G * the ObjectMap of F) . (o,o)) `1 by Def36 .= ( the ObjectMap of G . ( the ObjectMap of F . [o,o])) `1 by A1, FUNCT_1:13 .= G . (F . o) by Def10 ; ::_thesis: verum end; theorem Th34: :: FUNCTOR0:34 for C1 being non empty AltGraph for C2, C3 being non empty reflexive AltGraph for F being reflexive feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 for o being object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o)) proof let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph for F being reflexive feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 for o being object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o)) let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being reflexive feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 for o being object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o)) let F be reflexive feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 for o being object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o)) let G be FunctorStr over C2,C3; ::_thesis: for o being object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o)) let o be object of C1; ::_thesis: Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o)) A1: dom the MorphMap of G = [: the carrier of C2, the carrier of C2:] by PARTFUN1:def_2; rng the ObjectMap of F c= [: the carrier of C2, the carrier of C2:] ; then dom ( the MorphMap of G * the ObjectMap of F) = dom the ObjectMap of F by A1, RELAT_1:27 .= [: the carrier of C1, the carrier of C1:] by FUNCT_2:def_1 ; then A2: [o,o] in dom ( the MorphMap of G * the ObjectMap of F) by ZFMISC_1:87; dom the MorphMap of F = [: the carrier of C1, the carrier of C1:] by PARTFUN1:def_2; then [o,o] in dom the MorphMap of F by ZFMISC_1:87; then [o,o] in (dom ( the MorphMap of G * the ObjectMap of F)) /\ (dom the MorphMap of F) by A2, XBOOLE_0:def_4; then A3: [o,o] in dom (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) by PBOOLE:def_19; A4: ( the MorphMap of G * the ObjectMap of F) . [o,o] = the MorphMap of G . ( the ObjectMap of F . (o,o)) by A2, FUNCT_1:12 .= Morph-Map (G,(F . o),(F . o)) by Def10 ; thus Morph-Map ((G * F),o,o) = (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o,o) by Def36 .= (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o)) by A3, A4, PBOOLE:def_19 ; ::_thesis: verum end; registration let C1, C2, C3 be non empty with_units AltCatStr ; let F be reflexive feasible id-preserving FunctorStr over C1,C2; let G be id-preserving FunctorStr over C2,C3; clusterG * F -> strict id-preserving ; coherence G * F is id-preserving proof let o be object of C1; :: according to FUNCTOR0:def_20 ::_thesis: (Morph-Map ((G * F),o,o)) . (idm o) = idm ((G * F) . o) A1: [o,o] in [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87; then [o,o] in dom the ObjectMap of F by FUNCT_2:def_1; then ( the Arrows of C2 * the ObjectMap of F) . [o,o] = the Arrows of C2 . ( the ObjectMap of F . (o,o)) by FUNCT_1:13 .= the Arrows of C2 . ((F . o),(F . o)) by Def10 .= <^(F . o),(F . o)^> by ALTCAT_1:def_1 ; then A2: ( the Arrows of C2 * the ObjectMap of F) . [o,o] <> {} by ALTCAT_2:def_7; the MorphMap of F is ManySortedFunction of the Arrows of C1, the Arrows of C2 * the ObjectMap of F by Def4; then Morph-Map (F,o,o) is Function of ( the Arrows of C1 . [o,o]),(( the Arrows of C2 * the ObjectMap of F) . [o,o]) by A1, PBOOLE:def_15; then A3: dom (Morph-Map (F,o,o)) = the Arrows of C1 . (o,o) by A2, FUNCT_2:def_1 .= <^o,o^> by ALTCAT_1:def_1 ; thus (Morph-Map ((G * F),o,o)) . (idm o) = ((Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))) . (idm o) by Th34 .= (Morph-Map (G,(F . o),(F . o))) . ((Morph-Map (F,o,o)) . (idm o)) by A3, ALTCAT_1:19, FUNCT_1:13 .= (Morph-Map (G,(F . o),(F . o))) . (idm (F . o)) by Def20 .= idm (G . (F . o)) by Def20 .= idm ((G * F) . o) by Th33 ; ::_thesis: verum end; end; definition let A, C be non empty reflexive AltCatStr ; let B be non empty SubCatStr of A; let F be FunctorStr over A,C; funcF | B -> FunctorStr over B,C equals :: FUNCTOR0:def 37 F * (incl B); correctness coherence F * (incl B) is FunctorStr over B,C; ; end; :: deftheorem defines | FUNCTOR0:def_37_:_ for A, C being non empty reflexive AltCatStr for B being non empty SubCatStr of A for F being FunctorStr over A,C holds F | B = F * (incl B); begin definition let A, B be non empty AltGraph ; let F be FunctorStr over A,B; assume A1: F is bijective ; funcF " -> strict FunctorStr over B,A means :Def38: :: FUNCTOR0:def 38 ( the ObjectMap of it = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & the MorphMap of it = (f "") * ( the ObjectMap of F ") ) ); existence ex b1 being strict FunctorStr over B,A st ( the ObjectMap of b1 = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & the MorphMap of b1 = (f "") * ( the ObjectMap of F ") ) ) proof set OF = the ObjectMap of F; F is injective by A1, Def35; then F is one-to-one by Def33; then A2: the ObjectMap of F is one-to-one by Def6; F is surjective by A1, Def35; then F is onto by Def34; then the ObjectMap of F is onto by Def7; then A3: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] by FUNCT_2:def_3; then reconsider OM = the ObjectMap of F " as bifunction of the carrier of B, the carrier of A by A2, FUNCT_2:25; reconsider f = the MorphMap of F as ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F by Def4; ( the Arrows of B * the ObjectMap of F) * OM = the Arrows of B * ( the ObjectMap of F * OM) by RELAT_1:36 .= the Arrows of B * (id [: the carrier of B, the carrier of B:]) by A2, A3, FUNCT_2:29 .= the Arrows of B by Th2 ; then (f "") * OM is ManySortedFunction of the Arrows of B, the Arrows of A * OM by ALTCAT_2:5; then reconsider MM = (f "") * OM as MSUnTrans of OM, the Arrows of B, the Arrows of A by Def4; take G = FunctorStr(# OM,MM #); ::_thesis: ( the ObjectMap of G = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & the MorphMap of G = (f "") * ( the ObjectMap of F ") ) ) thus the ObjectMap of G = the ObjectMap of F " ; ::_thesis: ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & the MorphMap of G = (f "") * ( the ObjectMap of F ") ) take f ; ::_thesis: ( f = the MorphMap of F & the MorphMap of G = (f "") * ( the ObjectMap of F ") ) thus ( f = the MorphMap of F & the MorphMap of G = (f "") * ( the ObjectMap of F ") ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict FunctorStr over B,A st the ObjectMap of b1 = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & the MorphMap of b1 = (f "") * ( the ObjectMap of F ") ) & the ObjectMap of b2 = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & the MorphMap of b2 = (f "") * ( the ObjectMap of F ") ) holds b1 = b2 ; end; :: deftheorem Def38 defines " FUNCTOR0:def_38_:_ for A, B being non empty AltGraph for F being FunctorStr over A,B st F is bijective holds for b4 being strict FunctorStr over B,A holds ( b4 = F " iff ( the ObjectMap of b4 = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & the MorphMap of b4 = (f "") * ( the ObjectMap of F ") ) ) ); theorem Th35: :: FUNCTOR0:35 for A, B being non empty transitive with_units AltCatStr for F being feasible FunctorStr over A,B st F is bijective holds ( F " is bijective & F " is feasible ) proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being feasible FunctorStr over A,B st F is bijective holds ( F " is bijective & F " is feasible ) let F be feasible FunctorStr over A,B; ::_thesis: ( F is bijective implies ( F " is bijective & F " is feasible ) ) assume A1: F is bijective ; ::_thesis: ( F " is bijective & F " is feasible ) set G = F " ; A2: the ObjectMap of (F ") = the ObjectMap of F " by A1, Def38; A3: F is injective by A1, Def35; then F is one-to-one by Def33; then A4: the ObjectMap of F is one-to-one by Def6; hence the ObjectMap of (F ") is one-to-one by A2; :: according to FUNCTOR0:def_6,FUNCTOR0:def_33,FUNCTOR0:def_35 ::_thesis: ( F " is faithful & F " is surjective & F " is feasible ) F is faithful by A3, Def33; then A5: the MorphMap of F is "1-1" by Def30; A6: F is surjective by A1, Def35; then F is onto by Def34; then A7: the ObjectMap of F is onto by Def7; consider h being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A8: h = the MorphMap of F and A9: the MorphMap of (F ") = (h "") * ( the ObjectMap of F ") by A1, Def38; F is full by A6, Def34; then A10: ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & f is "onto" ) by Def32; set AA = [: the carrier of A, the carrier of A:]; set BB = [: the carrier of B, the carrier of B:]; A11: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] by A7, FUNCT_2:def_3; reconsider f = the MorphMap of (F ") as ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4; f is "1-1" proof let i be set ; :: according to MSUALG_3:def_2 ::_thesis: for b1 being set holds ( not i in proj1 f or not f . i = b1 or b1 is one-to-one ) let g be Function; ::_thesis: ( not i in proj1 f or not f . i = g or g is one-to-one ) assume that A12: i in dom f and A13: f . i = g ; ::_thesis: g is one-to-one i in [: the carrier of B, the carrier of B:] by A12; then A14: i in dom ( the ObjectMap of F ") by A4, A11, FUNCT_1:33; then ( the ObjectMap of F ") . i in rng ( the ObjectMap of F ") by FUNCT_1:def_3; then A15: ( the ObjectMap of F ") . i in dom the ObjectMap of F by A4, FUNCT_1:33; then ( the ObjectMap of F ") . i in [: the carrier of A, the carrier of A:] ; then ( the ObjectMap of F ") . i in dom h by PARTFUN1:def_2; then A16: h . (( the ObjectMap of F ") . i) is one-to-one by A5, A8, MSUALG_3:def_2; g = (h "") . (( the ObjectMap of F ") . i) by A9, A13, A14, FUNCT_1:13 .= (h . (( the ObjectMap of F ") . i)) " by A5, A8, A10, A15, MSUALG_3:def_4 ; hence g is one-to-one by A16; ::_thesis: verum end; hence the MorphMap of (F ") is "1-1" ; :: according to FUNCTOR0:def_30 ::_thesis: ( F " is surjective & F " is feasible ) thus F " is full :: according to FUNCTOR0:def_34 ::_thesis: ( F " is onto & F " is feasible ) proof take f ; :: according to FUNCTOR0:def_32 ::_thesis: ( f = the MorphMap of (F ") & f is "onto" ) thus f = the MorphMap of (F ") ; ::_thesis: f is "onto" let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in [: the carrier of B, the carrier of B:] or proj2 (f . i) = ( the Arrows of A * the ObjectMap of (F ")) . i ) assume A17: i in [: the carrier of B, the carrier of B:] ; ::_thesis: proj2 (f . i) = ( the Arrows of A * the ObjectMap of (F ")) . i then A18: i in dom the ObjectMap of (F ") by FUNCT_2:def_1; A19: i in dom ( the ObjectMap of F ") by A4, A11, A17, FUNCT_1:33; then ( the ObjectMap of F ") . i in rng ( the ObjectMap of F ") by FUNCT_1:def_3; then A20: ( the ObjectMap of F ") . i in dom the ObjectMap of F by A4, FUNCT_1:33; then ( the ObjectMap of F ") . i in [: the carrier of A, the carrier of A:] ; then the ObjectMap of (F ") . i in dom h by A2, PARTFUN1:def_2; then A21: h . ( the ObjectMap of (F ") . i) is one-to-one by A5, A8, MSUALG_3:def_2; set j = the ObjectMap of (F ") . i; A22: h . ( the ObjectMap of (F ") . i) is Function of ( the Arrows of A . ( the ObjectMap of (F ") . i)),(( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of (F ") . i)) by A2, A20, PBOOLE:def_15; consider o1, o2 being Element of A such that A23: the ObjectMap of (F ") . i = [o1,o2] by A2, A20, DOMAIN_1:1; reconsider o1 = o1, o2 = o2 as object of A ; A24: now__::_thesis:_(_the_Arrows_of_A_._(_the_ObjectMap_of_(F_")_._i)_<>_{}_implies_(_the_Arrows_of_B_*_the_ObjectMap_of_F)_._(_the_ObjectMap_of_(F_")_._i)_<>_{}_) assume the Arrows of A . ( the ObjectMap of (F ") . i) <> {} ; ::_thesis: ( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of (F ") . i) <> {} then the Arrows of A . (o1,o2) <> {} by A23; then <^o1,o2^> <> {} by ALTCAT_1:def_1; then the Arrows of B . ( the ObjectMap of F . (o1,o2)) <> {} by Def11; hence ( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of (F ") . i) <> {} by A2, A20, A23, FUNCT_1:13; ::_thesis: verum end; f . i = (h "") . (( the ObjectMap of F ") . i) by A9, A19, FUNCT_1:13 .= (h . (( the ObjectMap of F ") . i)) " by A5, A8, A10, A20, MSUALG_3:def_4 ; hence rng (f . i) = dom (h . ( the ObjectMap of (F ") . i)) by A2, A21, FUNCT_1:33 .= the Arrows of A . ( the ObjectMap of (F ") . i) by A22, A24, FUNCT_2:def_1 .= ( the Arrows of A * the ObjectMap of (F ")) . i by A18, FUNCT_1:13 ; ::_thesis: verum end; thus rng the ObjectMap of (F ") = dom the ObjectMap of F by A2, A4, FUNCT_1:33 .= [: the carrier of A, the carrier of A:] by FUNCT_2:def_1 ; :: according to FUNCT_2:def_3,FUNCTOR0:def_7 ::_thesis: F " is feasible let o1, o2 be object of B; :: according to FUNCTOR0:def_11 ::_thesis: ( <^o1,o2^> <> {} implies the Arrows of A . ( the ObjectMap of (F ") . (o1,o2)) <> {} ) assume <^o1,o2^> <> {} ; ::_thesis: the Arrows of A . ( the ObjectMap of (F ") . (o1,o2)) <> {} then A25: the Arrows of B . (o1,o2) <> {} by ALTCAT_1:def_1; A26: [o1,o2] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; then consider p1, p2 being Element of A such that A27: the ObjectMap of (F ") . [o1,o2] = [p1,p2] by DOMAIN_1:1, FUNCT_2:5; reconsider p1 = p1, p2 = p2 as object of A ; [o1,o2] in dom the ObjectMap of (F ") by A26, FUNCT_2:def_1; then A28: the ObjectMap of F . (p1,p2) = ( the ObjectMap of F * the ObjectMap of (F ")) . [o1,o2] by A27, FUNCT_1:13 .= (id [: the carrier of B, the carrier of B:]) . [o1,o2] by A2, A4, A11, FUNCT_1:39 .= [o1,o2] by A26, FUNCT_1:18 ; assume A29: the Arrows of A . ( the ObjectMap of (F ") . (o1,o2)) = {} ; ::_thesis: contradiction A30: [p1,p2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87; then A31: [p1,p2] in dom the ObjectMap of F by FUNCT_2:def_1; h . [p1,p2] is Function of ( the Arrows of A . [p1,p2]),(( the Arrows of B * the ObjectMap of F) . [p1,p2]) by A30, PBOOLE:def_15; then {} = rng (h . [p1,p2]) by A27, A29 .= ( the Arrows of B * the ObjectMap of F) . [p1,p2] by A8, A10, A30, MSUALG_3:def_3 .= the Arrows of B . [o1,o2] by A28, A31, FUNCT_1:13 ; hence contradiction by A25; ::_thesis: verum end; theorem Th36: :: FUNCTOR0:36 for A, B being non empty transitive with_units AltCatStr for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive holds F " is reflexive proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive holds F " is reflexive let F be reflexive feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is coreflexive implies F " is reflexive ) assume that A1: F is bijective and A2: F is coreflexive ; ::_thesis: F " is reflexive set G = F " ; A3: the ObjectMap of (F ") = the ObjectMap of F " by A1, Def38; let o be object of B; :: according to FUNCTOR0:def_10 ::_thesis: the ObjectMap of (F ") . (o,o) = [((F ") . o),((F ") . o)] A4: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def_1; consider p being object of A such that A5: o = F . p by A2, Th20; F is injective by A1, Def35; then F is one-to-one by Def33; then A6: the ObjectMap of F is one-to-one by Def6; A7: [p,p] in dom the ObjectMap of F by A4, ZFMISC_1:87; A8: (F ") . (F . p) = ((F ") * F) . p by Th33 .= (( the ObjectMap of (F ") * the ObjectMap of F) . (p,p)) `1 by Def36 .= ((id (dom the ObjectMap of F)) . [p,p]) `1 by A3, A6, FUNCT_1:39 .= [p,p] `1 by A7, FUNCT_1:18 .= p ; thus the ObjectMap of (F ") . (o,o) = the ObjectMap of (F ") . ( the ObjectMap of F . (p,p)) by A5, Def10 .= ( the ObjectMap of (F ") * the ObjectMap of F) . [p,p] by A7, FUNCT_1:13 .= (id (dom the ObjectMap of F)) . [p,p] by A3, A6, FUNCT_1:39 .= [((F ") . o),((F ") . o)] by A5, A7, A8, FUNCT_1:18 ; ::_thesis: verum end; theorem Th37: :: FUNCTOR0:37 for A, B being non empty transitive with_units AltCatStr for F being reflexive feasible id-preserving FunctorStr over A,B st F is bijective & F is coreflexive holds F " is id-preserving proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being reflexive feasible id-preserving FunctorStr over A,B st F is bijective & F is coreflexive holds F " is id-preserving let F be reflexive feasible id-preserving FunctorStr over A,B; ::_thesis: ( F is bijective & F is coreflexive implies F " is id-preserving ) assume A1: ( F is bijective & F is coreflexive ) ; ::_thesis: F " is id-preserving set G = F " ; reconsider H = F " as reflexive feasible FunctorStr over B,A by A1, Th35, Th36; A2: the ObjectMap of (F ") = the ObjectMap of F " by A1, Def38; consider f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A3: f = the MorphMap of F and A4: the MorphMap of (F ") = (f "") * ( the ObjectMap of F ") by A1, Def38; let o be object of B; :: according to FUNCTOR0:def_20 ::_thesis: (Morph-Map ((F "),o,o)) . (idm o) = idm ((F ") . o) A5: F is injective by A1, Def35; then F is one-to-one by Def33; then A6: the ObjectMap of F is one-to-one by Def6; F is faithful by A5, Def33; then A7: the MorphMap of F is "1-1" by Def30; F is surjective by A1, Def35; then F is full by Def34; then A8: ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & f is "onto" ) by Def32; A9: [((F ") . o),((F ") . o)] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87; A10: [o,o] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; then A11: [o,o] in dom the ObjectMap of (F ") by FUNCT_2:def_1; A12: the ObjectMap of (F * H) . (o,o) = ( the ObjectMap of F * the ObjectMap of H) . [o,o] by Def36 .= ( the ObjectMap of F * ( the ObjectMap of F ")) . [o,o] by A1, Def38 .= (id (rng the ObjectMap of F)) . [o,o] by A6, FUNCT_1:39 .= (id (dom the ObjectMap of (F "))) . [o,o] by A2, A6, FUNCT_1:33 .= (id [: the carrier of B, the carrier of B:]) . [o,o] by FUNCT_2:def_1 .= [o,o] by A10, FUNCT_1:18 ; A13: F . ((F ") . o) = (F * H) . o by Th33 .= o by A12, MCART_1:7 ; dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2; then [((F ") . o),((F ") . o)] in dom the MorphMap of F by ZFMISC_1:87; then A14: Morph-Map (F,((F ") . o),((F ") . o)) is one-to-one by A7, MSUALG_3:def_2; [((F ") . o),((F ") . o)] in dom the ObjectMap of F by A9, FUNCT_2:def_1; then ( the Arrows of B * the ObjectMap of F) . [((F ") . o),((F ") . o)] = the Arrows of B . ( the ObjectMap of F . (((F ") . o),((F ") . o))) by FUNCT_1:13 .= the Arrows of B . ((F . ((F ") . o)),(F . ((F ") . o))) by Def10 ; then A15: ( the Arrows of B * the ObjectMap of F) . [((F ") . o),((F ") . o)] <> {} by ALTCAT_2:def_6; Morph-Map (F,((F ") . o),((F ") . o)) is Function of ( the Arrows of A . [((F ") . o),((F ") . o)]),(( the Arrows of B * the ObjectMap of F) . [((F ") . o),((F ") . o)]) by A3, A9, PBOOLE:def_15; then A16: dom (Morph-Map (F,((F ") . o),((F ") . o))) = the Arrows of A . (((F ") . o),((F ") . o)) by A15, FUNCT_2:def_1 .= <^((F ") . o),((F ") . o)^> by ALTCAT_1:def_1 ; ( the Arrows of A * the ObjectMap of (F ")) . [o,o] = the Arrows of A . ( the ObjectMap of H . (o,o)) by A11, FUNCT_1:13 .= the Arrows of A . (((F ") . o),((F ") . o)) by Def10 ; then A17: ( the Arrows of A * the ObjectMap of (F ")) . [o,o] <> {} by ALTCAT_2:def_6; the MorphMap of (F ") is ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4; then Morph-Map ((F "),o,o) is Function of ( the Arrows of B . [o,o]),(( the Arrows of A * the ObjectMap of (F ")) . [o,o]) by A10, PBOOLE:def_15; then A18: dom (Morph-Map ((F "),o,o)) = the Arrows of B . (o,o) by A17, FUNCT_2:def_1 .= <^o,o^> by ALTCAT_1:def_1 ; then A19: idm o in dom (Morph-Map ((F "),o,o)) by ALTCAT_1:19; A20: Morph-Map ((F "),o,o) = (f "") . ( the ObjectMap of (F ") . (o,o)) by A2, A4, A11, FUNCT_1:13 .= (f "") . [(H . o),(H . o)] by Def10 .= (Morph-Map (F,((F ") . o),((F ") . o))) " by A3, A7, A8, A9, MSUALG_3:def_4 ; (Morph-Map ((F "),o,o)) . (idm o) in rng (Morph-Map ((F "),o,o)) by A19, FUNCT_1:def_3; then A21: (Morph-Map ((F "),o,o)) . (idm o) in dom (Morph-Map (F,((F ") . o),((F ") . o))) by A14, A20, FUNCT_1:33; (Morph-Map (F,((F ") . o),((F ") . o))) . ((Morph-Map ((F "),o,o)) . (idm o)) = ((Morph-Map (F,((F ") . o),((F ") . o))) * (Morph-Map ((F "),o,o))) . (idm o) by A18, ALTCAT_1:19, FUNCT_1:13 .= (id (rng (Morph-Map (F,((F ") . o),((F ") . o))))) . (idm o) by A14, A20, FUNCT_1:39 .= (id (dom (Morph-Map ((F "),o,o)))) . (idm o) by A14, A20, FUNCT_1:33 .= idm (F . ((F ") . o)) by A13, A18, ALTCAT_1:19, FUNCT_1:18 .= (Morph-Map (F,((F ") . o),((F ") . o))) . (idm ((F ") . o)) by Def20 ; hence (Morph-Map ((F "),o,o)) . (idm o) = idm ((F ") . o) by A14, A16, A21, FUNCT_1:def_4; ::_thesis: verum end; theorem Th38: :: FUNCTOR0:38 for A, B being non empty transitive with_units AltCatStr for F being feasible FunctorStr over A,B st F is bijective & F is Covariant holds F " is Covariant proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being feasible FunctorStr over A,B st F is bijective & F is Covariant holds F " is Covariant let F be feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is Covariant implies F " is Covariant ) assume A1: ( F is bijective & F is Covariant ) ; ::_thesis: F " is Covariant then F is injective by Def35; then F is one-to-one by Def33; then A2: the ObjectMap of F is one-to-one by Def6; F is surjective by A1, Def35; then F is onto by Def34; then A3: the ObjectMap of F is onto by Def7; the ObjectMap of F is Covariant by A1, Def12; then consider f being Function of the carrier of A, the carrier of B such that A4: the ObjectMap of F = [:f,f:] by Def1; A5: f is one-to-one by A2, A4, Th7; then A6: dom (f ") = rng f by FUNCT_1:33; A7: rng (f ") = dom f by A5, FUNCT_1:33; A8: rng [:f,f:] = [: the carrier of B, the carrier of B:] by A3, A4, FUNCT_2:def_3; rng [:f,f:] = [:(rng f),(rng f):] by FUNCT_3:67; then rng f = the carrier of B by A8, ZFMISC_1:92; then reconsider g = f " as Function of the carrier of B, the carrier of A by A6, A7, FUNCT_2:def_1, RELSET_1:4; take g ; :: according to FUNCTOR0:def_1,FUNCTOR0:def_12 ::_thesis: the ObjectMap of (F ") = [:g,g:] [:f,f:] " = [:g,g:] by A5, Th6; hence the ObjectMap of (F ") = [:g,g:] by A1, A4, Def38; ::_thesis: verum end; theorem Th39: :: FUNCTOR0:39 for A, B being non empty transitive with_units AltCatStr for F being feasible FunctorStr over A,B st F is bijective & F is Contravariant holds F " is Contravariant proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being feasible FunctorStr over A,B st F is bijective & F is Contravariant holds F " is Contravariant let F be feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is Contravariant implies F " is Contravariant ) assume A1: ( F is bijective & F is Contravariant ) ; ::_thesis: F " is Contravariant then F is injective by Def35; then F is one-to-one by Def33; then A2: the ObjectMap of F is one-to-one by Def6; F is surjective by A1, Def35; then F is onto by Def34; then A3: the ObjectMap of F is onto by Def7; the ObjectMap of F is Contravariant by A1, Def13; then consider f being Function of the carrier of A, the carrier of B such that A4: the ObjectMap of F = ~ [:f,f:] by Def2; [:f,f:] is one-to-one by A2, A4, Th9; then A5: f is one-to-one by Th7; then A6: dom (f ") = rng f by FUNCT_1:33; A7: rng (f ") = dom f by A5, FUNCT_1:33; [:f,f:] is onto by A3, A4, Th13; then A8: rng [:f,f:] = [: the carrier of B, the carrier of B:] by FUNCT_2:def_3; rng [:f,f:] = [:(rng f),(rng f):] by FUNCT_3:67; then rng f = the carrier of B by A8, ZFMISC_1:92; then reconsider g = f " as Function of the carrier of B, the carrier of A by A6, A7, FUNCT_2:def_1, RELSET_1:4; take g ; :: according to FUNCTOR0:def_2,FUNCTOR0:def_13 ::_thesis: the ObjectMap of (F ") = ~ [:g,g:] A9: [:f,f:] " = [:g,g:] by A5, Th6; thus the ObjectMap of (F ") = the ObjectMap of F " by A1, Def38 .= ~ [:g,g:] by A4, A5, A9, Th10 ; ::_thesis: verum end; theorem Th40: :: FUNCTOR0:40 for A, B being non empty transitive with_units AltCatStr for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Covariant holds for o1, o2 being object of B for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Covariant holds for o1, o2 being object of B for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m let F be reflexive feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is coreflexive & F is Covariant implies for o1, o2 being object of B for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m ) assume A1: ( F is bijective & F is coreflexive & F is Covariant ) ; ::_thesis: for o1, o2 being object of B for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m set G = F " ; A2: F " is Covariant by A1, Th38; reconsider H = F " as reflexive feasible FunctorStr over B,A by A1, Th35, Th36; A3: the ObjectMap of (F ") = the ObjectMap of F " by A1, Def38; consider f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A4: f = the MorphMap of F and A5: the MorphMap of (F ") = (f "") * ( the ObjectMap of F ") by A1, Def38; F is injective by A1, Def35; then F is faithful by Def33; then A6: the MorphMap of F is "1-1" by Def30; F is surjective by A1, Def35; then F is full by Def34; then A7: ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & f is "onto" ) by Def32; let o1, o2 be object of B; ::_thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m let m be Morphism of o1,o2; ::_thesis: ( <^o1,o2^> <> {} implies (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m ) assume A8: <^o1,o2^> <> {} ; ::_thesis: (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m A9: [((F ") . o1),((F ") . o2)] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87; A10: [o1,o2] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; then A11: [o1,o2] in dom the ObjectMap of (F ") by FUNCT_2:def_1; dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2; then [((F ") . o1),((F ") . o2)] in dom the MorphMap of F by ZFMISC_1:87; then A12: Morph-Map (F,((F ") . o1),((F ") . o2)) is one-to-one by A6, MSUALG_3:def_2; ( the Arrows of A * the ObjectMap of (F ")) . [o1,o2] = the Arrows of A . ( the ObjectMap of H . (o1,o2)) by A11, FUNCT_1:13 .= the Arrows of A . ((H . o1),(H . o2)) by A2, Th22 .= <^(H . o1),(H . o2)^> by ALTCAT_1:def_1 ; then A13: ( the Arrows of A * the ObjectMap of (F ")) . [o1,o2] <> {} by A2, A8, Def18; the MorphMap of (F ") is ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4; then Morph-Map ((F "),o1,o2) is Function of ( the Arrows of B . [o1,o2]),(( the Arrows of A * the ObjectMap of (F ")) . [o1,o2]) by A10, PBOOLE:def_15; then A14: dom (Morph-Map ((F "),o1,o2)) = the Arrows of B . (o1,o2) by A13, FUNCT_2:def_1 .= <^o1,o2^> by ALTCAT_1:def_1 ; A15: Morph-Map ((F "),o1,o2) = (f "") . ( the ObjectMap of (F ") . (o1,o2)) by A3, A5, A11, FUNCT_1:13 .= (f "") . [(H . o1),(H . o2)] by A2, Th22 .= (Morph-Map (F,((F ") . o1),((F ") . o2))) " by A4, A6, A7, A9, MSUALG_3:def_4 ; thus (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = ((Morph-Map (F,((F ") . o1),((F ") . o2))) * (Morph-Map ((F "),o1,o2))) . m by A8, A14, FUNCT_1:13 .= (id (rng (Morph-Map (F,((F ") . o1),((F ") . o2))))) . m by A12, A15, FUNCT_1:39 .= (id (dom (Morph-Map ((F "),o1,o2)))) . m by A12, A15, FUNCT_1:33 .= m by A8, A14, FUNCT_1:18 ; ::_thesis: verum end; theorem Th41: :: FUNCTOR0:41 for A, B being non empty transitive with_units AltCatStr for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Contravariant holds for o1, o2 being object of B for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Contravariant holds for o1, o2 being object of B for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m let F be reflexive feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is coreflexive & F is Contravariant implies for o1, o2 being object of B for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m ) assume A1: ( F is bijective & F is coreflexive & F is Contravariant ) ; ::_thesis: for o1, o2 being object of B for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m set G = F " ; A2: F " is Contravariant by A1, Th39; reconsider H = F " as reflexive feasible FunctorStr over B,A by A1, Th35, Th36; A3: the ObjectMap of (F ") = the ObjectMap of F " by A1, Def38; consider f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A4: f = the MorphMap of F and A5: the MorphMap of (F ") = (f "") * ( the ObjectMap of F ") by A1, Def38; F is injective by A1, Def35; then F is faithful by Def33; then A6: the MorphMap of F is "1-1" by Def30; F is surjective by A1, Def35; then F is full by Def34; then A7: ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & f is "onto" ) by Def32; let o1, o2 be object of B; ::_thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds (Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m let m be Morphism of o1,o2; ::_thesis: ( <^o1,o2^> <> {} implies (Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m ) assume A8: <^o1,o2^> <> {} ; ::_thesis: (Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m A9: [((F ") . o2),((F ") . o1)] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87; A10: [o1,o2] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; then A11: [o1,o2] in dom the ObjectMap of (F ") by FUNCT_2:def_1; dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2; then [((F ") . o2),((F ") . o1)] in dom the MorphMap of F by ZFMISC_1:87; then A12: Morph-Map (F,((F ") . o2),((F ") . o1)) is one-to-one by A6, MSUALG_3:def_2; ( the Arrows of A * the ObjectMap of (F ")) . [o1,o2] = the Arrows of A . ( the ObjectMap of H . (o1,o2)) by A11, FUNCT_1:13 .= the Arrows of A . ((H . o2),(H . o1)) by A2, Th23 .= <^(H . o2),(H . o1)^> by ALTCAT_1:def_1 ; then A13: ( the Arrows of A * the ObjectMap of (F ")) . [o1,o2] <> {} by A2, A8, Def19; the MorphMap of (F ") is ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4; then Morph-Map ((F "),o1,o2) is Function of ( the Arrows of B . [o1,o2]),(( the Arrows of A * the ObjectMap of (F ")) . [o1,o2]) by A10, PBOOLE:def_15; then A14: dom (Morph-Map ((F "),o1,o2)) = the Arrows of B . (o1,o2) by A13, FUNCT_2:def_1 .= <^o1,o2^> by ALTCAT_1:def_1 ; A15: Morph-Map ((F "),o1,o2) = (f "") . ( the ObjectMap of (F ") . (o1,o2)) by A3, A5, A11, FUNCT_1:13 .= (f "") . [(H . o2),(H . o1)] by A2, Th23 .= (Morph-Map (F,((F ") . o2),((F ") . o1))) " by A4, A6, A7, A9, MSUALG_3:def_4 ; thus (Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = ((Morph-Map (F,((F ") . o2),((F ") . o1))) * (Morph-Map ((F "),o1,o2))) . m by A8, A14, FUNCT_1:13 .= (id (rng (Morph-Map (F,((F ") . o2),((F ") . o1))))) . m by A12, A15, FUNCT_1:39 .= (id (dom (Morph-Map ((F "),o1,o2)))) . m by A12, A15, FUNCT_1:33 .= m by A8, A14, FUNCT_1:18 ; ::_thesis: verum end; theorem Th42: :: FUNCTOR0:42 for A, B being non empty transitive with_units AltCatStr for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-preserving & F is Covariant & F is coreflexive holds F " is comp-preserving proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-preserving & F is Covariant & F is coreflexive holds F " is comp-preserving let F be reflexive feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is comp-preserving & F is Covariant & F is coreflexive implies F " is comp-preserving ) assume A1: ( F is bijective & F is comp-preserving & F is Covariant & F is coreflexive ) ; ::_thesis: F " is comp-preserving set G = F " ; A2: F " is Covariant by A1, Th38; reconsider H = F " as reflexive feasible FunctorStr over B,A by A1, Th35, Th36; A3: the ObjectMap of (F ") = the ObjectMap of F " by A1, Def38; consider ff being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A4: ff = the MorphMap of F and A5: the MorphMap of (F ") = (ff "") * ( the ObjectMap of F ") by A1, Def38; A6: F is injective by A1, Def35; then F is one-to-one by Def33; then A7: the ObjectMap of F is one-to-one by Def6; F is faithful by A6, Def33; then A8: the MorphMap of F is "1-1" by Def30; F is surjective by A1, Def35; then F is full by Def34; then A9: ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & f is "onto" ) by Def32; let o1, o2, o3 be object of B; :: according to FUNCTOR0:def_21 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex g9 being Morphism of ((F ") . o2),((F ") . o3) st ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 ) ) assume A10: <^o1,o2^> <> {} ; ::_thesis: ( not <^o2,o3^> <> {} or for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex g9 being Morphism of ((F ") . o2),((F ") . o3) st ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 ) ) then A11: <^(H . o1),(H . o2)^> <> {} by A2, Def18; assume A12: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex g9 being Morphism of ((F ") . o2),((F ") . o3) st ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 ) then A13: <^(H . o2),(H . o3)^> <> {} by A2, Def18; A14: <^o1,o3^> <> {} by A10, A12, ALTCAT_1:def_2; then A15: <^(H . o1),(H . o3)^> <> {} by A2, Def18; then A16: <^(F . ((F ") . o1)),(F . ((F ") . o3))^> <> {} by A1, Def18; let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex g9 being Morphism of ((F ") . o2),((F ") . o3) st ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 ) let g be Morphism of o2,o3; ::_thesis: ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex g9 being Morphism of ((F ") . o2),((F ") . o3) st ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 ) reconsider K = F " as Covariant FunctorStr over B,A by A1, Th38; K . f = (Morph-Map (K,o1,o2)) . f by A10, A11, Def15; then reconsider f9 = (Morph-Map (K,o1,o2)) . f as Morphism of ((F ") . o1),((F ") . o2) ; K . g = (Morph-Map (K,o2,o3)) . g by A12, A13, Def15; then reconsider g9 = (Morph-Map (K,o2,o3)) . g as Morphism of ((F ") . o2),((F ") . o3) ; take f9 ; ::_thesis: ex g9 being Morphism of ((F ") . o2),((F ") . o3) st ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 ) take g9 ; ::_thesis: ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 ) thus f9 = (Morph-Map ((F "),o1,o2)) . f ; ::_thesis: ( g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 ) thus g9 = (Morph-Map ((F "),o2,o3)) . g ; ::_thesis: (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 consider f99 being Morphism of (F . ((F ") . o1)),(F . ((F ") . o2)), g99 being Morphism of (F . ((F ") . o2)),(F . ((F ") . o3)) such that A17: f99 = (Morph-Map (F,((F ") . o1),((F ") . o2))) . f9 and A18: g99 = (Morph-Map (F,((F ") . o2),((F ") . o3))) . g9 and A19: (Morph-Map (F,((F ") . o1),((F ") . o3))) . (g9 * f9) = g99 * f99 by A1, A11, A13, Def21; A20: g = g99 by A1, A12, A18, Th40; A21: f = f99 by A1, A10, A17, Th40; A22: [((F ") . o1),((F ") . o3)] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87; A23: [o1,o3] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; then A24: [o1,o3] in dom the ObjectMap of (F ") by FUNCT_2:def_1; dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2; then [((F ") . o1),((F ") . o3)] in dom the MorphMap of F by ZFMISC_1:87; then A25: Morph-Map (F,((F ") . o1),((F ") . o3)) is one-to-one by A8, MSUALG_3:def_2; [((F ") . o1),((F ") . o3)] in dom the ObjectMap of F by A22, FUNCT_2:def_1; then A26: ( the Arrows of B * the ObjectMap of F) . [((F ") . o1),((F ") . o3)] = the Arrows of B . ( the ObjectMap of F . (((F ") . o1),((F ") . o3))) by FUNCT_1:13 .= the Arrows of B . ((F . ((F ") . o1)),(F . ((F ") . o3))) by A1, Th22 .= <^(F . ((F ") . o1)),(F . ((F ") . o3))^> by ALTCAT_1:def_1 ; Morph-Map (F,((F ") . o1),((F ") . o3)) is Function of ( the Arrows of A . [((F ") . o1),((F ") . o3)]),(( the Arrows of B * the ObjectMap of F) . [((F ") . o1),((F ") . o3)]) by A4, A22, PBOOLE:def_15; then A27: dom (Morph-Map (F,((F ") . o1),((F ") . o3))) = the Arrows of A . (((F ") . o1),((F ") . o3)) by A16, A26, FUNCT_2:def_1 .= <^((F ") . o1),((F ") . o3)^> by ALTCAT_1:def_1 ; A28: ( the Arrows of A * the ObjectMap of (F ")) . [o1,o3] = the Arrows of A . ( the ObjectMap of H . (o1,o3)) by A24, FUNCT_1:13 .= the Arrows of A . (((F ") . o1),((F ") . o3)) by A2, Th22 .= <^((F ") . o1),((F ") . o3)^> by ALTCAT_1:def_1 ; the MorphMap of (F ") is ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4; then Morph-Map ((F "),o1,o3) is Function of ( the Arrows of B . [o1,o3]),(( the Arrows of A * the ObjectMap of (F ")) . [o1,o3]) by A23, PBOOLE:def_15; then A29: dom (Morph-Map ((F "),o1,o3)) = the Arrows of B . (o1,o3) by A15, A28, FUNCT_2:def_1 .= <^o1,o3^> by ALTCAT_1:def_1 ; A30: Morph-Map ((F "),o1,o3) = (ff "") . ( the ObjectMap of (F ") . (o1,o3)) by A3, A5, A24, FUNCT_1:13 .= (ff "") . [(H . o1),(H . o3)] by A2, Th22 .= (Morph-Map (F,((F ") . o1),((F ") . o3))) " by A4, A8, A9, A22, MSUALG_3:def_4 ; A31: the ObjectMap of (F * H) = the ObjectMap of F * the ObjectMap of H by Def36 .= the ObjectMap of F * ( the ObjectMap of F ") by A1, Def38 .= id (rng the ObjectMap of F) by A7, FUNCT_1:39 .= id (dom the ObjectMap of (F ")) by A3, A7, FUNCT_1:33 .= id [: the carrier of B, the carrier of B:] by FUNCT_2:def_1 ; [o1,o1] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; then A32: the ObjectMap of (F * H) . (o1,o1) = [o1,o1] by A31, FUNCT_1:18; A33: F . ((F ") . o1) = (F * H) . o1 by Th33 .= o1 by A32, MCART_1:7 ; [o2,o2] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; then A34: the ObjectMap of (F * H) . (o2,o2) = [o2,o2] by A31, FUNCT_1:18; A35: F . ((F ") . o2) = (F * H) . o2 by Th33 .= o2 by A34, MCART_1:7 ; [o3,o3] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; then A36: the ObjectMap of (F * H) . (o3,o3) = [o3,o3] by A31, FUNCT_1:18; A37: F . ((F ") . o3) = (F * H) . o3 by Th33 .= o3 by A36, MCART_1:7 ; (Morph-Map ((F "),o1,o3)) . (g * f) in rng (Morph-Map ((F "),o1,o3)) by A14, A29, FUNCT_1:def_3; then A38: (Morph-Map ((F "),o1,o3)) . (g * f) in dom (Morph-Map (F,((F ") . o1),((F ") . o3))) by A25, A30, FUNCT_1:33; (Morph-Map (F,((F ") . o1),((F ") . o3))) . ((Morph-Map ((F "),o1,o3)) . (g * f)) = (Morph-Map (F,((F ") . o1),((F ") . o3))) . (g9 * f9) by A1, A14, A19, A20, A21, A33, A35, A37, Th40; hence (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 by A25, A27, A38, FUNCT_1:def_4; ::_thesis: verum end; theorem Th43: :: FUNCTOR0:43 for A, B being non empty transitive with_units AltCatStr for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive holds F " is comp-reversing proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive holds F " is comp-reversing let F be reflexive feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive implies F " is comp-reversing ) assume A1: ( F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive ) ; ::_thesis: F " is comp-reversing set G = F " ; A2: F " is Contravariant by A1, Th39; reconsider H = F " as reflexive feasible FunctorStr over B,A by A1, Th35, Th36; A3: the ObjectMap of (F ") = the ObjectMap of F " by A1, Def38; consider ff being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A4: ff = the MorphMap of F and A5: the MorphMap of (F ") = (ff "") * ( the ObjectMap of F ") by A1, Def38; A6: F is injective by A1, Def35; then F is one-to-one by Def33; then A7: the ObjectMap of F is one-to-one by Def6; F is faithful by A6, Def33; then A8: the MorphMap of F is "1-1" by Def30; F is surjective by A1, Def35; then F is full by Def34; then A9: ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( f = the MorphMap of F & f is "onto" ) by Def32; let o1, o2, o3 be object of B; :: according to FUNCTOR0:def_22 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o2),((F ") . o1) ex g9 being Morphism of ((F ") . o3),((F ") . o2) st ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9 ) ) assume A10: <^o1,o2^> <> {} ; ::_thesis: ( not <^o2,o3^> <> {} or for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o2),((F ") . o1) ex g9 being Morphism of ((F ") . o3),((F ") . o2) st ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9 ) ) then A11: <^(H . o2),(H . o1)^> <> {} by A2, Def19; assume A12: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2 for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o2),((F ") . o1) ex g9 being Morphism of ((F ") . o3),((F ") . o2) st ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9 ) then A13: <^(H . o3),(H . o2)^> <> {} by A2, Def19; A14: <^o1,o3^> <> {} by A10, A12, ALTCAT_1:def_2; then A15: <^(H . o3),(H . o1)^> <> {} by A2, Def19; then A16: <^(F . ((F ") . o1)),(F . ((F ") . o3))^> <> {} by A1, Def19; let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o2),((F ") . o1) ex g9 being Morphism of ((F ") . o3),((F ") . o2) st ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9 ) let g be Morphism of o2,o3; ::_thesis: ex f9 being Morphism of ((F ") . o2),((F ") . o1) ex g9 being Morphism of ((F ") . o3),((F ") . o2) st ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9 ) reconsider K = F " as Contravariant FunctorStr over B,A by A1, Th39; K . f = (Morph-Map (K,o1,o2)) . f by A10, A11, Def16; then reconsider f9 = (Morph-Map (K,o1,o2)) . f as Morphism of ((F ") . o2),((F ") . o1) ; K . g = (Morph-Map (K,o2,o3)) . g by A12, A13, Def16; then reconsider g9 = (Morph-Map (K,o2,o3)) . g as Morphism of ((F ") . o3),((F ") . o2) ; take f9 ; ::_thesis: ex g9 being Morphism of ((F ") . o3),((F ") . o2) st ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9 ) take g9 ; ::_thesis: ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9 ) thus f9 = (Morph-Map ((F "),o1,o2)) . f ; ::_thesis: ( g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9 ) thus g9 = (Morph-Map ((F "),o2,o3)) . g ; ::_thesis: (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9 consider g99 being Morphism of (F . ((F ") . o2)),(F . ((F ") . o3)), f99 being Morphism of (F . ((F ") . o1)),(F . ((F ") . o2)) such that A17: g99 = (Morph-Map (F,((F ") . o3),((F ") . o2))) . g9 and A18: f99 = (Morph-Map (F,((F ") . o2),((F ") . o1))) . f9 and A19: (Morph-Map (F,((F ") . o3),((F ") . o1))) . (f9 * g9) = g99 * f99 by A1, A11, A13, Def22; A20: g = g99 by A1, A12, A17, Th41; A21: f = f99 by A1, A10, A18, Th41; A22: [((F ") . o3),((F ") . o1)] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87; A23: [o1,o3] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; then A24: [o1,o3] in dom the ObjectMap of (F ") by FUNCT_2:def_1; dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2; then [((F ") . o3),((F ") . o1)] in dom the MorphMap of F by ZFMISC_1:87; then A25: Morph-Map (F,((F ") . o3),((F ") . o1)) is one-to-one by A8, MSUALG_3:def_2; [((F ") . o3),((F ") . o1)] in dom the ObjectMap of F by A22, FUNCT_2:def_1; then A26: ( the Arrows of B * the ObjectMap of F) . [((F ") . o3),((F ") . o1)] = the Arrows of B . ( the ObjectMap of F . (((F ") . o3),((F ") . o1))) by FUNCT_1:13 .= the Arrows of B . ((F . ((F ") . o1)),(F . ((F ") . o3))) by A1, Th23 .= <^(F . ((F ") . o1)),(F . ((F ") . o3))^> by ALTCAT_1:def_1 ; Morph-Map (F,((F ") . o3),((F ") . o1)) is Function of ( the Arrows of A . [((F ") . o3),((F ") . o1)]),(( the Arrows of B * the ObjectMap of F) . [((F ") . o3),((F ") . o1)]) by A4, A22, PBOOLE:def_15; then A27: dom (Morph-Map (F,((F ") . o3),((F ") . o1))) = the Arrows of A . (((F ") . o3),((F ") . o1)) by A16, A26, FUNCT_2:def_1 .= <^((F ") . o3),((F ") . o1)^> by ALTCAT_1:def_1 ; A28: ( the Arrows of A * the ObjectMap of (F ")) . [o1,o3] = the Arrows of A . ( the ObjectMap of H . (o1,o3)) by A24, FUNCT_1:13 .= the Arrows of A . (((F ") . o3),((F ") . o1)) by A2, Th23 .= <^((F ") . o3),((F ") . o1)^> by ALTCAT_1:def_1 ; the MorphMap of (F ") is ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4; then Morph-Map ((F "),o1,o3) is Function of ( the Arrows of B . [o1,o3]),(( the Arrows of A * the ObjectMap of (F ")) . [o1,o3]) by A23, PBOOLE:def_15; then A29: dom (Morph-Map ((F "),o1,o3)) = the Arrows of B . (o1,o3) by A15, A28, FUNCT_2:def_1 .= <^o1,o3^> by ALTCAT_1:def_1 ; A30: Morph-Map ((F "),o1,o3) = (ff "") . ( the ObjectMap of (F ") . (o1,o3)) by A3, A5, A24, FUNCT_1:13 .= (ff "") . [(H . o3),(H . o1)] by A2, Th23 .= (Morph-Map (F,((F ") . o3),((F ") . o1))) " by A4, A8, A9, A22, MSUALG_3:def_4 ; A31: the ObjectMap of (F * H) = the ObjectMap of F * the ObjectMap of H by Def36 .= the ObjectMap of F * ( the ObjectMap of F ") by A1, Def38 .= id (rng the ObjectMap of F) by A7, FUNCT_1:39 .= id (dom the ObjectMap of (F ")) by A3, A7, FUNCT_1:33 .= id [: the carrier of B, the carrier of B:] by FUNCT_2:def_1 ; [o1,o1] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; then A32: the ObjectMap of (F * H) . (o1,o1) = [o1,o1] by A31, FUNCT_1:18; A33: F . ((F ") . o1) = (F * H) . o1 by Th33 .= o1 by A32, MCART_1:7 ; [o2,o2] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; then A34: the ObjectMap of (F * H) . (o2,o2) = [o2,o2] by A31, FUNCT_1:18; A35: F . ((F ") . o2) = (F * H) . o2 by Th33 .= o2 by A34, MCART_1:7 ; [o3,o3] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87; then A36: the ObjectMap of (F * H) . (o3,o3) = [o3,o3] by A31, FUNCT_1:18; A37: F . ((F ") . o3) = (F * H) . o3 by Th33 .= o3 by A36, MCART_1:7 ; (Morph-Map ((F "),o1,o3)) . (g * f) in rng (Morph-Map ((F "),o1,o3)) by A14, A29, FUNCT_1:def_3; then A38: (Morph-Map ((F "),o1,o3)) . (g * f) in dom (Morph-Map (F,((F ") . o3),((F ") . o1))) by A25, A30, FUNCT_1:33; (Morph-Map (F,((F ") . o3),((F ") . o1))) . ((Morph-Map ((F "),o1,o3)) . (g * f)) = (Morph-Map (F,((F ") . o3),((F ") . o1))) . (f9 * g9) by A1, A14, A19, A20, A21, A33, A35, A37, Th41; hence (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9 by A25, A27, A38, FUNCT_1:def_4; ::_thesis: verum end; registration let C1 be 1-sorted ; let C2 be non empty 1-sorted ; cluster Covariant -> reflexive for BimapStr over C1,C2; coherence for b1 being BimapStr over C1,C2 st b1 is Covariant holds b1 is reflexive proof let M be BimapStr over C1,C2; ::_thesis: ( M is Covariant implies M is reflexive ) assume M is Covariant ; ::_thesis: M is reflexive then the ObjectMap of M is Covariant by Def12; then ex f being Function of the carrier of C1, the carrier of C2 st the ObjectMap of M = [:f,f:] by Def1; hence the ObjectMap of M .: (id the carrier of C1) c= id the carrier of C2 by Th14; :: according to FUNCTOR0:def_8 ::_thesis: verum end; end; registration let C1 be 1-sorted ; let C2 be non empty 1-sorted ; cluster Contravariant -> reflexive for BimapStr over C1,C2; coherence for b1 being BimapStr over C1,C2 st b1 is Contravariant holds b1 is reflexive proof let M be BimapStr over C1,C2; ::_thesis: ( M is Contravariant implies M is reflexive ) assume M is Contravariant ; ::_thesis: M is reflexive then the ObjectMap of M is Contravariant by Def13; then consider f being Function of the carrier of C1, the carrier of C2 such that A1: the ObjectMap of M = ~ [:f,f:] by Def2; (~ [:f,f:]) .: (id the carrier of C1) = [:f,f:] .: (id the carrier of C1) by Th3; hence the ObjectMap of M .: (id the carrier of C1) c= id the carrier of C2 by A1, Th14; :: according to FUNCTOR0:def_8 ::_thesis: verum end; end; theorem Th44: :: FUNCTOR0:44 for C1, C2 being 1-sorted for M being BimapStr over C1,C2 st M is Covariant & M is onto holds M is coreflexive proof let C1, C2 be 1-sorted ; ::_thesis: for M being BimapStr over C1,C2 st M is Covariant & M is onto holds M is coreflexive let M be BimapStr over C1,C2; ::_thesis: ( M is Covariant & M is onto implies M is coreflexive ) assume A1: ( M is Covariant & M is onto ) ; ::_thesis: M is coreflexive then the ObjectMap of M is Covariant by Def12; then consider f being Function of the carrier of C1, the carrier of C2 such that A2: the ObjectMap of M = [:f,f:] by Def1; the ObjectMap of M is onto by A1, Def7; then f is onto by A2, Th4; hence id the carrier of C2 c= the ObjectMap of M .: (id the carrier of C1) by A2, Th11; :: according to FUNCTOR0:def_9 ::_thesis: verum end; theorem Th45: :: FUNCTOR0:45 for C1, C2 being 1-sorted for M being BimapStr over C1,C2 st M is Contravariant & M is onto holds M is coreflexive proof let C1, C2 be 1-sorted ; ::_thesis: for M being BimapStr over C1,C2 st M is Contravariant & M is onto holds M is coreflexive let M be BimapStr over C1,C2; ::_thesis: ( M is Contravariant & M is onto implies M is coreflexive ) assume A1: ( M is Contravariant & M is onto ) ; ::_thesis: M is coreflexive then the ObjectMap of M is Contravariant by Def13; then consider f being Function of the carrier of C1, the carrier of C2 such that A2: the ObjectMap of M = ~ [:f,f:] by Def2; the ObjectMap of M is onto by A1, Def7; then [:f,f:] is onto by A2, Th13; then A3: f is onto by Th4; the ObjectMap of M .: (id the carrier of C1) = [:f,f:] .: (id the carrier of C1) by A2, Th3; hence id the carrier of C2 c= the ObjectMap of M .: (id the carrier of C1) by A3, Th11; :: according to FUNCTOR0:def_9 ::_thesis: verum end; registration let C1 be non empty transitive with_units AltCatStr ; let C2 be non empty with_units AltCatStr ; cluster covariant -> reflexive for Functor of C1,C2; coherence for b1 being Functor of C1,C2 st b1 is covariant holds b1 is reflexive proof let F be Functor of C1,C2; ::_thesis: ( F is covariant implies F is reflexive ) assume F is covariant ; ::_thesis: F is reflexive then reconsider F = F as Covariant FunctorStr over C1,C2 by Def26; F is reflexive ; hence F is reflexive ; ::_thesis: verum end; end; registration let C1 be non empty transitive with_units AltCatStr ; let C2 be non empty with_units AltCatStr ; cluster contravariant -> reflexive for Functor of C1,C2; coherence for b1 being Functor of C1,C2 st b1 is contravariant holds b1 is reflexive proof let F be Functor of C1,C2; ::_thesis: ( F is contravariant implies F is reflexive ) assume F is contravariant ; ::_thesis: F is reflexive then reconsider F = F as Contravariant FunctorStr over C1,C2 by Def27; F is reflexive ; hence F is reflexive ; ::_thesis: verum end; end; theorem Th46: :: FUNCTOR0:46 for C1 being non empty transitive with_units AltCatStr for C2 being non empty with_units AltCatStr for F being Functor of C1,C2 st F is covariant & F is onto holds F is coreflexive proof let C1 be non empty transitive with_units AltCatStr ; ::_thesis: for C2 being non empty with_units AltCatStr for F being Functor of C1,C2 st F is covariant & F is onto holds F is coreflexive let C2 be non empty with_units AltCatStr ; ::_thesis: for F being Functor of C1,C2 st F is covariant & F is onto holds F is coreflexive let F be Functor of C1,C2; ::_thesis: ( F is covariant & F is onto implies F is coreflexive ) assume A1: ( F is covariant & F is onto ) ; ::_thesis: F is coreflexive then F is Covariant by Def26; hence F is coreflexive by A1, Th44; ::_thesis: verum end; theorem Th47: :: FUNCTOR0:47 for C1 being non empty transitive with_units AltCatStr for C2 being non empty with_units AltCatStr for F being Functor of C1,C2 st F is contravariant & F is onto holds F is coreflexive proof let C1 be non empty transitive with_units AltCatStr ; ::_thesis: for C2 being non empty with_units AltCatStr for F being Functor of C1,C2 st F is contravariant & F is onto holds F is coreflexive let C2 be non empty with_units AltCatStr ; ::_thesis: for F being Functor of C1,C2 st F is contravariant & F is onto holds F is coreflexive let F be Functor of C1,C2; ::_thesis: ( F is contravariant & F is onto implies F is coreflexive ) assume A1: ( F is contravariant & F is onto ) ; ::_thesis: F is coreflexive then F is Contravariant by Def27; hence F is coreflexive by A1, Th45; ::_thesis: verum end; theorem Th48: :: FUNCTOR0:48 for A, B being non empty transitive with_units AltCatStr for F being covariant Functor of A,B st F is bijective holds ex G being Functor of B,A st ( G = F " & G is bijective & G is covariant ) proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being covariant Functor of A,B st F is bijective holds ex G being Functor of B,A st ( G = F " & G is bijective & G is covariant ) let F be covariant Functor of A,B; ::_thesis: ( F is bijective implies ex G being Functor of B,A st ( G = F " & G is bijective & G is covariant ) ) assume A1: F is bijective ; ::_thesis: ex G being Functor of B,A st ( G = F " & G is bijective & G is covariant ) then F is injective by Def35; then F is one-to-one by Def33; then A2: the ObjectMap of F is one-to-one by Def6; A3: F is feasible by Def25; then A4: ( F " is bijective & F " is feasible ) by A1, Th35; A5: F is id-preserving by Def25; A6: F is comp-preserving by Def26; F is surjective by A1, Def35; then A7: F is onto by Def34; then A8: the ObjectMap of F is onto by Def7; A9: F is Covariant by Def26; A10: F is coreflexive by A7, Th46; A11: F " is Covariant proof F is Covariant by Def26; then the ObjectMap of F is Covariant by Def12; then consider f being Function of the carrier of A, the carrier of B such that A12: the ObjectMap of F = [:f,f:] by Def1; A13: f is one-to-one by A2, A12, Th7; then A14: dom (f ") = rng f by FUNCT_1:33; A15: rng (f ") = dom f by A13, FUNCT_1:33; A16: rng [:f,f:] = [: the carrier of B, the carrier of B:] by A8, A12, FUNCT_2:def_3; rng [:f,f:] = [:(rng f),(rng f):] by FUNCT_3:67; then rng f = the carrier of B by A16, ZFMISC_1:92; then reconsider g = f " as Function of the carrier of B, the carrier of A by A14, A15, FUNCT_2:def_1, RELSET_1:4; take g ; :: according to FUNCTOR0:def_1,FUNCTOR0:def_12 ::_thesis: the ObjectMap of (F ") = [:g,g:] [:f,f:] " = [:g,g:] by A13, Th6; hence the ObjectMap of (F ") = [:g,g:] by A1, A12, Def38; ::_thesis: verum end; A17: F " is id-preserving by A1, A3, A5, A10, Th37; F " is comp-preserving by A1, A3, A6, A9, A10, Th42; then reconsider G = F " as Functor of B,A by A4, A11, A17, Def25; take G ; ::_thesis: ( G = F " & G is bijective & G is covariant ) thus G = F " ; ::_thesis: ( G is bijective & G is covariant ) thus G is bijective by A1, A3, Th35; ::_thesis: G is covariant thus G is Covariant by A11; :: according to FUNCTOR0:def_26 ::_thesis: G is comp-preserving thus G is comp-preserving by A1, A3, A6, A9, A10, Th42; ::_thesis: verum end; theorem Th49: :: FUNCTOR0:49 for A, B being non empty transitive with_units AltCatStr for F being contravariant Functor of A,B st F is bijective holds ex G being Functor of B,A st ( G = F " & G is bijective & G is contravariant ) proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being contravariant Functor of A,B st F is bijective holds ex G being Functor of B,A st ( G = F " & G is bijective & G is contravariant ) let F be contravariant Functor of A,B; ::_thesis: ( F is bijective implies ex G being Functor of B,A st ( G = F " & G is bijective & G is contravariant ) ) assume A1: F is bijective ; ::_thesis: ex G being Functor of B,A st ( G = F " & G is bijective & G is contravariant ) then F is injective by Def35; then F is one-to-one by Def33; then A2: the ObjectMap of F is one-to-one by Def6; A3: F is feasible by Def25; then A4: ( F " is bijective & F " is feasible ) by A1, Th35; A5: F is id-preserving by Def25; A6: F is comp-reversing by Def27; F is surjective by A1, Def35; then A7: F is onto by Def34; then A8: the ObjectMap of F is onto by Def7; A9: F is Contravariant by Def27; A10: F is coreflexive by A7, Th47; A11: F " is Contravariant proof F is Contravariant by Def27; then the ObjectMap of F is Contravariant by Def13; then consider f being Function of the carrier of A, the carrier of B such that A12: the ObjectMap of F = ~ [:f,f:] by Def2; [:f,f:] is one-to-one by A2, A12, Th9; then A13: f is one-to-one by Th7; then A14: dom (f ") = rng f by FUNCT_1:33; A15: rng (f ") = dom f by A13, FUNCT_1:33; [:f,f:] is onto by A8, A12, Th13; then A16: rng [:f,f:] = [: the carrier of B, the carrier of B:] by FUNCT_2:def_3; rng [:f,f:] = [:(rng f),(rng f):] by FUNCT_3:67; then rng f = the carrier of B by A16, ZFMISC_1:92; then reconsider g = f " as Function of the carrier of B, the carrier of A by A14, A15, FUNCT_2:def_1, RELSET_1:4; take g ; :: according to FUNCTOR0:def_2,FUNCTOR0:def_13 ::_thesis: the ObjectMap of (F ") = ~ [:g,g:] A17: [:f,f:] " = [:g,g:] by A13, Th6; thus the ObjectMap of (F ") = the ObjectMap of F " by A1, Def38 .= ~ [:g,g:] by A12, A13, A17, Th10 ; ::_thesis: verum end; A18: F " is id-preserving by A1, A3, A5, A10, Th37; F " is comp-reversing by A1, A3, A6, A9, A10, Th43; then reconsider G = F " as Functor of B,A by A4, A11, A18, Def25; take G ; ::_thesis: ( G = F " & G is bijective & G is contravariant ) thus G = F " ; ::_thesis: ( G is bijective & G is contravariant ) thus G is bijective by A1, A3, Th35; ::_thesis: G is contravariant thus G is Contravariant by A11; :: according to FUNCTOR0:def_27 ::_thesis: G is comp-reversing thus G is comp-reversing by A1, A3, A6, A9, A10, Th43; ::_thesis: verum end; definition let A, B be non empty transitive with_units AltCatStr ; predA,B are_isomorphic means :: FUNCTOR0:def 39 ex F being Functor of A,B st ( F is bijective & F is covariant ); reflexivity for A being non empty transitive with_units AltCatStr ex F being Functor of A,A st ( F is bijective & F is covariant ) proof let A be non empty transitive with_units AltCatStr ; ::_thesis: ex F being Functor of A,A st ( F is bijective & F is covariant ) take id A ; ::_thesis: ( id A is bijective & id A is covariant ) thus ( id A is bijective & id A is covariant ) ; ::_thesis: verum end; symmetry for A, B being non empty transitive with_units AltCatStr st ex F being Functor of A,B st ( F is bijective & F is covariant ) holds ex F being Functor of B,A st ( F is bijective & F is covariant ) proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: ( ex F being Functor of A,B st ( F is bijective & F is covariant ) implies ex F being Functor of B,A st ( F is bijective & F is covariant ) ) given F being Functor of A,B such that A1: ( F is bijective & F is covariant ) ; ::_thesis: ex F being Functor of B,A st ( F is bijective & F is covariant ) consider G being Functor of B,A such that G = F " and A2: ( G is bijective & G is covariant ) by A1, Th48; take G ; ::_thesis: ( G is bijective & G is covariant ) thus ( G is bijective & G is covariant ) by A2; ::_thesis: verum end; predA,B are_anti-isomorphic means :: FUNCTOR0:def 40 ex F being Functor of A,B st ( F is bijective & F is contravariant ); symmetry for A, B being non empty transitive with_units AltCatStr st ex F being Functor of A,B st ( F is bijective & F is contravariant ) holds ex F being Functor of B,A st ( F is bijective & F is contravariant ) proof let A, B be non empty transitive with_units AltCatStr ; ::_thesis: ( ex F being Functor of A,B st ( F is bijective & F is contravariant ) implies ex F being Functor of B,A st ( F is bijective & F is contravariant ) ) given F being Functor of A,B such that A3: ( F is bijective & F is contravariant ) ; ::_thesis: ex F being Functor of B,A st ( F is bijective & F is contravariant ) consider G being Functor of B,A such that G = F " and A4: ( G is bijective & G is contravariant ) by A3, Th49; take G ; ::_thesis: ( G is bijective & G is contravariant ) thus ( G is bijective & G is contravariant ) by A4; ::_thesis: verum end; end; :: deftheorem defines are_isomorphic FUNCTOR0:def_39_:_ for A, B being non empty transitive with_units AltCatStr holds ( A,B are_isomorphic iff ex F being Functor of A,B st ( F is bijective & F is covariant ) ); :: deftheorem defines are_anti-isomorphic FUNCTOR0:def_40_:_ for A, B being non empty transitive with_units AltCatStr holds ( A,B are_anti-isomorphic iff ex F being Functor of A,B st ( F is bijective & F is contravariant ) );