[Agda] Right Distributivity

[Nils Anders Danielsson]

On 2018-03-22 21:55, Philip Wadler wrote:
> In Algebra.FunctionProperties one finds the definitions:
> 
>     _DistributesOverˡ_ : Op₂ A → Op₂ A → Set _
>     _*_ DistributesOverˡ _+_ =
>        ∀ x y z → (x * (y + z)) ≈ ((x * y) + (x * z))
> 
>     _DistributesOverʳ_ : Op₂ A → Op₂ A → Set _
>     _*_ DistributesOverʳ _+_ =
>        ∀ x y z → ((y + z) * x) ≈ ((y * x) + (z * x))
> 
> To me, the  second of these appears ass-backwards. I would expect
> 
>     _DistributesOverʳ_ : Op₂ A → Op₂ A → Set _
>     _*_ DistributesOverʳ _+_ =
>        ∀ x y z → ((x + y) * z) ≈ ((x * z) + (y * z))
> 
> 
> What is the rationale for the current definition?

I wrote that code more than ten years ago. My guess would be that I
copied the first definition,

   (x * (y + z)) ≈ ((x * y) + (x * z)),

and then simply swapped the arguments of every instance of _*_:

   ((y + z) * x) ≈ ((y * x) + (z * x)).

-- 
/NAD