[throwaway000002]

> I think it's clearer if you don't bring in the lemma.

Well of course it's clearer, it's because you're working with specific example, whereas Yoneda applies in a very general setting, you just have to see how you can "squint" and see the general setup in the specific case.

People always talk about a category Hask, but you can easily imagine a category "C" in an analogous way. You can also imagine an "SSA" category of a static single-assignment intermediate language of a compiler. Compilation would be a functor from C to SSA. Likewise you can consider an (endo)functor from C to C which turns a function from direct style to CPS, and then run the compiler to get SSA. You can then ask is the SSA generated in both steps the same "semantically". Actually proving that in all its gory detail is simplified by making the right setup as explicated by user tel and then applying the Yoneda lemma at the right moment to conclude the proof.

More interestingly you can ask questions like does an SSA optimisation, an (endo)functor on SSA correspond to some optimisation in C that could be a source-to-source transform.

Etc, etc.

The purpose of mathematical abstraction is simplification, even though it may transmogrify the concrete into a seemingly unpalatable form.