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

[Andreas Abel]

Dear Yoshiki,

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...

Cheers,
Andreas

On 11/1/11 1:57 PM, KINOSHITA Yoshiki wrote:
> Dear Andreas,
>
> surely, what James described is a part of (gateway to?) Yoneda lemma.
>
> I think you are right in saying that it is trivial.  The whole body of
> Yoneda lemma is trivial.  I recall Peter Freyd wrote something which
> means that many theorems in category theory are trivial, but it is not
> trivial to find a setting which makes those things trivial.  I am sure
> Freyd's original wording was much better.  I once read it in some
> mailing list, was impressed by it, talked about it with several
> people, lost the article and have never found it again.  I miss it...
>
> Yoshiki.
> --
> Yoshiki Kinoshita, D.Sc.
> Principal Research Scientist
> Information Technology Research Insititute
> National Institute of Advanced Industrial Science and Technology (AIST)
> 3-11-46 Nakoji, Amagasaki-shi
> Hyogo, 661-0974, Japan
> Phone: 06-6494-8017  Fax:
> E-mail: yoshiki at m.aist.go.jp
> home page: http://staff.aist.go.jp/kinoshita.yoshiki/
>
>
> From: Andreas Abel<andreas.abel at ifi.lmu.de>
> Subject: [yoshiki] Re: [Agda] Associativity for free!
> Date: Fri, 28 Oct 2011 17:26:54 +0200
> Message-ID:<4EAAC9BE.9010208 at ifi.lmu.de>
>
> andreas.abel>  On 10/27/11 3:47 PM, James Chapman wrote:
> andreas.abel>  >  Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
> andreas.abel>  >
> andreas.abel>  >  Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
> andreas.abel>  >  Y {C} f = λ Z g → comp C g f
> andreas.abel>  >
> andreas.abel>  >  and we can convert back again:
> andreas.abel>  >
> andreas.abel>  >  Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
> andreas.abel>  >  Y-1 {C}{A}{B} α = α B (iden C)
> andreas.abel>
> andreas.abel>  Is that the glorious Yoneda lemma?  Trivial in the language of types.
> andreas.abel>  Just subtract the categorical waffle and every programmer understands it...
> andreas.abel>
> andreas.abel>  Cheers,
> andreas.abel>  Andreas
> andreas.abel>
> andreas.abel>  --
> andreas.abel>  Andreas Abel<><       Du bist der geliebte Mensch.
> andreas.abel>
> andreas.abel>  Theoretical Computer Science, University of Munich
> andreas.abel>  Oettingenstr. 67, D-80538 Munich, GERMANY
> andreas.abel>
> andreas.abel>  andreas.abel at ifi.lmu.de
> andreas.abel>  http://www2.tcs.ifi.lmu.de/~abel/
> andreas.abel>  _______________________________________________
> andreas.abel>  Agda mailing list
> andreas.abel>  Agda at lists.chalmers.se
> andreas.abel>  https://lists.chalmers.se/mailman/listinfo/agda
> andreas.abel>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/