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

[KINOSHITA Yoshiki]

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>