[Agda] common super-structure

[Sergei Meshveliani]

People,

I have a question on the algebraic hierarchy architecture in Standard
library.
This concerns the problem of a common super-structure (super-class).

Consider the example:

 having  f : ∀ {c l} → Semigroup c l → Semigroup c l → Semigroup c l,
 implement 
  g : (H H' : Semigroup) → H and H' are on the same setoid → Semigroup
  g H H' =  f H H'

Consider the program

----------------------------------------------------------------------
postulate  f : ∀ {c l} → Semigroup c l → Semigroup c l → Semigroup c l

g :  ∀ {c l} → Semigroup c l → Semigroup c l → Semigroup c l  -- wrong
g H H' =  f H H'
----------------------------------------------------------------------

This will not do, because the domain of  g  is not as required.

Below  g'  pretends to implement the goal:

-------------------------------------------------------------
module CommonSuper where
open import Relation.Binary            using (Setoid)
open import Algebra                    using (Semigroup)
open import Algebra.Structures         using (IsSemigroup)
open import Algebra.FunctionProperties using (Op₂)

postulate f : ∀ {c l} → Semigroup c l → Semigroup c l → Semigroup c l

g' :  ∀ {c l} → (S : Setoid c l) → 
        let open Setoid S using (_≈_; Carrier) 
        in
        (_∙_ _∙'_ : Op₂ Carrier) → 
        IsSemigroup _≈_ _∙_ → IsSemigroup _≈_ _∙'_ → Semigroup c l   

g' S _∙_ _∙'_ isSemig isSemig' =  f H H'
                        where
                        open Setoid S using (_≈_; Carrier) 

                        H  = record{ Carrier     = Carrier
                                   ; _≈_         = _≈_ 
                                   ; _∙_         = _∙_ 
                                   ; isSemigroup = isSemig
                                   }
                        H' = record{ Carrier     = Carrier
                                   ; _≈_         = _≈_ 
                                   ; _∙_         = _∙'_ 
                                   ; isSemigroup = isSemig'
                                   }
--------------------------------------------------------------

But here  g'  is applied not to a pair of semigroups but to their rather
decomposed forms.

Further,  g''  looks as something more close to the goal: 


  g'' :  ∀ {c l} → (H H' : Semigroup c l) → 
                   let S  = Semigroup.setoid H 
                       S' = Semigroup.setoid H' 
                   in
                   (CoinverseSetoidIso S S') → Semigroup c l   

  g'' H H' _ =  f H H'


Here  isoPair : CoinverseSetoidIso S S'

is a pair of mutually inverse setoid isomorphisms between S and S'.
For the condition of "over the same setoid" it suggests to include a 
setoid isomorphism into the signature.
Still a complication. We have two different types for setoid instead of
one.

The release 0.04.1 of the DoCon-A library applies the approach in which
the Semigroup record will have (S : Setoid) as an _argument_.
And a similar construct with super-structures as arguments is repeated
for Group, Ring, and so on.
With this approach, the examples like the above  g  are programmed
easier.

But this still leads to a certain complication. Because this forces 
introduction of certain up-structures: Semigroup - UpSemigroup, 
Group - UpGroup, and so on (see Manual on DoCon-A-0.04.1).

In  DoCon-A-2.00,  I return to the approach similar to Standard library,
with adding the Is-structures (IsSemigroup, IsGroup, and such).

Anyway, a spot of inadequacy is visible.

Can anybody comment on this philosophy?

Regards,

------
Sergei