[Agda] Associativity for free!

[Andreas Abel]

On 10/27/11 3:47 PM, James Chapman wrote:
> Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
>
> Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
> Y {C} f = λ Z g → comp C g f
>
> and we can convert back again:
>
> Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
> Y-1 {C}{A}{B} α = α B (iden C)

Is that the glorious Yoneda lemma?  Trivial in the language of types. 
Just subtract the categorical waffle and every programmer understands it...

Cheers,
Andreas

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