Making sense of Yoneda

Further to the earlier conversation about (x→p)→q as a monad.

Let's make sense of the application of Yoneda lemma here:

https://chaource.dreamwidth.org/235262.html?thread=1023998#cmt1023998

( This part of the original proof... )

Hmmm... I was hoping to get rid of these loose ends in one go, but maybe later.