The Yoneda lemma deals with functors to the category of functions.
The Yoneda functor, say Y, for an object, say Z, is a specific example of such a functor.
The lemma establishes a one-to-one correspondence between natural transformations from the Yoneda functor Y, for an object Z, to functors, F, to the category of functions, and elements of F(Z).
Clearly the Yoneda lemma is pointful (it involves elements of sets).
Now assume that there exists a functor from the category of functions to the category. This functor can be composed with Yoneda functors to obtain endofunctors. Functional programming is a typical area where this is the case.
My questions are:
- Does there exist a pointfree alternative of the Yoneda lemma for endofunctors?
- What are the minimal extra requirements on the category that are needed to prove it?
Thanks, Luc