:: deftheorem Def4 defines Yoneda YONEDA_1:def 4 :
for A being Category
for b₂ being Contravariant_Functor of A, Functors (A,(EnsHom A)) holds
( b₂ = Yoneda A iff for f being Morphism of A holds b₂ . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] );