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

[Peter Hancock]

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

My supervisor, Robin Gandy, an old-school logician, once said to me
(approximately...): "I've stared at it several times.  Sometimes I feel it is
completely trivial; and at other times I feel it is totally mysterious."

I have to admit I often feel the same about things in category theory.

By the way, for the record, the Yoneda lemma says that the natural transformations
from the functor Hom[A,_] for A : C to some random functor F : C -> Set have
the same cardinal as F(A).  Maybe Andreas can translate that into a type signature?

Hank