[Agda] Raw algebraic structures in the standard library

[Matthew Daggitt]

Dear all,
 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 _≈_ is an equivalence, and that _∙_ 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.

Basically the question is does anyone have a use case for the raw
structures in which the equality axioms would be problematic to provide?
Best,
Matthew
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190804/54dff0a5/attachment.html>