1 (*******************************************************************************)
2 (* Chapter 8: Yoneda *)
3 (*******************************************************************************)
6 Lemma YonedaLemma : forall (A B:ec), (CategoryOfNaturalTransformations (RepresentableFunctor A) (RepresentableFunctor B)) ≅ (B~~>A)