(*******************************************************************************) (* Chapter 8: Yoneda *) (*******************************************************************************) (* Lemma YonedaLemma : forall (A B:ec), (CategoryOfNaturalTransformations (HomFunctor A) (HomFunctor B)) ≅ (B~~>A) *)