[yoshiki] Re: [Agda] Associativity for free!

[KINOSHITA Yoshiki]

Dear Anderas,

andreas.abel> my colleague Ulrich Schoepp always told me the Yoneda
andreas.abel> lemma was "trivial", meaning "easy", but me being not so
andreas.abel> fluent in category theory usually got lost trying to
andreas.abel> understand the statement.  However, I can read type
andreas.abel> signatures...

You might be interested in looking at the Agda code for the proof of
Yoneda lemma which I posted after the last AIM.  It is in "Libraries
and other developments" page of Agda wiki.  I have already started to
forget what are in it, but I just checked not only the proposition
attributed to Yoneda in MacLane's book but also the definition of
Yoneda embedding is there.

Yoshiki.