[Agda] common argument structure

[Sergei Meshveliani]

People,
I have the following question on the algebra classes in Standard library
(up to lib-0.7).

What is the simplest expression for the generic signature for two
semigroups over the same setoid?

I find that this is type-checked
(in development Agda of November 2013):

-------------------------------------------------------------------
f : ∀ {α α=} → (S : Setoid α α=) →
    let
       open Setoid S using (Carrier; _≈_)
    in
    (_∙_ _∙'_ : Op₂ Carrier) → (isSemig  : IsSemigroup _≈_ _∙_)  →
                               (isSemig' : IsSemigroup _≈_ _∙'_) → Set

f {α} {α=} S _∙_ _∙'_ isSemig isSemig' =  foo H H'
  where
  C = Setoid.Carrier S

  H : Semigroup α α=
  H = record{ Carrier = C; _∙_ = _∙_; isSemigroup = isSemig }

  H' : Semigroup α α=
  H' = record{ Carrier = C; _∙_ = _∙'_; isSemigroup = isSemig' }

  foo : Semigroup α α= → Semigroup α α= → Set     -- contrived    
  foo _ _ = ⊤
-------------------------------

Is there a simpler approach?
How complex will this turn, for example, for two Ring-s (Semiring-s)
over the same additive group?

I understand the approach of lib-0.7 like this:
to define a class Foo2 over the `argument' class Foo1 
one needs to use the library structure of kind  Is<Foo1>   and the
appropriate additional argument parameters.

In my library (not for standard), I use (so far) a different approach.
And then, need to define maps  my-class -> standard-class  for several
standard algebra classes (because it is still desirable to provide a
certain connection).

But in any case, I need to understand this architectural question about
Standard, somehow to estimate to what pool I am diving in.

The continuation of the line need to deal with 
* two Ring-s (Semiring-s) over the same additive group,
* modules (LeftModule) (of vectors) over the same Ring but of different
additive groups of vectors,
* and such.

Regards,

------
Sergei