[Agda] Associativity for free!

[Daniel Peebles]

That link looks broken, but
http://www.cse.chalmers.se/~peterd/papers/Coherence_Monoidal.pdf seemed to
work :)

2011/10/28 Peter Dybjer <peterd at chalmers.se>

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111028/f0d90991/attachment.html