[Agda] problem with algebraic hierarchy

[mechvel at scico.botik.ru]

We wrote the following to GitHub for the library:

mechvel
-------
I wonder: how to express in Agda-2.6.1 + lib-1.3 the following 
discourse?
Let R and U be semirings having the same additive monoid 
(+-commutativeMonoid).
Denote * and *' the multiplication operators in R and U respectively,
1# and e the unities in R and U respectively. Prove in Agda that

for all x in R  it holds  (1# + 1#) * x ≈ (e + e) *' x     -- (I)

And let us assume that the lemma 2*as+ : ∀ x → (1# + 1#) * x ≈ x + x
is proved in the module OfSemiring parameterized by Semiring
(it is proved simply in 2-4 steps).
Mathematically, the statement (I) has sense.
And its proof is simple: the left hand side equals x + x by the laws of 
R;
the right hand side equals x + x by the laws of U, and this is the same
element of their common Carrier.
The matter is not in the proof itself, it is in finding a valid 
formulation
of the theorem (I) in Agda.
Can anybody, please, demonstrate?


Matthew Daggitt
---------------
> This is not a question for the standard library.
> Best to ask this on the mailing list.


No, it is for the standard library.
But let it be, I write to the Agda list.

For example, if the library was organized in a different way, the 
following code would work:

-----------------------------------------
theorem : ∀ {α α≈} (S : Setoid α α≈) (+cMon : CommutativeMonoid S)
                                      (*Mon  : Monoid S)
                                      (*'Mon : Monoid S)
                    (R : Semiring S +cMon *Mon) (U : Semiring S +cMon 
*Mon) →
                    let open Semiring R
                        open Semiring U using ()
                                        renaming (_*_ to _*'_; 1# to e)
                    in
                    (x : Carrier) → (1# + 1#) * x ≈ (e + e) *' x

theorem S R +cMon *Mon *'Mon R U x =
     begin
       (1# + 1#) * x  ≈⟨ OfSemiring.2*as+ R x ⟩
       x + x          ≈⟨ sym (OfSemiring.2*as+ U x) ⟩
       (e + e) *' x
     ∎
------------------------------------------

Here Magma, Semigroup, Monoid, CommutativeMonoid  have an argument of 
the Setoid type.
Semiring has arguments (S : Setoid _ _), (+M : CommutativeMonoid S),
(*M : Monoid S).

Also this solves the problem of a common setoid for +-magma and *-magma 
in a semiring
(of what we wrote earlier).

I do not say that everything is all right there.
But generally, it has sense to think of experimental libraries that 
reorganize the
algebraic part, of different ways to transfer the domain parameters.

The first step may be setting (S : Setoid) as an argument as above.
This will improve much, without spoiling anything.
But I am not sure that this will be sufficient.

Regards,

------
Sergei