<div dir="ltr">Thanks Jacques, that's a great explanation of their function and explains a lot. I have to confess I haven't seen any programs that do such "raw" computation, but I can see why they would be useful. Hmm maybe the algebraic structures with just equality axioms need to be added as another level of between the two existing levels. Maybe "raw", "medium" and "well-done" is the way to go :)<div><br></div><div>Sergei, yes if we made the previously proposed change then RawMagma would be equivalent to Magma but the rest of the hierarchy would diverge. RawMagma would not be equivalent to Semigroup as it would lack associativity, likewise RawMonoid would not be equivalent to Monoid. I'm afraid I don't understand your second question.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Aug 6, 2019 at 12:58 AM <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 2019-08-04 11:08, Matthew Daggitt wrote:<br>
> Dear all,<br>
>  This is a question for anyone who uses the raw algebraic structures<br>
> from the standard library. Currently `RawMagma`, `RawMonoid`,<br>
> `RawRing` etc. contain no axioms whatsoever. We're not entirely<br>
> convinced this is the right approach as without proofs that _≈_ is<br>
> an equivalence, and that _∙_ is congruent with respect to it then it<br>
> is impossible to do any reasoning at all about them. In order to make<br>
> them more useful we're considering changing their definitions so that<br>
> they include the equality axioms above.<br>
> <br>
> Basically the question is does anyone have a use case for the raw<br>
> structures in which the equality axioms would be problematic to<br>
> provide?<br>
> Best,<br>
> Matthew<br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
If you require the axioms of equivalence or/and congruence for _≈_ and <br>
_∙_ for RawMagma,<br>
then it will turn out that RawMagma is same as Magma. And further, this <br>
approach leads to eliminating the Raw structures<br>
-- ?<br>
<br>
I thought that the Raw records are introduced to represent and consider <br>
the signatures as not provided with any properties besides those induced <br>
automatically by a non-dependent type signature<br>
(I never thought of this, is it true that they deal with non-dependent <br>
types?).<br>
For example,  foo : Carrier -> Nat  automatically postulates that foo <br>
returns a member of Nat and not of Bool, and the type checker checks <br>
this property, and dependent types are not needed for this.<br>
<br>
--<br>
SM<br>
</blockquote></div>