[Agda] (Semi)RingWithOne

[Sergei Meshveliani]

Dear all,

This is a certain minor point about algebra in Standard library.
I am writing a certain application that relies on  Standard library
algebra, from Semigroup up to CommutativeRing.
And I observe the following.

(I) A classical book by Lang (1968) defines that a Ring has an unity 
    element by multiplication.

(II) A classical book by Van Der Waerden (1971) defines that a Ring does
not necessary has unity. If it has, people call it "Ring with unity". 
I expected that in Standard library it would be called  RinWithOne.
But I do not find such there.

(III) Standard library defines that Semiring has unity (1#),
  and Ring inherits Semiring, so that Ring always has an unity element
  by multiplication. And this agrees with (I).
  (and naturally, the name RingWithOne is skipped).

(IV) But Standard library also introduces SemiringWithoutOne.
                                                  -------

(V) Even integer numbers occur a Ring according to (II), 
    but not according to (I).


Summing all this, I think that this will be more natural for Standard
library 
* to define Ring as in (II),
* to define Semiring with skipping 1#  (instead of SemiringWihoutOne),
* to define SemiringWithOne as including 1#,
* to define RingWithOne as inheriting SemiringWithOne.

-- ?

Regards,

------
Sergei