The existing Yoneda_Embedding theorem in Functor/Hom/Yoneda.v asserts that there exists an isomorphism Hom(c,d) \cong Nat(Hom(-,c), Hom(-,d)). However if one already is working with the Curried_Hom functor, it is not clear how to use this theorem to prove that the fmap[Curried_Hom] functor is a bijection. There is a need for some theorem which explicitly mentions the functor Curried_Hom in the statement so that one can use the Yoneda embedding bijection together with the functoriality properties of Curried_Hom.
jwiegley
commented
1 year ago
The existing Yoneda_Embedding theorem in Functor/Hom/Yoneda.v asserts that there exists an isomorphism Hom(c,d) \cong Nat(Hom(-,c), Hom(-,d)). However if one already is working with the Curried_Hom functor, it is not clear how to use this theorem to prove that the fmap[Curried_Hom] functor is a bijection. There is a need for some theorem which explicitly mentions the functor Curried_Hom in the statement so that one can use the Yoneda embedding bijection together with the functoriality properties of Curried_Hom.