src/Yoneda_ch8.v

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