X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FYoneda_ch8.v;h=d7652da44026fc5fd8188bdaebfa0d2654652702;hp=045c427710206c6a94a6d5c80d832eaa0f4a6ad1;hb=00b060e4854e5a1ba01746be44ac9deb49d7fbf5;hpb=18d94149267db9cf2e8e93977c5506278309173d

diff --git a/src/Yoneda_ch8.v b/src/Yoneda_ch8.v
index 045c427..d7652da 100644
--- a/src/Yoneda_ch8.v
+++ b/src/Yoneda_ch8.v
@@ -3,5 +3,5 @@
 (*******************************************************************************)
 
   (*
-  Lemma YonedaLemma : forall (A B:ec), (CategoryOfNaturalTransformations (RepresentableFunctor A) (RepresentableFunctor B)) ≅ (B~~>A)
+  Lemma YonedaLemma : forall (A B:ec), (CategoryOfNaturalTransformations (HomFunctor A) (HomFunctor B)) ≅ (B~~>A)
   *)