That link looks broken, but <a href="http://www.cse.chalmers.se/~peterd/papers/Coherence_Monoidal.pdf">http://www.cse.chalmers.se/~peterd/papers/Coherence_Monoidal.pdf</a> seemed to work :)<div><br><div class="gmail_quote">
2011/10/28 Peter Dybjer <span dir="ltr"><<a href="mailto:peterd@chalmers.se">peterd@chalmers.se</a>></span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">Have a look at<br>
<br>
<a href="http://www.cse.chalmers.se/~peterd/papers/nbe.html/Coherence_Monoidal.pdf" target="_blank">http://www.cse.chalmers.se/~peterd/papers/nbe.html/Coherence_Monoidal.pdf</a><br>
<br>
I think it is related.<br>
Peter<br>
<br>
________________________________________<br>
From: <a href="mailto:agda-bounces@lists.chalmers.se">agda-bounces@lists.chalmers.se</a> [<a href="mailto:agda-bounces@lists.chalmers.se">agda-bounces@lists.chalmers.se</a>] On Behalf Of Alan Jeffrey [<a href="mailto:ajeffrey@bell-labs.com">ajeffrey@bell-labs.com</a>]<br>
Sent: Friday, October 28, 2011 7:55 PM<br>
To: Andreas Abel<br>
Cc: Agda mailing list<br>
Subject: Re: [Agda] Associativity for free!<br>
<div><div></div><div class="h5"><br>
That's the Glorious Yoneda Lemma's action on homs, you are also expected<br>
to prove a bunch of coherence properties. I suspect that if we assumed<br>
parametricity of Agda, then many of the coherence properties would come<br>
out in the wash.<br>
<br>
I prefer categorical waffles to burned toast, which is often the<br>
alternative.<br>
<br>
A.<br>
<br>
On 10/28/2011 10:26 AM, Andreas Abel wrote:<br>
> On 10/27/11 3:47 PM, James Chapman wrote:<br>
>> Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:<br>
>><br>
>> Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)<br>
>> Y {C} f = λ Z g → comp C g f<br>
>><br>
>> and we can convert back again:<br>
>><br>
>> Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B<br>
>> Y-1 {C}{A}{B} α = α B (iden C)<br>
><br>
> Is that the glorious Yoneda lemma? Trivial in the language of types.<br>
> Just subtract the categorical waffle and every programmer understands it...<br>
><br>
> Cheers,<br>
> Andreas<br>
><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>