[Agda] Associativity for free!

[Alan Jeffrey]

Hmm, thinking of which, this means that adding:

   ≡-relevant : ∀ {A} {a b : A} → .(a ≡ b) → (a ≡ b)

means that given f : A → B, we can define a subset of B isomorphic to 
the image of f as:

   record Image {A B : Set} (f : A → B) : Set where
     b : B
     .b✓ : ∃ (λ a → f a ≡ b)

The "assoiativity for free" construction for a monoid (_+_ : A → A → A) 
is just (Image _+_).

A.

On 10/28/2011 01:49 PM, Jeffrey, Alan S A (Alan) wrote:
> 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