[Agda] Associativity for free!

[Peter Dybjer]

Have a look at

http://www.cse.chalmers.se/~peterd/papers/nbe.html/Coherence_Monoidal.pdf

I think it is related.
Peter

________________________________________
From: agda-bounces at lists.chalmers.se [agda-bounces at lists.chalmers.se] On Behalf Of Alan Jeffrey [ajeffrey at bell-labs.com]
Sent: Friday, October 28, 2011 7:55 PM
To: Andreas Abel
Cc: Agda mailing list
Subject: Re: [Agda] Associativity for free!

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
>
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda