<div dir="ltr">Dear all,<br><div> This is a question for anyone who uses the raw algebraic structures from the standard library. Currently `RawMagma`, `RawMonoid`, `RawRing` etc. contain no axioms whatsoever. We're not entirely convinced this is the right approach as without proofs that <span style="color:rgb(36,41,46);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,monospace;font-size:12px;white-space:pre">_≈_ </span>is an equivalence, and that <span style="color:rgb(36,41,46);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,monospace;font-size:12px;white-space:pre">_∙_</span> is congruent with respect to it then it is impossible to do any reasoning at all about them. In order to make them more useful we're considering changing their definitions so that they include the equality axioms above. </div><div><br></div><div>Basically the question is does anyone have a use case for the raw structures in which the equality axioms would be problematic to provide?</div><div>Best,</div><div>Matthew</div></div>