The abstract of the Mizar article:

Yoneda Embedding

by

Miroslaw Wojciechowski

Received June 12, 1997

MML identifier: YONEDA_1

[ Mizar article, MML identifier index ]

environ

 vocabulary CAT_1, ENS_1, FUNCT_1, RELAT_1, MCART_1, NATTRA_1, BOOLE, OPPCAT_1,
      CAT_2, FUNCT_2, YONEDA_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2,
      CAT_1, CAT_2, OPPCAT_1, ENS_1, NATTRA_1;
 constructors DOMAIN_1, ENS_1, NATTRA_1, PARTFUN1;
 clusters FUNCT_1, RELSET_1, ENS_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

reserve y for set;
reserve A for Category, a,o for Object of A;
reserve f for Morphism of A;

definition let A;
 func EnsHom(A) -> Category equals
:: YONEDA_1:def 1
  Ens(Hom(A));
end;

theorem :: YONEDA_1:1
 for f,g being Function, 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;

theorem :: YONEDA_1:2
hom?-(a) is Functor of A,EnsHom(A);

definition let A,a;
  func <|a,?> -> Functor of A,EnsHom(A) equals
:: YONEDA_1:def 2
             hom?-(a);
end;

theorem :: YONEDA_1:3
for f being Morphism of A holds
 <|cod f,?> is_naturally_transformable_to <|dom f,?>;

definition let A,f;
func <|f,?> -> natural_transformation of <|cod f,?>, <|dom f,?> means
:: YONEDA_1:def 3
  for o be Object of A holds
       it.o = [[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)];
end;

theorem :: YONEDA_1:4
for f being Element of the Morphisms of A holds
  [[<|cod f,?>,<|dom f,?>],<|f,?>] is Element of the Morphisms of
                                                        Functors(A,EnsHom(A));

definition let A;
func Yoneda(A) -> Contravariant_Functor of A,Functors(A,EnsHom(A)) means
:: YONEDA_1:def 4
      for f being Morphism of A holds
              it.f = [[<|cod f,?>,<|dom f,?>],<|f,?>];
end;

definition let A,B be Category;
 let F be Contravariant_Functor of A,B;
 let c be Object of A;
func F.c -> Object of B equals
:: YONEDA_1:def 5
   (Obj F).c;
end;


theorem :: YONEDA_1:5
   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;


definition let C,D be Category;
           let T be Contravariant_Functor of C,D;
  attr T is faithful means
:: YONEDA_1:def 6
  for c,c' being Object of C st Hom(c,c') <> {}
   for f1,f2 being Morphism of c,c' holds T.f1 = T.f2 implies f1 = f2;
end;

theorem :: YONEDA_1:6
 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;

theorem :: YONEDA_1:7
  Yoneda A is faithful;

theorem :: YONEDA_1:8
  Yoneda A is one-to-one;

definition let C,D be Category;
           let T be Contravariant_Functor of C,D;
attr T is full means
:: YONEDA_1:def 7
 for c,c' being Object of C st Hom(T.c',T.c) <> {}
    for g being Morphism of T.c',T.c holds
    Hom(c,c') <> {} & ex f being Morphism of c,c' st g = T.f;
end;

theorem :: YONEDA_1:9
  Yoneda A is full;