# [Agda] common argument structure

Sergei Meshveliani mechvel at botik.ru
Wed Dec 4 15:42:04 CET 2013

```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)

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

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
* and such.

Regards,

------
Sergei

```