[Agda] Associativity for free!

[Alan Jeffrey]

Oops, URL typo...

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

I had a quick read through, and it is indeed related, but (I believe) 
is, given any monoid (resp. monoidal category) M, building a strict 
monoid (resp. strict monoidal category) N and a morphism (resp. monoidal 
functor) J : M -> N such that (a ~ b in M) iff (J a = J b).

This is indeed related. The thing I think might be new is using 
irrelevance as a way to build the subset of N such that J forms an 
isomorphism.

A.

On 10/28/2011 01:23 PM, Peter Dybjer wrote:
> 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