[Agda] Associativity for free!

[Alan Jeffrey]

That's the Glorious Yoneda Lemma's action on homs, you are also expected 
to prove a bunch of coherence properties. I suspect that if we assumed 
parametricity of Agda, then many of the coherence properties would come 
out in the wash.

I prefer categorical waffles to burned toast, which is often the 
alternative.

A.

On 10/28/2011 10:26 AM, Andreas Abel wrote:
> 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
>