[Agda] Right Distributivity

[Philip Wadler]

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? Cheers, -- P


.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180322/058ea61d/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180322/058ea61d/attachment.ksh>