[Agda] Raw algebraic structures in the standard library

[mechvel at scico.botik.ru]

On 2019-08-08 13:55, Matthew Daggitt wrote:
> [..]


> 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.

I presumed that as you consider moving the _≈_ laws and the congruence 
law for _∙_ to RawMagma,
then you are probably going to bring the laws for _∙_ to RawSemigroup 
(associativity), and so on.
If not, then do you consider moving other congruence laws to the Raw 
structures?
So far, I see only ∙-cong, but there may appear others. Also what about 
the "resp" laws?
They are somewhat similar (<-resp-≈ ...).

--
SM


> On Tue, Aug 6, 2019 at 12:58 AM <mechvel at scico.botik.ru> wrote:
> 
>> 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