:: YONEDA_1 semantic presentation begin definition let A be Category; func EnsHom A -> Category equals :: YONEDA_1:def 1 Ens (Hom A); correctness coherence Ens (Hom A) is Category; ; end; :: deftheorem defines EnsHom YONEDA_1:def_1_:_ for A being Category holds EnsHom A = Ens (Hom A); theorem Th1: :: YONEDA_1:1 for A being Category for f, g being Function for m1, m2 being Morphism of (EnsHom A) st cod m1 = dom m2 & [[(dom m1),(cod m1)],f] = m1 & [[(dom m2),(cod m2)],g] = m2 holds [[(dom m1),(cod m2)],(g * f)] = m2 (*) m1 proof let A be Category; ::_thesis: for f, g being Function for m1, m2 being Morphism of (EnsHom A) st cod m1 = dom m2 & [[(dom m1),(cod m1)],f] = m1 & [[(dom m2),(cod m2)],g] = m2 holds [[(dom m1),(cod m2)],(g * f)] = m2 (*) m1 let f, g be Function; ::_thesis: for m1, m2 being Morphism of (EnsHom A) st cod m1 = dom m2 & [[(dom m1),(cod m1)],f] = m1 & [[(dom m2),(cod m2)],g] = m2 holds [[(dom m1),(cod m2)],(g * f)] = m2 (*) m1 let m1, m2 be Morphism of (EnsHom A); ::_thesis: ( cod m1 = dom m2 & [[(dom m1),(cod m1)],f] = m1 & [[(dom m2),(cod m2)],g] = m2 implies [[(dom m1),(cod m2)],(g * f)] = m2 (*) m1 ) assume that A1: cod m1 = dom m2 and A2: [[(dom m1),(cod m1)],f] = m1 and A3: [[(dom m2),(cod m2)],g] = m2 ; ::_thesis: [[(dom m1),(cod m2)],(g * f)] = m2 (*) m1 A4: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13; then reconsider m19 = m1 as Element of Maps (Hom A) ; reconsider m29 = m2 as Element of Maps (Hom A) by A4; A5: cod m19 = (m1 `1) `2 by ENS_1:def_4 .= [(dom m1),(cod m1)] `2 by A2, MCART_1:7 .= dom m2 by A1 .= [(dom m2),(cod m2)] `1 .= (m2 `1) `1 by A3, MCART_1:7 .= dom m29 by ENS_1:def_3 ; [[(dom m19),(cod m19)],(m19 `2)] = m1 by ENS_1:8; then A6: m19 `2 = f by A2, XTUPLE_0:1; [[(dom m29),(cod m29)],(m29 `2)] = m2 by ENS_1:8; then A7: m29 `2 = g by A3, XTUPLE_0:1; A8: cod m2 = [(dom m2),(cod m2)] `2 .= (m2 `1) `2 by A3, MCART_1:7 .= cod m29 by ENS_1:def_4 ; A9: dom m19 = (m1 `1) `1 by ENS_1:def_3 .= [(dom m1),(cod m1)] `1 by A2, MCART_1:7 .= dom m1 ; [m2,m1] in dom the Comp of (EnsHom A) by A1, CAT_1:15; then m2 (*) m1 = (fComp (Hom A)) . (m29,m19) by A4, CAT_1:def_1 .= m29 * m19 by A5, ENS_1:def_11 .= [[(dom m1),(cod m2)],(g * f)] by A5, A9, A8, A7, A6, ENS_1:def_6 ; hence [[(dom m1),(cod m2)],(g * f)] = m2 (*) m1 ; ::_thesis: verum end; definition let A be Category; let a be Object of A; func<|a,?> -> Functor of A, EnsHom A equals :: YONEDA_1:def 2 hom?- a; coherence hom?- a is Functor of A, EnsHom A by ENS_1:49; end; :: deftheorem defines <| YONEDA_1:def_2_:_ for A being Category for a being Object of A holds <|a,?> = hom?- a; theorem Th2: :: YONEDA_1:2 for A being Category for f being Morphism of A holds <|(cod f),?> is_naturally_transformable_to <|(dom f),?> proof let A be Category; ::_thesis: for f being Morphism of A holds <|(cod f),?> is_naturally_transformable_to <|(dom f),?> let f be Morphism of A; ::_thesis: <|(cod f),?> is_naturally_transformable_to <|(dom f),?> set F1 = <|(cod f),?>; set F2 = <|(dom f),?>; set B = EnsHom A; deffunc H1( Element of A) -> set = [[(Hom ((cod f),\$1)),(Hom ((dom f),\$1))],(hom (f,\$1))]; A1: for a being Object of A holds [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) proof let a be Object of A; ::_thesis: [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) A2: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13; then reconsider m = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] as Morphism of (EnsHom A) by ENS_1:48; reconsider m9 = m as Element of Maps (Hom A) by ENS_1:48; A3: cod m = (fCod (Hom A)) . m by A2 .= cod m9 by ENS_1:def_10 .= (m `1) `2 by ENS_1:def_4 .= [(Hom ((cod f),a)),(Hom ((dom f),a))] `2 by MCART_1:7 .= Hom ((dom f),a) .= (Obj (hom?- ((Hom A),(dom f)))) . a by ENS_1:60 .= (hom?- ((Hom A),(dom f))) . a .= <|(dom f),?> . a by ENS_1:def_25 ; dom m = (fDom (Hom A)) . m by A2 .= dom m9 by ENS_1:def_9 .= (m `1) `1 by ENS_1:def_3 .= [(Hom ((cod f),a)),(Hom ((dom f),a))] `1 by MCART_1:7 .= Hom ((cod f),a) .= (Obj (hom?- ((Hom A),(cod f)))) . a by ENS_1:60 .= (hom?- ((Hom A),(cod f))) . a .= <|(cod f),?> . a by ENS_1:def_25 ; hence [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A3; ::_thesis: verum end; A4: for a being Element of A holds H1(a) in the carrier' of (EnsHom A) proof let a be Object of A; ::_thesis: H1(a) in the carrier' of (EnsHom A) [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A1; hence H1(a) in the carrier' of (EnsHom A) ; ::_thesis: verum end; consider t being Function of the carrier of A, the carrier' of (EnsHom A) such that A5: for o being Element of A holds t . o = H1(o) from FUNCT_2:sch_8(A4); A6: for a being Object of A holds t . a is Morphism of <|(cod f),?> . a,<|(dom f),?> . a proof let a be Object of A; ::_thesis: t . a is Morphism of <|(cod f),?> . a,<|(dom f),?> . a [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A1; then [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] is Morphism of <|(cod f),?> . a,<|(dom f),?> . a by CAT_1:def_5; hence t . a is Morphism of <|(cod f),?> . a,<|(dom f),?> . a by A5; ::_thesis: verum end; for a being Object of A holds Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) <> {} by A1; then A7: <|(cod f),?> is_transformable_to <|(dom f),?> by NATTRA_1:def_2; then reconsider t = t as transformation of <|(cod f),?>,<|(dom f),?> by A6, NATTRA_1:def_3; for a, b being Object of A st Hom (a,b) <> {} holds for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) proof let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) ) assume A8: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) A9: Hom ((<|(cod f),?> . a),(<|(cod f),?> . b)) <> {} by A8, CAT_1:84; let g be Morphism of a,b; ::_thesis: (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) A10: dom g = a by A8, CAT_1:5; A11: rng (hom ((cod f),g)) c= dom (hom (f,b)) proof A12: cod g = b by A8, CAT_1:5; percases ( Hom ((dom f),b) = {} or Hom ((dom f),b) <> {} ) ; supposeA13: Hom ((dom f),b) = {} ; ::_thesis: rng (hom ((cod f),g)) c= dom (hom (f,b)) Hom ((cod f),b) = {} by A13, ENS_1:42; hence rng (hom ((cod f),g)) c= dom (hom (f,b)) by A12; ::_thesis: verum end; supposeA14: Hom ((dom f),b) <> {} ; ::_thesis: rng (hom ((cod f),g)) c= dom (hom (f,b)) cod g = b by A8, CAT_1:5; then A15: ( rng (hom ((cod f),g)) c= Hom ((cod f),(cod g)) & Hom ((cod f),(cod g)) = dom (hom (f,b)) ) by A14, FUNCT_2:def_1, RELAT_1:def_19; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (hom ((cod f),g)) or e in dom (hom (f,b)) ) assume e in rng (hom ((cod f),g)) ; ::_thesis: e in dom (hom (f,b)) hence e in dom (hom (f,b)) by A15; ::_thesis: verum end; end; end; A16: rng (hom (f,a)) c= dom (hom ((dom f),g)) proof A17: dom g = a by A8, CAT_1:5; percases ( Hom ((dom f),(cod g)) = {} or Hom ((dom f),(cod g)) <> {} ) ; supposeA18: Hom ((dom f),(cod g)) = {} ; ::_thesis: rng (hom (f,a)) c= dom (hom ((dom f),g)) Hom ((dom f),(dom g)) = {} by A18, ENS_1:42; hence rng (hom (f,a)) c= dom (hom ((dom f),g)) by A17; ::_thesis: verum end; supposeA19: Hom ((dom f),(cod g)) <> {} ; ::_thesis: rng (hom (f,a)) c= dom (hom ((dom f),g)) let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (hom (f,a)) or e in dom (hom ((dom f),g)) ) assume A20: e in rng (hom (f,a)) ; ::_thesis: e in dom (hom ((dom f),g)) ( rng (hom (f,a)) c= Hom ((dom f),a) & Hom ((dom f),a) = dom (hom ((dom f),g)) ) by A17, A19, FUNCT_2:def_1, RELAT_1:def_19; hence e in dom (hom ((dom f),g)) by A20; ::_thesis: verum end; end; end; A21: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) proof percases ( Hom ((cod f),(dom g)) = {} or Hom ((cod f),(dom g)) <> {} ) ; supposeA22: Hom ((cod f),(dom g)) = {} ; ::_thesis: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) dom ((hom (f,b)) * (hom ((cod f),g))) = dom (hom ((cod f),g)) by A11, RELAT_1:27 .= Hom ((cod f),(dom g)) by A22 .= dom (hom (f,a)) by A10, A22 .= dom ((hom ((dom f),g)) * (hom (f,a))) by A16, RELAT_1:27 ; hence dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) ; ::_thesis: verum end; supposeA23: Hom ((cod f),(dom g)) <> {} ; ::_thesis: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) then A24: Hom ((cod f),(cod g)) <> {} by ENS_1:42; A25: Hom ((dom f),a) <> {} by A10, A23, ENS_1:42; dom ((hom (f,b)) * (hom ((cod f),g))) = dom (hom ((cod f),g)) by A11, RELAT_1:27 .= Hom ((cod f),(dom g)) by A24, FUNCT_2:def_1 .= Hom ((cod f),a) by A8, CAT_1:5 .= dom (hom (f,a)) by A25, FUNCT_2:def_1 .= dom ((hom ((dom f),g)) * (hom (f,a))) by A16, RELAT_1:27 ; hence dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) ; ::_thesis: verum end; end; end; A26: for x being set st x in dom ((hom (f,b)) * (hom ((cod f),g))) holds ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x proof let x be set ; ::_thesis: ( x in dom ((hom (f,b)) * (hom ((cod f),g))) implies ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x ) assume A27: x in dom ((hom (f,b)) * (hom ((cod f),g))) ; ::_thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x percases ( Hom ((cod f),(dom g)) <> {} or Hom ((cod f),(dom g)) = {} ) ; supposeA28: Hom ((cod f),(dom g)) <> {} ; ::_thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x A29: x in dom (hom ((cod f),g)) by A27, FUNCT_1:11; Hom ((cod f),(cod g)) <> {} by A28, ENS_1:42; then A30: x in Hom ((cod f),(dom g)) by A29, FUNCT_2:def_1; then reconsider x = x as Morphism of A ; A31: ( dom g = cod x & dom x = cod f ) by A30, CAT_1:1; A32: dom g = cod x by A30, CAT_1:1; then A33: cod (g (*) x) = cod g by CAT_1:17 .= b by A8, CAT_1:5 ; A34: (hom (f,a)) . x = x (*) f by A10, A30, ENS_1:def_20; then reconsider h = (hom (f,a)) . x as Morphism of A ; A35: dom x = cod f by A30, CAT_1:1; then A36: dom (x (*) f) = dom f by CAT_1:17; dom (g (*) x) = dom x by A32, CAT_1:17 .= cod f by A30, CAT_1:1 ; then A37: g (*) x in Hom ((cod f),b) by A33; cod (x (*) f) = cod x by A35, CAT_1:17 .= dom g by A30, CAT_1:1 ; then A38: (hom (f,a)) . x in Hom ((dom f),(dom g)) by A34, A36; ((hom (f,b)) * (hom ((cod f),g))) . x = (hom (f,b)) . ((hom ((cod f),g)) . x) by A27, FUNCT_1:12 .= (hom (f,b)) . (g (*) x) by A30, ENS_1:def_19 .= (g (*) x) (*) f by A37, ENS_1:def_20 .= g (*) (x (*) f) by A31, CAT_1:18 .= g (*) h by A10, A30, ENS_1:def_20 .= (hom ((dom f),g)) . ((hom (f,a)) . x) by A38, ENS_1:def_19 .= ((hom ((dom f),g)) * (hom (f,a))) . x by A21, A27, FUNCT_1:12 ; hence ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x ; ::_thesis: verum end; supposeA39: Hom ((cod f),(dom g)) = {} ; ::_thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x x in dom (hom ((cod f),g)) by A27, FUNCT_1:11; hence ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x by A39; ::_thesis: verum end; end; end; A40: Hom ((<|(dom f),?> . a),(<|(dom f),?> . b)) <> {} by A8, CAT_1:84; A41: cod g = b by A8, CAT_1:5; reconsider f4 = t . a as Morphism of (EnsHom A) ; A42: t . a = t . a by A7, NATTRA_1:def_5 .= [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] by A5 ; then reconsider f49 = f4 as Element of Maps (Hom A) by ENS_1:48; A43: Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) <> {} by A1; reconsider f1 = t . b as Morphism of (EnsHom A) ; A44: t . b = t . b by A7, NATTRA_1:def_5 .= [[(Hom ((cod f),b)),(Hom ((dom f),b))],(hom (f,b))] by A5 ; then reconsider f19 = f1 as Element of Maps (Hom A) by ENS_1:48; A45: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13; then A46: cod f1 = (fCod (Hom A)) . f1 .= cod f19 by ENS_1:def_10 .= (f1 `1) `2 by ENS_1:def_4 .= [(Hom ((cod f),b)),(Hom ((dom f),b))] `2 by A44, MCART_1:7 .= Hom ((dom f),b) ; A47: dom f4 = (fDom (Hom A)) . f4 by A45 .= dom f49 by ENS_1:def_9 .= (f4 `1) `1 by ENS_1:def_3 .= [(Hom ((cod f),a)),(Hom ((dom f),a))] `1 by A42, MCART_1:7 .= Hom ((cod f),a) ; A48: cod f4 = (fCod (Hom A)) . f4 by A45 .= cod f49 by ENS_1:def_10 .= (f4 `1) `2 by ENS_1:def_4 .= [(Hom ((cod f),a)),(Hom ((dom f),a))] `2 by A42, MCART_1:7 .= Hom ((dom f),a) ; reconsider f2 = <|(cod f),?> /. g as Morphism of (EnsHom A) ; A49: f2 = (hom?- (cod f)) . g by A8, CAT_3:def_10 .= [[(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))],(hom ((cod f),g))] by ENS_1:def_21 ; then reconsider f29 = f2 as Element of Maps (Hom A) by ENS_1:47; A50: dom f2 = (fDom (Hom A)) . f2 by A45 .= dom f29 by ENS_1:def_9 .= (f2 `1) `1 by ENS_1:def_3 .= [(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))] `1 by A49, MCART_1:7 .= Hom ((cod f),(dom g)) ; A51: cod f2 = (fCod (Hom A)) . f2 by A45 .= cod f29 by ENS_1:def_10 .= (f2 `1) `2 by ENS_1:def_4 .= [(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))] `2 by A49, MCART_1:7 .= Hom ((cod f),(cod g)) ; A52: dom f1 = (fDom (Hom A)) . f1 by A45 .= dom f19 by ENS_1:def_9 .= (f1 `1) `1 by ENS_1:def_3 .= [(Hom ((cod f),b)),(Hom ((dom f),b))] `1 by A44, MCART_1:7 .= Hom ((cod f),b) ; then A53: cod f2 = dom f1 by A8, A51, CAT_1:5; reconsider f3 = <|(dom f),?> /. g as Morphism of (EnsHom A) ; A54: f3 = (hom?- (dom f)) . g by A8, CAT_3:def_10 .= [[(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))],(hom ((dom f),g))] by ENS_1:def_21 ; then reconsider f39 = f3 as Element of Maps (Hom A) by ENS_1:47; A55: cod f3 = (fCod (Hom A)) . f3 by A45 .= cod f39 by ENS_1:def_10 .= (f3 `1) `2 by ENS_1:def_4 .= [(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))] `2 by A54, MCART_1:7 .= Hom ((dom f),(cod g)) ; A56: dom f3 = (fDom (Hom A)) . f3 by A45 .= dom f39 by ENS_1:def_9 .= (f3 `1) `1 by ENS_1:def_3 .= [(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))] `1 by A54, MCART_1:7 .= Hom ((dom f),(dom g)) ; then A57: cod f4 = dom f3 by A8, A48, CAT_1:5; Hom ((<|(cod f),?> . b),(<|(dom f),?> . b)) <> {} by A1; then (t . b) * (<|(cod f),?> /. g) = f1 (*) f2 by A9, CAT_1:def_13 .= [[(Hom ((cod f),(dom g))),(Hom ((dom f),b))],((hom (f,b)) * (hom ((cod f),g)))] by A44, A52, A46, A49, A50, A51, A53, Th1 .= [[(Hom ((cod f),a)),(Hom ((dom f),(cod g)))],((hom ((dom f),g)) * (hom (f,a)))] by A10, A41, A21, A26, FUNCT_1:2 .= f3 (*) f4 by A54, A56, A55, A42, A47, A48, A57, Th1 .= (<|(dom f),?> /. g) * (t . a) by A40, A43, CAT_1:def_13 ; hence (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) ; ::_thesis: verum end; hence <|(cod f),?> is_naturally_transformable_to <|(dom f),?> by A7, NATTRA_1:def_7; ::_thesis: verum end; definition let A be Category; let f be Morphism of A; func<|f,?> -> natural_transformation of <|(cod f),?>,<|(dom f),?> means :Def3: :: YONEDA_1:def 3 for o being Object of A holds it . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))]; existence ex b1 being natural_transformation of <|(cod f),?>,<|(dom f),?> st for o being Object of A holds b1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] proof set B = EnsHom A; deffunc H1( Element of A) -> set = [[(Hom ((cod f),\$1)),(Hom ((dom f),\$1))],(hom (f,(id \$1)))]; set F1 = <|(cod f),?>; set F2 = <|(dom f),?>; A1: for o being Object of A holds [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) proof let o be Object of A; ::_thesis: [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) A2: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13; A3: hom (f,(id o)) = hom (f,o) by ENS_1:53; then reconsider m = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] as Morphism of (EnsHom A) by A2, ENS_1:48; reconsider m9 = m as Element of Maps (Hom A) by A3, ENS_1:48; A4: cod m = (fCod (Hom A)) . m by A2 .= cod m9 by ENS_1:def_10 .= (m `1) `2 by ENS_1:def_4 .= [(Hom ((cod f),o)),(Hom ((dom f),o))] `2 by MCART_1:7 .= Hom ((dom f),o) .= (Obj (hom?- ((Hom A),(dom f)))) . o by ENS_1:60 .= (hom?- ((Hom A),(dom f))) . o .= <|(dom f),?> . o by ENS_1:def_25 ; dom m = (fDom (Hom A)) . m by A2 .= dom m9 by ENS_1:def_9 .= (m `1) `1 by ENS_1:def_3 .= [(Hom ((cod f),o)),(Hom ((dom f),o))] `1 by MCART_1:7 .= Hom ((cod f),o) .= (Obj (hom?- ((Hom A),(cod f)))) . o by ENS_1:60 .= (hom?- ((Hom A),(cod f))) . o .= <|(cod f),?> . o by ENS_1:def_25 ; hence [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) by A4; ::_thesis: verum end; A5: for o being Element of A holds H1(o) in the carrier' of (EnsHom A) proof let o be Object of A; ::_thesis: H1(o) in the carrier' of (EnsHom A) [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) by A1; hence H1(o) in the carrier' of (EnsHom A) ; ::_thesis: verum end; consider t being Function of the carrier of A, the carrier' of (EnsHom A) such that A6: for o being Element of A holds t . o = H1(o) from FUNCT_2:sch_8(A5); A7: for o being Object of A holds t . o is Morphism of <|(cod f),?> . o,<|(dom f),?> . o proof let o be Object of A; ::_thesis: t . o is Morphism of <|(cod f),?> . o,<|(dom f),?> . o [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) by A1; then [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] is Morphism of <|(cod f),?> . o,<|(dom f),?> . o by CAT_1:def_5; hence t . o is Morphism of <|(cod f),?> . o,<|(dom f),?> . o by A6; ::_thesis: verum end; for o being Object of A holds Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) <> {} by A1; then A8: <|(cod f),?> is_transformable_to <|(dom f),?> by NATTRA_1:def_2; then reconsider t = t as transformation of <|(cod f),?>,<|(dom f),?> by A7, NATTRA_1:def_3; A9: for a, b being Object of A st Hom (a,b) <> {} holds for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) proof let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) ) assume A10: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) A11: Hom ((<|(cod f),?> . a),(<|(cod f),?> . b)) <> {} by A10, CAT_1:84; let g be Morphism of a,b; ::_thesis: (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) A12: dom g = a by A10, CAT_1:5; A13: rng (hom ((cod f),g)) c= dom (hom (f,b)) proof A14: cod g = b by A10, CAT_1:5; percases ( Hom ((dom f),b) = {} or Hom ((dom f),b) <> {} ) ; supposeA15: Hom ((dom f),b) = {} ; ::_thesis: rng (hom ((cod f),g)) c= dom (hom (f,b)) Hom ((cod f),b) = {} by A15, ENS_1:42; hence rng (hom ((cod f),g)) c= dom (hom (f,b)) by A14; ::_thesis: verum end; supposeA16: Hom ((dom f),b) <> {} ; ::_thesis: rng (hom ((cod f),g)) c= dom (hom (f,b)) cod g = b by A10, CAT_1:5; then A17: ( rng (hom ((cod f),g)) c= Hom ((cod f),(cod g)) & Hom ((cod f),(cod g)) = dom (hom (f,b)) ) by A16, FUNCT_2:def_1, RELAT_1:def_19; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (hom ((cod f),g)) or e in dom (hom (f,b)) ) assume e in rng (hom ((cod f),g)) ; ::_thesis: e in dom (hom (f,b)) hence e in dom (hom (f,b)) by A17; ::_thesis: verum end; end; end; A18: rng (hom (f,a)) c= dom (hom ((dom f),g)) proof A19: dom g = a by A10, CAT_1:5; percases ( Hom ((dom f),(cod g)) = {} or Hom ((dom f),(cod g)) <> {} ) ; supposeA20: Hom ((dom f),(cod g)) = {} ; ::_thesis: rng (hom (f,a)) c= dom (hom ((dom f),g)) Hom ((dom f),(dom g)) = {} by A20, ENS_1:42; hence rng (hom (f,a)) c= dom (hom ((dom f),g)) by A19; ::_thesis: verum end; supposeA21: Hom ((dom f),(cod g)) <> {} ; ::_thesis: rng (hom (f,a)) c= dom (hom ((dom f),g)) let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (hom (f,a)) or e in dom (hom ((dom f),g)) ) assume A22: e in rng (hom (f,a)) ; ::_thesis: e in dom (hom ((dom f),g)) ( rng (hom (f,a)) c= Hom ((dom f),a) & Hom ((dom f),a) = dom (hom ((dom f),g)) ) by A19, A21, FUNCT_2:def_1, RELAT_1:def_19; hence e in dom (hom ((dom f),g)) by A22; ::_thesis: verum end; end; end; A23: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) proof percases ( Hom ((cod f),(dom g)) = {} or Hom ((cod f),(dom g)) <> {} ) ; supposeA24: Hom ((cod f),(dom g)) = {} ; ::_thesis: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) dom ((hom (f,b)) * (hom ((cod f),g))) = dom (hom ((cod f),g)) by A13, RELAT_1:27 .= Hom ((cod f),a) by A12, A24 .= dom (hom (f,a)) by A12, A24 .= dom ((hom ((dom f),g)) * (hom (f,a))) by A18, RELAT_1:27 ; hence dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) ; ::_thesis: verum end; supposeA25: Hom ((cod f),(dom g)) <> {} ; ::_thesis: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) then A26: Hom ((cod f),(cod g)) <> {} by ENS_1:42; A27: Hom ((dom f),a) <> {} by A12, A25, ENS_1:42; dom ((hom (f,b)) * (hom ((cod f),g))) = dom (hom ((cod f),g)) by A13, RELAT_1:27 .= Hom ((cod f),a) by A12, A26, FUNCT_2:def_1 .= dom (hom (f,a)) by A27, FUNCT_2:def_1 .= dom ((hom ((dom f),g)) * (hom (f,a))) by A18, RELAT_1:27 ; hence dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) ; ::_thesis: verum end; end; end; A28: for x being set st x in dom ((hom (f,b)) * (hom ((cod f),g))) holds ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x proof let x be set ; ::_thesis: ( x in dom ((hom (f,b)) * (hom ((cod f),g))) implies ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x ) assume A29: x in dom ((hom (f,b)) * (hom ((cod f),g))) ; ::_thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x percases ( Hom ((cod f),(dom g)) <> {} or Hom ((cod f),(dom g)) = {} ) ; supposeA30: Hom ((cod f),(dom g)) <> {} ; ::_thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x A31: x in dom (hom ((cod f),g)) by A29, FUNCT_1:11; Hom ((cod f),(cod g)) <> {} by A30, ENS_1:42; then A32: x in Hom ((cod f),(dom g)) by A31, FUNCT_2:def_1; then reconsider x = x as Morphism of A ; A33: dom g = cod x by A32, CAT_1:1; cod g = b by A10, CAT_1:5; then A34: cod (g (*) x) = b by A33, CAT_1:17; dom (g (*) x) = dom x by A33, CAT_1:17 .= cod f by A32, CAT_1:1 ; then A35: g (*) x in Hom ((cod f),b) by A34; A36: dom x = cod f by A32, CAT_1:1; then A37: dom (x (*) f) = dom f by CAT_1:17; A38: (hom (f,a)) . x = x (*) f by A12, A32, ENS_1:def_20; then reconsider h = (hom (f,a)) . x as Morphism of A ; A39: ( dom g = cod x & dom x = cod f ) by A32, CAT_1:1; cod (x (*) f) = cod x by A36, CAT_1:17 .= dom g by A32, CAT_1:1 ; then A40: (hom (f,a)) . x in Hom ((dom f),(dom g)) by A38, A37; ((hom (f,b)) * (hom ((cod f),g))) . x = (hom (f,b)) . ((hom ((cod f),g)) . x) by A29, FUNCT_1:12 .= (hom (f,b)) . (g (*) x) by A32, ENS_1:def_19 .= (g (*) x) (*) f by A35, ENS_1:def_20 .= g (*) (x (*) f) by A39, CAT_1:18 .= g (*) h by A12, A32, ENS_1:def_20 .= (hom ((dom f),g)) . ((hom (f,a)) . x) by A40, ENS_1:def_19 .= ((hom ((dom f),g)) * (hom (f,a))) . x by A23, A29, FUNCT_1:12 ; hence ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x ; ::_thesis: verum end; supposeA41: Hom ((cod f),(dom g)) = {} ; ::_thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x x in dom (hom ((cod f),g)) by A29, FUNCT_1:11; hence ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x by A41; ::_thesis: verum end; end; end; A42: Hom ((<|(dom f),?> . a),(<|(dom f),?> . b)) <> {} by A10, CAT_1:84; A43: cod g = b by A10, CAT_1:5; reconsider f4 = t . a as Morphism of (EnsHom A) ; A44: t . a = t . a by A8, NATTRA_1:def_5 .= [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,(id a)))] by A6 .= [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] by ENS_1:53 ; then reconsider f49 = f4 as Element of Maps (Hom A) by ENS_1:48; A45: Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) <> {} by A1; reconsider f1 = t . b as Morphism of (EnsHom A) ; A46: t . b = t . b by A8, NATTRA_1:def_5 .= [[(Hom ((cod f),b)),(Hom ((dom f),b))],(hom (f,(id b)))] by A6 .= [[(Hom ((cod f),b)),(Hom ((dom f),b))],(hom (f,b))] by ENS_1:53 ; then reconsider f19 = f1 as Element of Maps (Hom A) by ENS_1:48; A47: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13; then A48: cod f1 = (fCod (Hom A)) . f1 .= cod f19 by ENS_1:def_10 .= (f1 `1) `2 by ENS_1:def_4 .= [(Hom ((cod f),b)),(Hom ((dom f),b))] `2 by A46, MCART_1:7 .= Hom ((dom f),b) ; A49: dom f4 = (fDom (Hom A)) . f4 by A47 .= dom f49 by ENS_1:def_9 .= (f4 `1) `1 by ENS_1:def_3 .= [(Hom ((cod f),a)),(Hom ((dom f),a))] `1 by A44, MCART_1:7 .= Hom ((cod f),a) ; A50: cod f4 = (fCod (Hom A)) . f4 by A47 .= cod f49 by ENS_1:def_10 .= (f4 `1) `2 by ENS_1:def_4 .= [(Hom ((cod f),a)),(Hom ((dom f),a))] `2 by A44, MCART_1:7 .= Hom ((dom f),a) ; reconsider f2 = <|(cod f),?> /. g as Morphism of (EnsHom A) ; A51: f2 = (hom?- (cod f)) . g by A10, CAT_3:def_10 .= [[(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))],(hom ((cod f),g))] by ENS_1:def_21 ; then reconsider f29 = f2 as Element of Maps (Hom A) by ENS_1:47; A52: dom f2 = (fDom (Hom A)) . f2 by A47 .= dom f29 by ENS_1:def_9 .= (f2 `1) `1 by ENS_1:def_3 .= [(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))] `1 by A51, MCART_1:7 .= Hom ((cod f),(dom g)) ; A53: cod f2 = (fCod (Hom A)) . f2 by A47 .= cod f29 by ENS_1:def_10 .= (f2 `1) `2 by ENS_1:def_4 .= [(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))] `2 by A51, MCART_1:7 .= Hom ((cod f),(cod g)) ; A54: dom f1 = (fDom (Hom A)) . f1 by A47 .= dom f19 by ENS_1:def_9 .= (f1 `1) `1 by ENS_1:def_3 .= [(Hom ((cod f),b)),(Hom ((dom f),b))] `1 by A46, MCART_1:7 .= Hom ((cod f),b) ; then A55: cod f2 = dom f1 by A10, A53, CAT_1:5; reconsider f3 = <|(dom f),?> /. g as Morphism of (EnsHom A) ; A56: f3 = (hom?- (dom f)) . g by A10, CAT_3:def_10 .= [[(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))],(hom ((dom f),g))] by ENS_1:def_21 ; then reconsider f39 = f3 as Element of Maps (Hom A) by ENS_1:47; A57: cod f3 = (fCod (Hom A)) . f3 by A47 .= cod f39 by ENS_1:def_10 .= (f3 `1) `2 by ENS_1:def_4 .= [(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))] `2 by A56, MCART_1:7 .= Hom ((dom f),(cod g)) ; A58: dom f3 = (fDom (Hom A)) . f3 by A47 .= dom f39 by ENS_1:def_9 .= (f3 `1) `1 by ENS_1:def_3 .= [(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))] `1 by A56, MCART_1:7 .= Hom ((dom f),(dom g)) ; then A59: cod f4 = dom f3 by A10, A50, CAT_1:5; Hom ((<|(cod f),?> . b),(<|(dom f),?> . b)) <> {} by A1; then (t . b) * (<|(cod f),?> /. g) = f1 (*) f2 by A11, CAT_1:def_13 .= [[(Hom ((cod f),(dom g))),(Hom ((dom f),b))],((hom (f,b)) * (hom ((cod f),g)))] by A46, A54, A48, A51, A52, A53, A55, Th1 .= [[(Hom ((cod f),a)),(Hom ((dom f),(cod g)))],((hom ((dom f),g)) * (hom (f,a)))] by A12, A43, A23, A28, FUNCT_1:2 .= f3 (*) f4 by A56, A58, A57, A44, A49, A50, A59, Th1 .= (<|(dom f),?> /. g) * (t . a) by A42, A45, CAT_1:def_13 ; hence (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) ; ::_thesis: verum end; <|(cod f),?> is_naturally_transformable_to <|(dom f),?> by Th2; then reconsider t = t as natural_transformation of <|(cod f),?>,<|(dom f),?> by A9, NATTRA_1:def_8; for o being Element of A holds t . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] proof let o be Object of A; ::_thesis: t . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] t . o = t . o by A8, NATTRA_1:def_5 .= [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] by A6 ; hence t . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ; ::_thesis: verum end; hence ex b1 being natural_transformation of <|(cod f),?>,<|(dom f),?> st for o being Object of A holds b1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ; ::_thesis: verum end; uniqueness for b1, b2 being natural_transformation of <|(cod f),?>,<|(dom f),?> st ( for o being Object of A holds b1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ) & ( for o being Object of A holds b2 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ) holds b1 = b2 proof for a being Object of A holds [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) proof let a be Object of A; ::_thesis: [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) A60: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13; then reconsider m = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] as Morphism of (EnsHom A) by ENS_1:48; reconsider m9 = m as Element of Maps (Hom A) by ENS_1:48; A61: cod m = (fCod (Hom A)) . m by A60 .= cod m9 by ENS_1:def_10 .= (m `1) `2 by ENS_1:def_4 .= [(Hom ((cod f),a)),(Hom ((dom f),a))] `2 by MCART_1:7 .= Hom ((dom f),a) .= (Obj (hom?- ((Hom A),(dom f)))) . a by ENS_1:60 .= (hom?- ((Hom A),(dom f))) . a .= <|(dom f),?> . a by ENS_1:def_25 ; dom m = (fDom (Hom A)) . m by A60 .= dom m9 by ENS_1:def_9 .= (m `1) `1 by ENS_1:def_3 .= [(Hom ((cod f),a)),(Hom ((dom f),a))] `1 by MCART_1:7 .= Hom ((cod f),a) .= (Obj (hom?- ((Hom A),(cod f)))) . a by ENS_1:60 .= (hom?- ((Hom A),(cod f))) . a .= <|(cod f),?> . a by ENS_1:def_25 ; hence [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A61; ::_thesis: verum end; then for a being Object of A holds Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) <> {} ; then A62: <|(cod f),?> is_transformable_to <|(dom f),?> by NATTRA_1:def_2; let h1, h2 be natural_transformation of <|(cod f),?>,<|(dom f),?>; ::_thesis: ( ( for o being Object of A holds h1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ) & ( for o being Object of A holds h2 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ) implies h1 = h2 ) assume that A63: for o being Object of A holds h1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] and A64: for o being Object of A holds h2 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ; ::_thesis: h1 = h2 now__::_thesis:_for_o_being_Object_of_A_holds_h1_._o_=_h2_._o let o be Object of A; ::_thesis: h1 . o = h2 . o thus h1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] by A63 .= h2 . o by A64 ; ::_thesis: verum end; hence h1 = h2 by A62, NATTRA_1:19; ::_thesis: verum end; end; :: deftheorem Def3 defines <| YONEDA_1:def_3_:_ for A being Category for f being Morphism of A for b3 being natural_transformation of <|(cod f),?>,<|(dom f),?> holds ( b3 = <|f,?> iff for o being Object of A holds b3 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ); theorem Th3: :: YONEDA_1:3 for A being Category for f being Element of the carrier' of A holds [[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Element of the carrier' of (Functors (A,(EnsHom A))) proof let A be Category; ::_thesis: for f being Element of the carrier' of A holds [[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Element of the carrier' of (Functors (A,(EnsHom A))) let f be Element of the carrier' of A; ::_thesis: [[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Element of the carrier' of (Functors (A,(EnsHom A))) <|(cod f),?> is_naturally_transformable_to <|(dom f),?> by Th2; then [[<|(cod f),?>,<|(dom f),?>],<|f,?>] in NatTrans (A,(EnsHom A)) by NATTRA_1:def_16; hence [[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Element of the carrier' of (Functors (A,(EnsHom A))) by NATTRA_1:def_17; ::_thesis: verum end; definition let A be Category; func Yoneda A -> Contravariant_Functor of A, Functors (A,(EnsHom A)) means :Def4: :: YONEDA_1:def 4 for f being Morphism of A holds it . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>]; existence ex b1 being Contravariant_Functor of A, Functors (A,(EnsHom A)) st for f being Morphism of A holds b1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] proof deffunc H1( Element of the carrier' of A) -> set = [[<|(cod \$1),?>,<|(dom \$1),?>],<|\$1,?>]; A1: for f being Element of the carrier' of A holds H1(f) in the carrier' of (Functors (A,(EnsHom A))) proof let f be Morphism of A; ::_thesis: H1(f) in the carrier' of (Functors (A,(EnsHom A))) [[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Morphism of (Functors (A,(EnsHom A))) by Th3; hence H1(f) in the carrier' of (Functors (A,(EnsHom A))) ; ::_thesis: verum end; consider F being Function of the carrier' of A, the carrier' of (Functors (A,(EnsHom A))) such that A2: for f being Element of the carrier' of A holds F . f = H1(f) from FUNCT_2:sch_8(A1); A3: for f, g being Morphism of A st dom g = cod f holds F . (g (*) f) = (F . f) (*) (F . g) proof let f, g be Morphism of A; ::_thesis: ( dom g = cod f implies F . (g (*) f) = (F . f) (*) (F . g) ) reconsider t1 = <|g,?> as natural_transformation of <|(cod g),?>,<|(dom g),?> ; assume A4: dom g = cod f ; ::_thesis: F . (g (*) f) = (F . f) (*) (F . g) then reconsider t = <|f,?> as natural_transformation of <|(dom g),?>,<|(dom f),?> ; A5: F . g = [[<|(cod g),?>,<|(dom g),?>],t1] by A2; A6: dom (g (*) f) = dom f by A4, CAT_1:17; then reconsider tt = t `*` t1 as natural_transformation of <|(cod (g (*) f)),?>,<|(dom (g (*) f)),?> by A4, CAT_1:17; A7: cod (g (*) f) = cod g by A4, CAT_1:17; for o being Object of A holds <|(g (*) f),?> . o = tt . o proof set F1 = <|(cod f),?>; set F2 = <|(dom f),?>; let o be Object of A; ::_thesis: <|(g (*) f),?> . o = tt . o reconsider f1 = t . o as Morphism of (EnsHom A) ; reconsider f2 = t1 . o as Morphism of (EnsHom A) ; A8: f2 = [[(Hom ((cod g),o)),(Hom ((dom g),o))],(hom (g,(id o)))] by Def3; for a being Object of A holds [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom ((<|(cod g),?> . a),(<|(dom g),?> . a)) proof let a be Object of A; ::_thesis: [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom ((<|(cod g),?> . a),(<|(dom g),?> . a)) A9: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13; then reconsider m = [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] as Morphism of (EnsHom A) by ENS_1:48; reconsider m9 = m as Element of Maps (Hom A) by ENS_1:48; A10: cod m = (fCod (Hom A)) . m by A9 .= cod m9 by ENS_1:def_10 .= (m `1) `2 by ENS_1:def_4 .= [(Hom ((cod g),a)),(Hom ((dom g),a))] `2 by MCART_1:7 .= Hom ((dom g),a) .= (Obj (hom?- ((Hom A),(dom g)))) . a by ENS_1:60 .= (hom?- ((Hom A),(dom g))) . a .= <|(dom g),?> . a by ENS_1:def_25 ; dom m = (fDom (Hom A)) . m by A9 .= dom m9 by ENS_1:def_9 .= (m `1) `1 by ENS_1:def_3 .= [(Hom ((cod g),a)),(Hom ((dom g),a))] `1 by MCART_1:7 .= Hom ((cod g),a) .= (Obj (hom?- ((Hom A),(cod g)))) . a by ENS_1:60 .= (hom?- ((Hom A),(cod g))) . a .= <|(cod g),?> . a by ENS_1:def_25 ; hence [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom ((<|(cod g),?> . a),(<|(dom g),?> . a)) by A10; ::_thesis: verum end; then A11: Hom ((<|(cod g),?> . o),(<|(dom g),?> . o)) <> {} ; for a being Object of A holds [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) proof let a be Object of A; ::_thesis: [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) A12: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13; then reconsider m = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] as Morphism of (EnsHom A) by ENS_1:48; reconsider m9 = m as Element of Maps (Hom A) by ENS_1:48; A13: cod m = (fCod (Hom A)) . m by A12 .= cod m9 by ENS_1:def_10 .= (m `1) `2 by ENS_1:def_4 .= [(Hom ((cod f),a)),(Hom ((dom f),a))] `2 by MCART_1:7 .= Hom ((dom f),a) .= (Obj (hom?- ((Hom A),(dom f)))) . a by ENS_1:60 .= (hom?- ((Hom A),(dom f))) . a .= <|(dom f),?> . a by ENS_1:def_25 ; dom m = (fDom (Hom A)) . m by A12 .= dom m9 by ENS_1:def_9 .= (m `1) `1 by ENS_1:def_3 .= [(Hom ((cod f),a)),(Hom ((dom f),a))] `1 by MCART_1:7 .= Hom ((cod f),a) .= (Obj (hom?- ((Hom A),(cod f)))) . a by ENS_1:60 .= (hom?- ((Hom A),(cod f))) . a .= <|(cod f),?> . a by ENS_1:def_25 ; hence [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A13; ::_thesis: verum end; then A14: Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) <> {} ; A15: <|(g (*) f),?> . o = [[(Hom ((cod g),o)),(Hom ((dom (g (*) f)),o))],(hom ((g (*) f),(id o)))] by A7, Def3 .= [[(Hom ((cod g),o)),(Hom ((dom f),o))],(hom ((g (*) f),o))] by A6, ENS_1:53 ; A16: t . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] by A4, Def3; A17: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13; then reconsider f19 = f1 as Element of Maps (Hom A) ; reconsider f29 = f2 as Element of Maps (Hom A) by A17; A18: cod f2 = (fCod (Hom A)) . f2 by A17 .= cod f29 by ENS_1:def_10 .= (f2 `1) `2 by ENS_1:def_4 .= [(Hom ((cod g),o)),(Hom ((dom g),o))] `2 by A8, MCART_1:7 .= Hom ((dom g),o) ; A19: cod f1 = (fCod (Hom A)) . f1 by A17 .= cod f19 by ENS_1:def_10 .= (f1 `1) `2 by ENS_1:def_4 .= [(Hom ((cod f),o)),(Hom ((dom f),o))] `2 by A16, MCART_1:7 .= Hom ((dom f),o) ; A20: dom f1 = (fDom (Hom A)) . f1 by A17 .= dom f19 by ENS_1:def_9 .= (f1 `1) `1 by ENS_1:def_3 .= [(Hom ((cod f),o)),(Hom ((dom f),o))] `1 by A16, MCART_1:7 .= Hom ((cod f),o) ; A21: dom f2 = (fDom (Hom A)) . f2 by A17 .= dom f29 by ENS_1:def_9 .= (f2 `1) `1 by ENS_1:def_3 .= [(Hom ((cod g),o)),(Hom ((dom g),o))] `1 by A8, MCART_1:7 .= Hom ((cod g),o) ; ( <|(dom g),?> is_naturally_transformable_to <|(dom f),?> & <|(cod g),?> is_naturally_transformable_to <|(dom g),?> ) by A4, Th2; then tt . o = (t . o) * (t1 . o) by A6, A7, NATTRA_1:25 .= f1 (*) f2 by A4, A14, A11, CAT_1:def_13 .= [[(Hom ((cod g),o)),(Hom ((dom f),o))],((hom (f,(id o))) * (hom (g,(id o))))] by A4, A16, A8, A20, A18, A21, A19, Th1 .= [[(Hom ((cod g),o)),(Hom ((dom f),o))],((hom (f,o)) * (hom (g,(id o))))] by ENS_1:53 .= [[(Hom ((cod g),o)),(Hom ((dom f),o))],((hom (f,o)) * (hom (g,o)))] by ENS_1:53 .= [[(Hom ((cod g),o)),(Hom ((dom f),o))],(hom ((g (*) f),o))] by A4, ENS_1:46 ; hence <|(g (*) f),?> . o = tt . o by A15; ::_thesis: verum end; then A22: <|(g (*) f),?> = tt by Th2, ISOCAT_1:26; A23: F . f = [[<|(dom g),?>,<|(dom f),?>],t] by A2, A4; then A24: [(F . f),(F . g)] in dom the Comp of (Functors (A,(EnsHom A))) by A5, NATTRA_1:35; then consider F9, F19, F29 being Functor of A, EnsHom A, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that A25: F . g = [[F9,F19],t9] and A26: F . f = [[F19,F29],t19] and A27: the Comp of (Functors (A,(EnsHom A))) . ((F . f),(F . g)) = [[F9,F29],(t19 `*` t9)] by NATTRA_1:def_17; A28: <|f,?> = t19 by A23, A26, XTUPLE_0:1; [F19,F29] = [<|(dom g),?>,<|(dom f),?>] by A23, A26, XTUPLE_0:1; then A29: <|(dom f),?> = F29 by XTUPLE_0:1; [F9,F19] = [<|(cod g),?>,<|(dom g),?>] by A5, A25, XTUPLE_0:1; then A30: ( <|(cod g),?> = F9 & <|(dom g),?> = F19 ) by XTUPLE_0:1; <|g,?> = t9 by A5, A25, XTUPLE_0:1; then (F . f) (*) (F . g) = [[<|(cod g),?>,<|(dom f),?>],(t `*` t1)] by A24, A27, A28, A30, A29, CAT_1:def_1; hence F . (g (*) f) = (F . f) (*) (F . g) by A2, A6, A7, A22; ::_thesis: verum end; A31: for f being Morphism of A holds ( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . f)) ) proof let f be Morphism of A; ::_thesis: ( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . f)) ) set g = F . f; set X = dom <|(id (dom f)),?>; A32: dom <|(id (dom f)),?> = the carrier of A by FUNCT_2:def_1 .= dom (id <|(dom f),?>) by FUNCT_2:def_1 ; A33: F . (id (dom f)) = [[<|(cod (id (dom f))),?>,<|(dom (id (dom f))),?>],<|(id (dom f)),?>] by A2 .= [[<|(dom f),?>,<|(dom (id (dom f))),?>],<|(id (dom f)),?>] by CAT_1:58 .= [[<|(dom f),?>,<|(dom f),?>],<|(id (dom f)),?>] by CAT_1:58 ; A34: F . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] by A2; then cod (F . f) = <|(dom f),?> by NATTRA_1:33; then A35: [[<|(dom f),?>,<|(dom f),?>],(id <|(dom f),?>)] = id (cod (F . f)) by NATTRA_1:def_17; A36: for y being set st y in dom <|(id (dom f)),?> holds <|(id (dom f)),?> . y = (id <|(dom f),?>) . y proof let y be set ; ::_thesis: ( y in dom <|(id (dom f)),?> implies <|(id (dom f)),?> . y = (id <|(dom f),?>) . y ) assume y in dom <|(id (dom f)),?> ; ::_thesis: <|(id (dom f)),?> . y = (id <|(dom f),?>) . y then reconsider z = y as Object of A by FUNCT_2:def_1; reconsider zz = id z as Morphism of z,z ; A37: Hom (z,z) <> {} ; A38: <|(cod (id (dom f))),?> is_transformable_to <|(dom (id (dom f))),?> ; <|(id (dom f)),?> . z = [[(Hom ((cod (id (dom f))),z)),(Hom ((dom (id (dom f))),z))],(hom ((id (dom f)),(id z)))] by Def3 .= [[(Hom ((dom f),z)),(Hom ((dom (id (dom f))),z))],(hom ((id (dom f)),(id z)))] .= [[(Hom ((dom f),z)),(Hom ((dom f),z))],(hom ((id (dom f)),(id z)))] .= [[(Hom ((dom f),z)),(Hom ((dom f),z))],(hom ((dom f),(id z)))] by ENS_1:53 .= [[(Hom ((dom f),z)),(Hom ((dom f),(cod (id z))))],(hom ((dom f),(id z)))] .= [[(Hom ((dom f),(dom (id z)))),(Hom ((dom f),(cod (id z))))],(hom ((dom f),(id z)))] .= <|(dom f),?> . (id z) by ENS_1:def_21 .= <|(dom f),?> /. zz by A37, CAT_3:def_10 .= id (<|(dom f),?> . z) by NATTRA_1:15 .= (id <|(dom f),?>) . z by NATTRA_1:20 .= (id <|(dom f),?>) . z by NATTRA_1:def_5 ; hence <|(id (dom f)),?> . y = (id <|(dom f),?>) . y by A38, NATTRA_1:def_5; ::_thesis: verum end; set X = dom <|(id (cod f)),?>; A39: for y being set st y in dom <|(id (cod f)),?> holds <|(id (cod f)),?> . y = (id <|(cod f),?>) . y proof let y be set ; ::_thesis: ( y in dom <|(id (cod f)),?> implies <|(id (cod f)),?> . y = (id <|(cod f),?>) . y ) assume y in dom <|(id (cod f)),?> ; ::_thesis: <|(id (cod f)),?> . y = (id <|(cod f),?>) . y then reconsider z = y as Object of A by FUNCT_2:def_1; A40: Hom (z,z) <> {} ; A41: <|(cod (id (cod f))),?> is_transformable_to <|(dom (id (cod f))),?> ; <|(id (cod f)),?> . z = [[(Hom ((cod (id (cod f))),z)),(Hom ((dom (id (cod f))),z))],(hom ((id (cod f)),(id z)))] by Def3 .= [[(Hom ((cod f),z)),(Hom ((dom (id (cod f))),z))],(hom ((id (cod f)),(id z)))] .= [[(Hom ((cod f),z)),(Hom ((cod f),z))],(hom ((id (cod f)),(id z)))] .= [[(Hom ((cod f),z)),(Hom ((cod f),z))],(hom ((cod f),(id z)))] by ENS_1:53 .= [[(Hom ((cod f),z)),(Hom ((cod f),(cod (id z))))],(hom ((cod f),(id z)))] .= [[(Hom ((cod f),(dom (id z)))),(Hom ((cod f),(cod (id z))))],(hom ((cod f),(id z)))] .= <|(cod f),?> . (id z) by ENS_1:def_21 .= <|(cod f),?> /. (id z) by A40, CAT_3:def_10 .= id (<|(cod f),?> . z) by NATTRA_1:15 .= (id <|(cod f),?>) . z by NATTRA_1:20 .= (id <|(cod f),?>) . z by NATTRA_1:def_5 ; hence <|(id (cod f)),?> . y = (id <|(cod f),?>) . y by A41, NATTRA_1:def_5; ::_thesis: verum end; dom <|(id (cod f)),?> = the carrier of A by FUNCT_2:def_1 .= dom (id <|(cod f),?>) by FUNCT_2:def_1 ; then A42: <|(id (cod f)),?> = id <|(cod f),?> by A39, FUNCT_1:2; A43: F . (id (cod f)) = [[<|(cod (id (cod f))),?>,<|(dom (id (cod f))),?>],<|(id (cod f)),?>] by A2 .= [[<|(cod f),?>,<|(dom (id (cod f))),?>],<|(id (cod f)),?>] by CAT_1:58 .= [[<|(cod f),?>,<|(cod f),?>],<|(id (cod f)),?>] by CAT_1:58 ; dom (F . f) = <|(cod f),?> by A34, NATTRA_1:33; hence ( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . f)) ) by A33, A35, A32, A36, A43, A42, FUNCT_1:2, NATTRA_1:def_17; ::_thesis: verum end; for c being Object of A ex d being Object of (Functors (A,(EnsHom A))) st F . (id c) = id d proof let c be Object of A; ::_thesis: ex d being Object of (Functors (A,(EnsHom A))) st F . (id c) = id d set X = dom <|(id c),?>; <|c,?> in Funct (A,(EnsHom A)) by CAT_2:def_2; then reconsider d = <|c,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def_17; take d ; ::_thesis: F . (id c) = id d A44: for y being set st y in dom <|(id c),?> holds <|(id c),?> . y = (id <|c,?>) . y proof let y be set ; ::_thesis: ( y in dom <|(id c),?> implies <|(id c),?> . y = (id <|c,?>) . y ) assume y in dom <|(id c),?> ; ::_thesis: <|(id c),?> . y = (id <|c,?>) . y then reconsider z = y as Object of A by FUNCT_2:def_1; reconsider zz = id z as Morphism of z,z ; A45: Hom (z,z) <> {} ; A46: <|(cod (id c)),?> is_transformable_to <|(dom (id c)),?> ; <|(id c),?> . z = [[(Hom ((cod (id c)),z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))] by Def3 .= [[(Hom (c,z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))] .= [[(Hom (c,z)),(Hom (c,z))],(hom ((id c),(id z)))] .= [[(Hom (c,z)),(Hom (c,z))],(hom (c,(id z)))] by ENS_1:53 .= [[(Hom (c,z)),(Hom (c,(cod (id z))))],(hom (c,(id z)))] .= [[(Hom (c,(dom (id z)))),(Hom (c,(cod (id z))))],(hom (c,(id z)))] .= <|c,?> . (id z) by ENS_1:def_21 .= <|c,?> /. zz by A45, CAT_3:def_10 .= id (<|c,?> . z) by NATTRA_1:15 .= (id <|c,?>) . z by NATTRA_1:20 .= (id <|c,?>) . z by NATTRA_1:def_5 ; hence <|(id c),?> . y = (id <|c,?>) . y by A46, NATTRA_1:def_5; ::_thesis: verum end; dom <|(id c),?> = the carrier of A by FUNCT_2:def_1 .= dom (id <|c,?>) by FUNCT_2:def_1 ; then A47: <|(id c),?> = id <|c,?> by A44, FUNCT_1:2; F . (id c) = [[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>] by A2 .= [[<|c,?>,<|(dom (id c)),?>],<|(id c),?>] by CAT_1:58 .= [[<|c,?>,<|c,?>],(id <|c,?>)] by A47, CAT_1:58 .= id d by NATTRA_1:def_17 ; hence F . (id c) = id d ; ::_thesis: verum end; then reconsider F = F as Contravariant_Functor of A, Functors (A,(EnsHom A)) by A31, A3, OPPCAT_1:def_9; for f being Element of the carrier' of A holds F . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] by A2; hence ex b1 being Contravariant_Functor of A, Functors (A,(EnsHom A)) st for f being Morphism of A holds b1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ; ::_thesis: verum end; uniqueness for b1, b2 being Contravariant_Functor of A, Functors (A,(EnsHom A)) st ( for f being Morphism of A holds b1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) & ( for f being Morphism of A holds b2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) holds b1 = b2 proof let h1, h2 be Contravariant_Functor of A, Functors (A,(EnsHom A)); ::_thesis: ( ( for f being Morphism of A holds h1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) & ( for f being Morphism of A holds h2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) implies h1 = h2 ) assume that A48: for f being Morphism of A holds h1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] and A49: for f being Morphism of A holds h2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ; ::_thesis: h1 = h2 now__::_thesis:_for_f_being_Morphism_of_A_holds_h1_._f_=_h2_._f let f be Morphism of A; ::_thesis: h1 . f = h2 . f thus h1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] by A48 .= h2 . f by A49 ; ::_thesis: verum end; hence h1 = h2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines Yoneda YONEDA_1:def_4_:_ for A being Category for b2 being Contravariant_Functor of A, Functors (A,(EnsHom A)) holds ( b2 = Yoneda A iff for f being Morphism of A holds b2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ); definition let A, B be Category; let F be Contravariant_Functor of A,B; let c be Object of A; funcF . c -> Object of B equals :: YONEDA_1:def 5 (Obj F) . c; correctness coherence (Obj F) . c is Object of B; ; end; :: deftheorem defines . YONEDA_1:def_5_:_ for A, B being Category for F being Contravariant_Functor of A,B for c being Object of A holds F . c = (Obj F) . c; theorem :: YONEDA_1:4 for A being Category for F being Functor of A, Functors (A,(EnsHom A)) st Obj F is one-to-one & F is faithful holds F is one-to-one proof let A be Category; ::_thesis: for F being Functor of A, Functors (A,(EnsHom A)) st Obj F is one-to-one & F is faithful holds F is one-to-one let F be Functor of A, Functors (A,(EnsHom A)); ::_thesis: ( Obj F is one-to-one & F is faithful implies F is one-to-one ) assume A1: Obj F is one-to-one ; ::_thesis: ( not F is faithful or F is one-to-one ) assume A2: F is faithful ; ::_thesis: F is one-to-one for x1, x2 being set st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 ) assume that A3: ( x1 in dom F & x2 in dom F ) and A4: F . x1 = F . x2 ; ::_thesis: x1 = x2 reconsider m1 = x1, m2 = x2 as Morphism of A by A3, FUNCT_2:def_1; set o1 = dom m1; set o2 = cod m1; set o3 = dom m2; set o4 = cod m2; reconsider m19 = m1 as Morphism of dom m1, cod m1 by CAT_1:4; reconsider m29 = m2 as Morphism of dom m2, cod m2 by CAT_1:4; A5: Hom ((dom m1),(cod m1)) <> {} by CAT_1:2; then A6: Hom ((F . (dom m1)),(F . (cod m1))) <> {} by CAT_1:84; A7: Hom ((dom m2),(cod m2)) <> {} by CAT_1:2; then A8: Hom ((F . (dom m2)),(F . (cod m2))) <> {} by CAT_1:84; A9: F /. m19 = F . m2 by A4, A5, CAT_3:def_10 .= F /. m29 by A7, CAT_3:def_10 ; (Obj F) . (dom m1) = F . (dom m1) .= dom (F /. m29) by A9, A6, CAT_1:5 .= (Obj F) . (dom m2) by A8, CAT_1:5 ; then A10: ( m2 is Morphism of dom m2, cod m2 & dom m1 = dom m2 ) by A1, CAT_1:4, FUNCT_2:19; (Obj F) . (cod m1) = F . (cod m1) .= cod (F /. m29) by A9, A6, CAT_1:5 .= (Obj F) . (cod m2) by A8, CAT_1:5 ; then ( m1 is Morphism of dom m1, cod m1 & m2 is Morphism of dom m1, cod m1 ) by A1, A10, CAT_1:4, FUNCT_2:19; hence x1 = x2 by A2, A4, A5, CAT_1:def_27; ::_thesis: verum end; hence F is one-to-one by FUNCT_1:def_4; ::_thesis: verum end; definition let C, D be Category; let T be Contravariant_Functor of C,D; attrT is faithful means :Def6: :: YONEDA_1:def 6 for c, c9 being Object of C st Hom (c,c9) <> {} holds for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds f1 = f2; end; :: deftheorem Def6 defines faithful YONEDA_1:def_6_:_ for C, D being Category for T being Contravariant_Functor of C,D holds ( T is faithful iff for c, c9 being Object of C st Hom (c,c9) <> {} holds for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds f1 = f2 ); theorem Th5: :: YONEDA_1:5 for A being Category for F being Contravariant_Functor of A, Functors (A,(EnsHom A)) st Obj F is one-to-one & F is faithful holds F is one-to-one proof let A be Category; ::_thesis: for F being Contravariant_Functor of A, Functors (A,(EnsHom A)) st Obj F is one-to-one & F is faithful holds F is one-to-one let F be Contravariant_Functor of A, Functors (A,(EnsHom A)); ::_thesis: ( Obj F is one-to-one & F is faithful implies F is one-to-one ) assume A1: Obj F is one-to-one ; ::_thesis: ( not F is faithful or F is one-to-one ) assume A2: F is faithful ; ::_thesis: F is one-to-one for x1, x2 being set st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 ) assume that A3: ( x1 in dom F & x2 in dom F ) and A4: F . x1 = F . x2 ; ::_thesis: x1 = x2 reconsider m1 = x1, m2 = x2 as Morphism of A by A3, FUNCT_2:def_1; set o1 = dom m1; set o2 = cod m1; set o3 = dom m2; set o4 = cod m2; reconsider m29 = m2 as Morphism of dom m2, cod m2 by CAT_1:4; (Obj F) . (dom m1) = cod (F . m29) by A4, OPPCAT_1:32 .= (Obj F) . (dom m2) by OPPCAT_1:32 ; then A5: ( m2 is Morphism of dom m2, cod m2 & dom m1 = dom m2 ) by A1, CAT_1:4, FUNCT_2:19; A6: ( m1 is Morphism of dom m1, cod m1 & Hom ((dom m1),(cod m1)) <> {} ) by CAT_1:2, CAT_1:4; (Obj F) . (cod m1) = dom (F . m29) by A4, OPPCAT_1:32 .= (Obj F) . (cod m2) by OPPCAT_1:32 ; then m2 is Morphism of dom m1, cod m1 by A1, A5, FUNCT_2:19; hence x1 = x2 by A2, A4, A6, Def6; ::_thesis: verum end; hence F is one-to-one by FUNCT_1:def_4; ::_thesis: verum end; registration let A be Category; cluster Yoneda A -> faithful ; coherence Yoneda A is faithful proof set F = Yoneda A; for o1, o2 being Object of A st Hom (o1,o2) <> {} holds for x1, x2 being Morphism of o1,o2 st (Yoneda A) . x1 = (Yoneda A) . x2 holds x1 = x2 proof let o1, o2 be Object of A; ::_thesis: ( Hom (o1,o2) <> {} implies for x1, x2 being Morphism of o1,o2 st (Yoneda A) . x1 = (Yoneda A) . x2 holds x1 = x2 ) assume A1: Hom (o1,o2) <> {} ; ::_thesis: for x1, x2 being Morphism of o1,o2 st (Yoneda A) . x1 = (Yoneda A) . x2 holds x1 = x2 let x1, x2 be Morphism of o1,o2; ::_thesis: ( (Yoneda A) . x1 = (Yoneda A) . x2 implies x1 = x2 ) A2: x2 in Hom (o1,o2) by A1, CAT_1:def_5; assume (Yoneda A) . x1 = (Yoneda A) . x2 ; ::_thesis: x1 = x2 then [[<|(cod x1),?>,<|(dom x1),?>],<|x1,?>] = (Yoneda A) . x2 by Def4; then [[<|(cod x1),?>,<|(dom x1),?>],<|x1,?>] = [[<|(cod x2),?>,<|(dom x2),?>],<|x2,?>] by Def4; then [<|(cod x1),?>,<|(dom x1),?>,<|x1,?>] = [[<|(cod x2),?>,<|(dom x2),?>],<|x2,?>] ; then [<|(cod x1),?>,<|(dom x1),?>,<|x1,?>] = [<|(cod x2),?>,<|(dom x2),?>,<|x2,?>] ; then A3: <|x1,?> = <|x2,?> by XTUPLE_0:3; A4: x1 in Hom (o1,o2) by A1, CAT_1:def_5; then A5: dom x1 = o1 by CAT_1:1 .= dom x2 by A2, CAT_1:1 ; cod x1 = o2 by A4, CAT_1:1 .= cod x2 by A2, CAT_1:1 ; then [[(Hom ((cod x1),o2)),(Hom ((dom x1),o2))],(hom (x1,(id o2)))] = <|x2,?> . o2 by A5, A3, Def3; then [[(Hom ((cod x1),o2)),(Hom ((dom x1),o2))],(hom (x1,(id o2)))] = [[(Hom ((cod x2),o2)),(Hom ((dom x2),o2))],(hom (x2,(id o2)))] by Def3; then [[(Hom (o2,o2)),(Hom ((dom x1),o2))],(hom (x1,(id o2)))] = [[(Hom ((cod x2),o2)),(Hom ((dom x2),o2))],(hom (x2,(id o2)))] by A4, CAT_1:1; then [[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x1,(id o2)))] = [[(Hom ((cod x2),o2)),(Hom ((dom x2),o2))],(hom (x2,(id o2)))] by A4, CAT_1:1; then [[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x1,(id o2)))] = [[(Hom (o2,o2)),(Hom ((dom x2),o2))],(hom (x2,(id o2)))] by A2, CAT_1:1; then [[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x1,(id o2)))] = [[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x2,(id o2)))] by A2, CAT_1:1; then [[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x1,(id o2)))] = [(Hom (o2,o2)),(Hom (o1,o2)),(hom (x2,(id o2)))] ; then A6: [(Hom (o2,o2)),(Hom (o1,o2)),(hom (x1,(id o2)))] = [(Hom (o2,o2)),(Hom (o1,o2)),(hom (x2,(id o2)))] ; reconsider dd = id o2 as Morphism of A ; A7: Hom (o2,o2) <> {} ; then A8: (id o2) (*) dd = (id o2) * (id o2) by CAT_1:def_13; id o2 in Hom (o2,o2) by CAT_1:27; then id o2 in Hom ((cod x2),o2) by A2, CAT_1:1; then id o2 in Hom ((cod x2),(dom (id o2))) ; then A9: (hom (x2,(id o2))) . dd = ((id o2) * (id o2)) (*) x2 by A8, ENS_1:def_23 .= (id o2) (*) x2 .= (id o2) * x2 by A1, A7, CAT_1:def_13 .= x2 by A1, CAT_1:28 ; id o2 in Hom (o2,o2) by CAT_1:27; then id o2 in Hom ((cod x1),o2) by A4, CAT_1:1; then id o2 in Hom ((cod x1),(dom (id o2))) ; then (hom (x1,(id o2))) . dd = ((id o2) * (id o2)) (*) x1 by A8, ENS_1:def_23 .= (id o2) (*) x1 .= (id o2) * x1 by A1, A7, CAT_1:def_13 .= x1 by A1, CAT_1:28 ; hence x1 = x2 by A9, A6, XTUPLE_0:3; ::_thesis: verum end; hence Yoneda A is faithful by Def6; ::_thesis: verum end; end; registration let A be Category; cluster Yoneda A -> one-to-one ; coherence Yoneda A is one-to-one proof set F = Yoneda A; for x1, x2 being set st x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) & (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) & (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 implies x1 = x2 ) assume that A1: ( x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) ) and A2: (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 ; ::_thesis: x1 = x2 reconsider c = x1, c1 = x2 as Object of A by A1, FUNCT_2:def_1; reconsider f = id c1 as Morphism of c1,c1 ; A3: Hom (c1,c1) <> {} ; <|c1,?> in Funct (A,(EnsHom A)) by CAT_2:def_2; then reconsider d1 = <|c1,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def_17; <|c,?> in Funct (A,(EnsHom A)) by CAT_2:def_2; then reconsider d = <|c,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def_17; (Yoneda A) . (id c1) = id d1 proof set X = dom <|(id c1),?>; A4: for y being set st y in dom <|(id c1),?> holds <|(id c1),?> . y = (id <|c1,?>) . y proof let y be set ; ::_thesis: ( y in dom <|(id c1),?> implies <|(id c1),?> . y = (id <|c1,?>) . y ) assume y in dom <|(id c1),?> ; ::_thesis: <|(id c1),?> . y = (id <|c1,?>) . y then reconsider z = y as Object of A by FUNCT_2:def_1; reconsider zz = id z as Morphism of z,z ; A5: Hom (z,z) <> {} ; A6: <|(cod (id c1)),?> is_transformable_to <|(dom (id c1)),?> ; <|(id c1),?> . z = [[(Hom ((cod (id c1)),z)),(Hom ((dom (id c1)),z))],(hom ((id c1),(id z)))] by Def3 .= [[(Hom (c1,z)),(Hom ((dom (id c1)),z))],(hom ((id c1),(id z)))] .= [[(Hom (c1,z)),(Hom (c1,z))],(hom ((id c1),(id z)))] .= [[(Hom (c1,z)),(Hom (c1,z))],(hom (c1,(id z)))] by ENS_1:53 .= [[(Hom (c1,z)),(Hom (c1,(cod (id z))))],(hom (c1,(id z)))] .= [[(Hom (c1,(dom (id z)))),(Hom (c1,(cod (id z))))],(hom (c1,(id z)))] .= <|c1,?> . (id z) by ENS_1:def_21 .= <|c1,?> /. zz by A5, CAT_3:def_10 .= id (<|c1,?> . z) by NATTRA_1:15 .= (id <|c1,?>) . z by NATTRA_1:20 .= (id <|c1,?>) . z by NATTRA_1:def_5 ; hence <|(id c1),?> . y = (id <|c1,?>) . y by A6, NATTRA_1:def_5; ::_thesis: verum end; dom <|(id c1),?> = the carrier of A by FUNCT_2:def_1 .= dom (id <|c1,?>) by FUNCT_2:def_1 ; then A7: <|(id c1),?> = id <|c1,?> by A4, FUNCT_1:2; (Yoneda A) . (id c1) = [[<|(cod (id c1)),?>,<|(dom (id c1)),?>],<|(id c1),?>] by Def4 .= [[<|c1,?>,<|(dom (id c1)),?>],<|(id c1),?>] by CAT_1:58 .= [[<|c1,?>,<|c1,?>],(id <|c1,?>)] by A7, CAT_1:58 .= id d1 by NATTRA_1:def_17 ; hence (Yoneda A) . (id c1) = id d1 ; ::_thesis: verum end; then A8: (Obj (Yoneda A)) . c1 = d1 by OPPCAT_1:30; (Yoneda A) . (id c) = id d proof set X = dom <|(id c),?>; A9: for y being set st y in dom <|(id c),?> holds <|(id c),?> . y = (id <|c,?>) . y proof let y be set ; ::_thesis: ( y in dom <|(id c),?> implies <|(id c),?> . y = (id <|c,?>) . y ) assume y in dom <|(id c),?> ; ::_thesis: <|(id c),?> . y = (id <|c,?>) . y then reconsider z = y as Object of A by FUNCT_2:def_1; reconsider zz = id z as Morphism of z,z ; A10: Hom (z,z) <> {} ; A11: <|(cod (id c)),?> is_transformable_to <|(dom (id c)),?> ; <|(id c),?> . z = [[(Hom ((cod (id c)),z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))] by Def3 .= [[(Hom (c,z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))] .= [[(Hom (c,z)),(Hom (c,z))],(hom ((id c),(id z)))] .= [[(Hom (c,z)),(Hom (c,z))],(hom (c,(id z)))] by ENS_1:53 .= [[(Hom (c,z)),(Hom (c,(cod (id z))))],(hom (c,(id z)))] .= [[(Hom (c,(dom (id z)))),(Hom (c,(cod (id z))))],(hom (c,(id z)))] .= <|c,?> . (id z) by ENS_1:def_21 .= <|c,?> /. zz by A10, CAT_3:def_10 .= id (<|c,?> . z) by NATTRA_1:15 .= (id <|c,?>) . z by NATTRA_1:20 .= (id <|c,?>) . z by NATTRA_1:def_5 ; hence <|(id c),?> . y = (id <|c,?>) . y by A11, NATTRA_1:def_5; ::_thesis: verum end; dom <|(id c),?> = the carrier of A by FUNCT_2:def_1 .= dom (id <|c,?>) by FUNCT_2:def_1 ; then A12: <|(id c),?> = id <|c,?> by A9, FUNCT_1:2; (Yoneda A) . (id c) = [[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>] by Def4 .= [[<|c,?>,<|(dom (id c)),?>],<|(id c),?>] by CAT_1:58 .= [[<|c,?>,<|c,?>],(id <|c,?>)] by A12, CAT_1:58 .= id d by NATTRA_1:def_17 ; hence (Yoneda A) . (id c) = id d ; ::_thesis: verum end; then (Obj (Yoneda A)) . c = d by OPPCAT_1:30; then [[(Hom (c,(dom f))),(Hom (c,(cod f)))],(hom (c,f))] = (hom?- c1) . f by A2, A8, ENS_1:def_21; then [[(Hom (c,(dom f))),(Hom (c,(cod f)))],(hom (c,f))] = [[(Hom (c1,(dom f))),(Hom (c1,(cod f)))],(hom (c1,f))] by ENS_1:def_21; then [(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [[(Hom (c1,(dom f))),(Hom (c1,(cod f)))],(hom (c1,f))] ; then [(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [(Hom (c1,(dom f))),(Hom (c1,(cod f))),(hom (c1,f))] ; then Hom (c,(dom f)) = Hom (c1,(dom f)) by XTUPLE_0:3; then Hom (c,(dom f)) = Hom (c1,c1) by CAT_1:5; then A13: Hom (c,c1) = Hom (c1,c1) by CAT_1:5; id c1 in Hom (c1,c1) by CAT_1:27; then reconsider h = id c1 as Morphism of c,c1 by A13, CAT_1:def_5; dom h = c by A13, CAT_1:5; hence x1 = x2 by A3, CAT_1:5; ::_thesis: verum end; then Obj (Yoneda A) is one-to-one by FUNCT_1:def_4; hence Yoneda A is one-to-one by Th5; ::_thesis: verum end; end; definition let C, D be Category; let T be Contravariant_Functor of C,D; attrT is full means :Def7: :: YONEDA_1:def 7 for c, c9 being Object of C st Hom ((T . c9),(T . c)) <> {} holds for g being Morphism of T . c9,T . c holds ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ); end; :: deftheorem Def7 defines full YONEDA_1:def_7_:_ for C, D being Category for T being Contravariant_Functor of C,D holds ( T is full iff for c, c9 being Object of C st Hom ((T . c9),(T . c)) <> {} holds for g being Morphism of T . c9,T . c holds ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) ); registration let A be Category; cluster Yoneda A -> full ; coherence Yoneda A is full proof set F = Yoneda A; for c, c9 being Object of A st Hom (((Yoneda A) . c9),((Yoneda A) . c)) <> {} holds for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f ) proof let c, c9 be Object of A; ::_thesis: ( Hom (((Yoneda A) . c9),((Yoneda A) . c)) <> {} implies for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f ) ) assume A1: Hom (((Yoneda A) . c9),((Yoneda A) . c)) <> {} ; ::_thesis: for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f ) A2: <|c9,?> . c9 = (hom?- ((Hom A),c9)) . c9 by ENS_1:def_25 .= (Obj (hom?- ((Hom A),c9))) . c9 .= Hom (c9,c9) by ENS_1:60 ; let g be Morphism of (Yoneda A) . c9,(Yoneda A) . c; ::_thesis: ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f ) g in the carrier' of (Functors (A,(EnsHom A))) ; then g in NatTrans (A,(EnsHom A)) by NATTRA_1:def_17; then consider F1, F2 being Functor of A, EnsHom A, t being natural_transformation of F1,F2 such that A3: g = [[F1,F2],t] and A4: F1 is_naturally_transformable_to F2 by NATTRA_1:def_16; A5: dom g = F1 by A3, NATTRA_1:33; <|c9,?> in Funct (A,(EnsHom A)) by CAT_2:def_2; then reconsider d1 = <|c9,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def_17; <|c,?> in Funct (A,(EnsHom A)) by CAT_2:def_2; then reconsider d = <|c,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def_17; A6: (Yoneda A) . (id c) = id d proof set X = dom <|(id c),?>; A7: for y being set st y in dom <|(id c),?> holds <|(id c),?> . y = (id <|c,?>) . y proof let y be set ; ::_thesis: ( y in dom <|(id c),?> implies <|(id c),?> . y = (id <|c,?>) . y ) assume y in dom <|(id c),?> ; ::_thesis: <|(id c),?> . y = (id <|c,?>) . y then reconsider z = y as Object of A by FUNCT_2:def_1; reconsider zz = id z as Morphism of z,z ; A8: Hom (z,z) <> {} ; A9: <|(cod (id c)),?> is_transformable_to <|(dom (id c)),?> ; <|(id c),?> . z = [[(Hom ((cod (id c)),z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))] by Def3 .= [[(Hom (c,z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))] .= [[(Hom (c,z)),(Hom (c,z))],(hom ((id c),(id z)))] .= [[(Hom (c,z)),(Hom (c,z))],(hom (c,(id z)))] by ENS_1:53 .= [[(Hom (c,z)),(Hom (c,(cod (id z))))],(hom (c,(id z)))] .= [[(Hom (c,(dom (id z)))),(Hom (c,(cod (id z))))],(hom (c,(id z)))] .= <|c,?> . (id z) by ENS_1:def_21 .= <|c,?> /. zz by A8, CAT_3:def_10 .= id (<|c,?> . z) by NATTRA_1:15 .= (id <|c,?>) . z by NATTRA_1:20 .= (id <|c,?>) . z by NATTRA_1:def_5 ; hence <|(id c),?> . y = (id <|c,?>) . y by A9, NATTRA_1:def_5; ::_thesis: verum end; dom <|(id c),?> = the carrier of A by FUNCT_2:def_1 .= dom (id <|c,?>) by FUNCT_2:def_1 ; then A10: <|(id c),?> = id <|c,?> by A7, FUNCT_1:2; (Yoneda A) . (id c) = [[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>] by Def4 .= [[<|c,?>,<|(dom (id c)),?>],<|(id c),?>] by CAT_1:58 .= [[<|c,?>,<|c,?>],(id <|c,?>)] by A10, CAT_1:58 .= id d by NATTRA_1:def_17 ; hence (Yoneda A) . (id c) = id d ; ::_thesis: verum end; then A11: (Yoneda A) . c = d by OPPCAT_1:30; A12: (Yoneda A) . (id c9) = id d1 proof set X = dom <|(id c9),?>; A13: for y being set st y in dom <|(id c9),?> holds <|(id c9),?> . y = (id <|c9,?>) . y proof let y be set ; ::_thesis: ( y in dom <|(id c9),?> implies <|(id c9),?> . y = (id <|c9,?>) . y ) assume y in dom <|(id c9),?> ; ::_thesis: <|(id c9),?> . y = (id <|c9,?>) . y then reconsider z = y as Object of A by FUNCT_2:def_1; reconsider zz = id z as Morphism of z,z ; A14: Hom (z,z) <> {} ; A15: <|(cod (id c9)),?> is_transformable_to <|(dom (id c9)),?> ; <|(id c9),?> . z = [[(Hom ((cod (id c9)),z)),(Hom ((dom (id c9)),z))],(hom ((id c9),(id z)))] by Def3 .= [[(Hom (c9,z)),(Hom ((dom (id c9)),z))],(hom ((id c9),(id z)))] .= [[(Hom (c9,z)),(Hom (c9,z))],(hom ((id c9),(id z)))] .= [[(Hom (c9,z)),(Hom (c9,z))],(hom (c9,(id z)))] by ENS_1:53 .= [[(Hom (c9,z)),(Hom (c9,(cod (id z))))],(hom (c9,(id z)))] .= [[(Hom (c9,(dom (id z)))),(Hom (c9,(cod (id z))))],(hom (c9,(id z)))] .= <|c9,?> . (id z) by ENS_1:def_21 .= <|c9,?> /. zz by A14, CAT_3:def_10 .= id (<|c9,?> . z) by NATTRA_1:15 .= (id <|c9,?>) . z by NATTRA_1:20 .= (id <|c9,?>) . z by NATTRA_1:def_5 ; hence <|(id c9),?> . y = (id <|c9,?>) . y by A15, NATTRA_1:def_5; ::_thesis: verum end; dom <|(id c9),?> = the carrier of A by FUNCT_2:def_1 .= dom (id <|c9,?>) by FUNCT_2:def_1 ; then A16: <|(id c9),?> = id <|c9,?> by A13, FUNCT_1:2; (Yoneda A) . (id c9) = [[<|(cod (id c9)),?>,<|(dom (id c9)),?>],<|(id c9),?>] by Def4 .= [[<|c9,?>,<|(dom (id c9)),?>],<|(id c9),?>] by CAT_1:58 .= [[<|c9,?>,<|c9,?>],(id <|c9,?>)] by A16, CAT_1:58 .= id d1 by NATTRA_1:def_17 ; hence (Yoneda A) . (id c9) = id d1 ; ::_thesis: verum end; then A17: (Obj (Yoneda A)) . c9 = d1 by OPPCAT_1:30; A18: cod g = F2 by A3, NATTRA_1:33; then A19: F2 = (Yoneda A) . c by A1, CAT_1:5; A20: (Yoneda A) . c9 = d1 by A12, OPPCAT_1:30; A21: <|c,?> . c9 = (hom?- ((Hom A),c)) . c9 by ENS_1:def_25 .= (Obj (hom?- ((Hom A),c))) . c9 .= Hom (c,c9) by ENS_1:60 ; A22: ( dom g = (Yoneda A) . c9 & cod g = (Yoneda A) . c ) by A1, CAT_1:5; then reconsider t = t as natural_transformation of <|c9,?>,<|c,?> by A5, A18, A12, A11, OPPCAT_1:30; (Obj (Yoneda A)) . c = d by A6, OPPCAT_1:30; then <|c9,?> is_transformable_to <|c,?> by A4, A5, A18, A22, A20, NATTRA_1:def_7; then Hom ((<|c9,?> . c9),(<|c,?> . c9)) <> {} by NATTRA_1:def_2; then A23: t . c9 in Hom ((<|c9,?> . c9),(<|c,?> . c9)) by CAT_1:def_5; then A24: cod (t . c9) = <|c,?> . c9 by CAT_1:1; A25: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13; then reconsider t1 = t . c9 as Element of Maps (Hom A) ; A26: cod (t . c9) = (fCod (Hom A)) . (t . c9) by A25 .= cod t1 by ENS_1:def_10 ; t1 in Maps ((dom t1),(cod t1)) by ENS_1:19; then A27: t1 `2 in Funcs ((dom t1),(cod t1)) by ENS_1:20; A28: dom (t . c9) = <|c9,?> . c9 by A23, CAT_1:1; then the Source of (EnsHom A) . (t . c9) <> {} by A2; then dom t1 <> {} by A25, ENS_1:def_9; then A29: cod t1 <> {} by A27; then A30: cod (t . c9) <> {} by A25, ENS_1:def_10; hence Hom (c,c9) <> {} by A21, A23, CAT_1:1; ::_thesis: ex f being Morphism of c,c9 st g = (Yoneda A) . f dom (t . c9) = (fDom (Hom A)) . (t . c9) by A25 .= dom t1 by ENS_1:def_9 ; then A31: t1 `2 is Function of (<|c9,?> . c9),(<|c,?> . c9) by A28, A24, A27, A26, FUNCT_2:66; then A32: dom (t1 `2) = Hom (c9,c9) by A2, A24, A30, FUNCT_2:def_1; then id c9 in dom (t1 `2) by CAT_1:27; then A33: (t1 `2) . (id c9) in rng (t1 `2) by FUNCT_1:def_3; rng (t1 `2) c= Hom (c,c9) by A21, A31, RELAT_1:def_19; then (t1 `2) . (id c9) in Hom (c,c9) by A33; then reconsider f = (t1 `2) . (id c9) as Morphism of c,c9 by CAT_1:def_5; A34: <|c,?> . c9 <> {} by A24, A25, A29, ENS_1:def_10; then A35: dom f = c by A21, CAT_1:5; take f ; ::_thesis: g = (Yoneda A) . f A36: cod f = c9 by A21, A34, CAT_1:5; A37: F1 = (Yoneda A) . c9 by A1, A5, CAT_1:5; then A38: <|c9,?> is_transformable_to <|c,?> by A4, A19, A17, A11, NATTRA_1:def_7; for a being Object of A holds <|f,?> . a = t . a proof let a be Object of A; ::_thesis: <|f,?> . a = t . a A39: <|c,?> . a = (hom?- ((Hom A),c)) . a by ENS_1:def_25 .= (Obj (hom?- ((Hom A),c))) . a .= Hom (c,a) by ENS_1:60 ; reconsider ta1 = t . a as Element of Maps (Hom A) by A25; A40: <|c9,?> . a = (hom?- ((Hom A),c9)) . a by ENS_1:def_25 .= (Obj (hom?- ((Hom A),c9))) . a .= Hom (c9,a) by ENS_1:60 ; ta1 in Maps ((dom ta1),(cod ta1)) by ENS_1:19; then A41: ta1 `2 in Funcs ((dom ta1),(cod ta1)) by ENS_1:20; then A42: ta1 `2 is Function of (dom ta1),(cod ta1) by FUNCT_2:66; set X = dom (ta1 `2); A43: dom (t . a) = (fDom (Hom A)) . (t . a) by A25 .= dom ta1 by ENS_1:def_9 ; A44: Hom ((<|c9,?> . a),(<|c,?> . a)) <> {} by A38, NATTRA_1:def_2; then A45: dom (t . a) = <|c9,?> . a by CAT_1:5; A46: cod (t . a) = <|c,?> . a by A44, CAT_1:5; A47: cod (t . a) = (fCod (Hom A)) . (t . a) by A25 .= cod ta1 by ENS_1:def_10 ; then A48: ta1 = [[(<|c9,?> . a),(<|c,?> . a)],(ta1 `2)] by A45, A46, A43, ENS_1:8; A49: ta1 `2 is Function of (dom (t . a)),(cod (t . a)) by A43, A47, A41, FUNCT_2:66; A50: dom (ta1 `2) = Hom (c9,a) proof percases ( Hom (c9,a) = {} or Hom (c9,a) <> {} ) ; suppose Hom (c9,a) = {} ; ::_thesis: dom (ta1 `2) = Hom (c9,a) hence dom (ta1 `2) = Hom (c9,a) by A45, A43, A40, A42; ::_thesis: verum end; suppose Hom (c9,a) <> {} ; ::_thesis: dom (ta1 `2) = Hom (c9,a) then Hom ((dom f),a) <> {} by A36, ENS_1:42; hence dom (ta1 `2) = Hom (c9,a) by A35, A45, A46, A40, A39, A49, FUNCT_2:def_1; ::_thesis: verum end; end; end; A51: for x being set st x in dom (ta1 `2) holds (hom (f,(id a))) . x = (ta1 `2) . x proof reconsider t1 = t . c9 as Element of Maps (Hom A) by A25; let x be set ; ::_thesis: ( x in dom (ta1 `2) implies (hom (f,(id a))) . x = (ta1 `2) . x ) A52: f in Hom (c,(cod f)) by A35; assume A53: x in dom (ta1 `2) ; ::_thesis: (hom (f,(id a))) . x = (ta1 `2) . x then reconsider y = x as Morphism of cod f,a by A36, A50, CAT_1:def_5; reconsider h = y as Morphism of c9,a by A21, A24, A30, CAT_1:5; A54: dom h = c9 by A50, A53, CAT_1:5; reconsider tc9 = <|c9,?> . h as Element of Maps (Hom A) by A25; A55: cod h = a by A50, A53, CAT_1:5; reconsider tch = <|c,?> . h as Element of Maps (Hom A) by A25; A56: [[(Hom (c,(dom h))),(Hom (c,(cod h)))],(hom (c,h))] = <|c,?> . h by ENS_1:def_21 .= <|c,?> . h ; A57: [[(Hom (c9,(dom h))),(Hom (c9,(cod h)))],(hom (c9,h))] = <|c9,?> . h by ENS_1:def_21 .= <|c9,?> . h ; A58: cod (<|c9,?> . h) = (fCod (Hom A)) . (<|c9,?> . h) by A25 .= cod tc9 by ENS_1:def_10 ; then A59: cod (<|c9,?> . h) = (tc9 `1) `2 by ENS_1:def_4 .= [(Hom (c9,(dom h))),(Hom (c9,(cod h)))] `2 by A57, MCART_1:7 .= Hom (c9,(cod h)) ; then A60: [(t . a),(<|c9,?> . h)] in dom the Comp of (EnsHom A) by A45, A40, A55, CAT_1:15; tc9 in Maps ((dom tc9),(cod tc9)) by ENS_1:19; then A61: tc9 `2 in Funcs ((dom tc9),(cod tc9)) by ENS_1:20; A62: dom (<|c9,?> . h) = (fDom (Hom A)) . (<|c9,?> . h) by A25 .= dom tc9 by ENS_1:def_9 ; then dom (<|c9,?> . h) = (tc9 `1) `1 by ENS_1:def_3 .= [(Hom (c9,(dom h))),(Hom (c9,(cod h)))] `1 by A57, MCART_1:7 .= Hom (c9,(dom h)) ; then tc9 `2 is Function of (Hom (c9,(dom h))),(Hom (c9,(cod h))) by A62, A58, A59, A61, FUNCT_2:66; then A63: dom (tc9 `2) = Hom (c9,c9) by A50, A53, A54, A55, FUNCT_2:def_1; A64: dom y = cod f by A36, A50, A53, CAT_1:5; tch = [[(dom tch),(cod tch)],(tch `2)] by ENS_1:8; then [(Hom (c,(dom h))),(Hom (c,(cod h))),(hom (c,h))] = [[(dom tch),(cod tch)],(tch `2)] by A56; then [(Hom (c,(dom h))),(Hom (c,(cod h))),(hom (c,h))] = [(dom tch),(cod tch),(tch `2)] ; then A65: hom (c,h) = tch `2 by XTUPLE_0:3; tc9 = [[(dom tc9),(cod tc9)],(tc9 `2)] by ENS_1:8; then [(dom tc9),(cod tc9),(tc9 `2)] = [[(Hom (c9,(dom h))),(Hom (c9,(cod h)))],(hom (c9,h))] by A57; then [(dom tc9),(cod tc9),(tc9 `2)] = [(Hom (c9,(dom h))),(Hom (c9,(cod h))),(hom (c9,h))] ; then A66: tc9 `2 = hom (c9,h) by XTUPLE_0:3; A67: Hom ((<|c9,?> . c9),(<|c,?> . c9)) <> {} by A38, NATTRA_1:def_2; then t . c9 in Hom ((<|c9,?> . c9),(<|c,?> . c9)) by CAT_1:def_5; then A68: cod (t . c9) = <|c,?> . c9 by CAT_1:1; dom (<|c,?> . h) = (fDom (Hom A)) . (<|c,?> . h) by A25 .= dom tch by ENS_1:def_9 ; then dom (<|c,?> . h) = (tch `1) `1 by ENS_1:def_3 .= [(Hom (c,(dom h))),(Hom (c,(cod h)))] `1 by A56, MCART_1:7 .= Hom (c,(dom h)) ; then A69: [(<|c,?> . h),(t . c9)] in dom the Comp of (EnsHom A) by A21, A54, A68, CAT_1:15; cod (t . c9) = (fCod (Hom A)) . (t . c9) by A25 .= cod t1 by ENS_1:def_10 ; then A70: cod t1 = [(Hom (c,(dom h))),(Hom (c,(cod h)))] `1 by A21, A54, A68 .= (tch `1) `1 by A56, MCART_1:7 .= dom tch by ENS_1:def_3 ; A71: h in Hom (c9,a) by A50, A53; then A72: <|c,?> /. h = <|c,?> . h by CAT_3:def_10; Hom ((<|c,?> . c9),(<|c,?> . a)) <> {} by A50, A53, CAT_1:84; then A73: (<|c,?> /. h) * (t . c9) = (<|c,?> . h) (*) (t . c9) by A67, A72, CAT_1:def_13 .= (fComp (Hom A)) . (tch,t1) by A25, A69, CAT_1:def_1 .= tch * t1 by A70, ENS_1:def_11 .= [[(dom t1),(cod tch)],((tch `2) * (t1 `2))] by A70, ENS_1:def_6 ; A74: cod tc9 = (tc9 `1) `2 by ENS_1:def_4 .= [(Hom (c9,(dom h))),(Hom (c9,(cod h)))] `2 by A57, MCART_1:7 .= dom ta1 by A45, A43, A40, A55 ; A75: <|c9,?> /. h = <|c9,?> . h by A71, CAT_3:def_10; Hom ((<|c9,?> . c9),(<|c9,?> . a)) <> {} by A50, A53, CAT_1:84; then A76: (t . a) * (<|c9,?> /. h) = (t . a) (*) (<|c9,?> . h) by A44, A75, CAT_1:def_13 .= (fComp (Hom A)) . (ta1,tc9) by A25, A60, CAT_1:def_1 .= ta1 * tc9 by A74, ENS_1:def_11 .= [[(dom tc9),(cod ta1)],((ta1 `2) * (tc9 `2))] by A74, ENS_1:def_6 ; (t . a) * (<|c9,?> /. h) = (<|c,?> /. h) * (t . c9) by A4, A37, A19, A17, A11, A50, A53, NATTRA_1:def_8; then [(dom tc9),(cod ta1),((ta1 `2) * (tc9 `2))] = [[(dom t1),(cod tch)],((tch `2) * (t1 `2))] by A76, A73; then [(dom tc9),(cod ta1),((ta1 `2) * (tc9 `2))] = [(dom t1),(cod tch),((tch `2) * (t1 `2))] ; then A77: (ta1 `2) * (tc9 `2) = (tch `2) * (t1 `2) by XTUPLE_0:3; A78: id c9 in Hom (c9,(cod f)) by A36, CAT_1:27; (hom (f,(id a))) . x = (hom (f,a)) . y by ENS_1:53 .= y (*) f by A36, A50, A53, ENS_1:def_20 .= (tch `2) . ((t1 `2) . (id c9)) by A64, A65, A52, ENS_1:def_19 .= ((ta1 `2) * (tc9 `2)) . (id c9) by A32, A77, CAT_1:27, FUNCT_1:13 .= (ta1 `2) . ((hom (c9,h)) . (id c9)) by A66, A63, CAT_1:27, FUNCT_1:13 .= (ta1 `2) . (y (*) (id c9)) by A64, A78, ENS_1:def_19 .= (ta1 `2) . x by A36, A64, CAT_1:22 ; hence (hom (f,(id a))) . x = (ta1 `2) . x ; ::_thesis: verum end; dom (hom (f,a)) = Hom ((cod f),a) proof percases ( Hom ((cod f),a) = {} or Hom ((cod f),a) <> {} ) ; suppose Hom ((cod f),a) = {} ; ::_thesis: dom (hom (f,a)) = Hom ((cod f),a) hence dom (hom (f,a)) = Hom ((cod f),a) ; ::_thesis: verum end; suppose Hom ((cod f),a) <> {} ; ::_thesis: dom (hom (f,a)) = Hom ((cod f),a) then Hom (c,a) <> {} by A35, ENS_1:42; hence dom (hom (f,a)) = Hom ((cod f),a) by A35, FUNCT_2:def_1; ::_thesis: verum end; end; end; then dom (ta1 `2) = dom (hom (f,(id a))) by A36, A50, ENS_1:53; then hom (f,(id a)) = ta1 `2 by A51, FUNCT_1:2; hence <|f,?> . a = t . a by A35, A36, A40, A39, A48, Def3; ::_thesis: verum end; then <|f,?> = t by A4, A37, A19, A17, A11, A35, A36, ISOCAT_1:26; hence g = (Yoneda A) . f by A3, A5, A18, A22, A17, A11, A35, A36, Def4; ::_thesis: verum end; hence Yoneda A is full by Def7; ::_thesis: verum end; end;