[Agda] Raw algebraic structures in the standard library

[mechvel at scico.botik.ru]

On 2019-08-04 11:08, Matthew Daggitt wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


If you require the axioms of equivalence or/and congruence for _≈_ and 
_∙_ for RawMagma,
then it will turn out that RawMagma is same as Magma. And further, this 
approach leads to eliminating the Raw structures
-- ?

I thought that the Raw records are introduced to represent and consider 
the signatures as not provided with any properties besides those induced 
automatically by a non-dependent type signature
(I never thought of this, is it true that they deal with non-dependent 
types?).
For example,  foo : Carrier -> Nat  automatically postulates that foo 
returns a member of Nat and not of Bool, and the type checker checks 
this property, and dependent types are not needed for this.

--
SM