<div dir="ltr"><div>In Algebra.FunctionProperties one finds the definitions:</div><div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><font face="monospace, monospace">_DistributesOverˡ_ : Op₂ A → Op₂ A → Set _<br>_*_ DistributesOverˡ _+_ =<br>  ∀ x y z → (x * (y + z)) ≈ ((x * y) + (x * z))<br></font></blockquote><div><font face="monospace, monospace"> </font></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><font face="monospace, monospace">_DistributesOverʳ_ : Op₂ A → Op₂ A → Set _<br>_*_ DistributesOverʳ _+_ =<br>  ∀ x y z → ((y + z) * x) ≈ ((y * x) + (z * x))<br></font></blockquote><div><br></div><div>To me, the  second of these appears ass-backwards. I would expect</div></div><div><br></div><div><blockquote class="gmail_quote" style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><font face="monospace, monospace">_DistributesOverʳ_ : Op₂ A → Op₂ A → Set _<br>_*_ DistributesOverʳ _+_ =<br>  ∀ x y z → ((x + y) * z) ≈ ((x * z) + (y * z))<br></font></blockquote><div><br></div><div>What is the rationale for the current definition? Cheers, -- P</div></div><div><br></div><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
</div>