[Agda] algebra hierarchy in library

[Sergei Meshveliani]

Dear standard library developers and supporters,

can you please answer in (simple words) several questions about the
representation of the algebraic hierarchy in standard library?


1. Why `Raw' structures?

There are classical generic algebraic structures (call them GAS):
Magma, Semigroup, Monoid, and so on.

Those of them having some new field respectively to previous structures
are accompanied with the corresponding `Raw' record. For example, Magma
is preceded with RawMagma, Monoid with RawMonoid. Each `Raw' structure
expresses only the signature of the corresponding GAS.

What the `Raw' structures serve for?


2. Why putting `Is' structures into a different file?

For example, the reader looks into Algebra.agda to find what is
Semigroup:

-------------------------------------------------------
  record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
    ...
    field Carrier     : Set c
          _≈_         : Rel Carrier ℓ
          _∙_         : Op₂ Carrier
          isSemigroup : IsSemigroup _≈_ _∙_

    open IsSemigroup isSemigroup public
    ...
    magma = record { isMagma = isMagma }
    ...

Now, one needs to find a declaration for IsSemigroup.
And it resides in a different file of
                                   Algebra/Structures.agda :

  record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
    field
      isMagma : IsMagma ∙
      assoc   : Associative ∙

    open IsMagma isMagma public
---------------------------------------------------------

And all this implements the meaning of a small sentence:
``Semigroup is Magma in which multiplication _∙_ is associative''.

Why not put ``record IsSemigroup'' before ``record Semigroup'' in the
same file  Algebra.agda ?

Similarly other `Is' GAS decls can join. So that Algebra.agda and
Algebra/Structures.agda will merge into  Algebra.agda   in which each
GAS will be defined in one place.
For example, to see what is a group will need to look into one file, not
in two files.
?


3. Why Magma declares the fields  Carrier and _≈_  by new?

Similarly, why other GAS re-declare many fields?

In theory, we have
``Magma is a setoid with an operation _∙_ congruent with respect to the
equality _≈_''.

So, Magma inherits Setoid. And it is natural for its representation in
Agda to have  setoid  somewhere inside it. So, it opens this setoid and
uses its fields in further definitions. For example, like this:

-- Version II ---------------------------------------------------------

record IsMagma {α α=} (S : Setoid α α=) (_∙_ : Op₂ (Setoid.Carrier S)) :
                                                           Set (α ⊔ α=)
  where
  open Setoid S using (_≈_; Carrier)
  field
    ∙cong : _∙_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_

record Magma α α= :  Set (suc (α ⊔ α=))
  where
  field  setoid : Setoid α α=

  open Setoid setoid public
  infixl 7 _∙_

  field  _∙_     : Op₂ Carrier
         isMagma : IsMagma setoid _∙_
------------------------------------------------------------------------

And let us call  Version I  the approach of Standard library lib-0.17.

Both versions use an `Is' structure, but II does not re-declare fields.
Is not II more natural?


Another question may be:
``why splitting each GAS into proper structure and `Is' structure?''.

My guess is that this approach allows us to express two GAS-s that are
over the same inherited GAS. For example, a programmer can express a
product of two Magmae over the same Setoid:
------------------------------------------------------------
module _ {α α=} (S : Setoid α α=)
  where
  open Setoid S using (Carrier; _≈_)
  SS = ×-setoid S S
  open Setoid SS using () renaming (Carrier to CC; _≈_ to _=p_)

  magmaProduct' :
    (_*₁_ _*₂_ : Op₂ Carrier) → IsMagma _≈_ _*₁_ →
                                IsMagma _≈_ _*₂_ → Magma α α=
  magmaProduct' _*₁_ _*₂_ insM₁ isM₂ =
                       <define coordinate-wise multiplcation on CC;
                        prove ...;  return the Magma record
                       >
------------------------------------------------------------

(is there any other purpose to introduce `Is' -structures?).

This is equally easy to set both in Version I and Version II.

But note that both approaches still deviate, a bit, from the theory.
Because in theory, it is 
\ (mg1 : Magma_ _) (mg2 : Magma _ _) (HaveCommonSetoid mg1 mg2) →
product-magma,
while magmaProduct' takes certain parts of the two magmae.

So, there remain somewhat three and a half questions.

Thank you in advance for your possible explanation.

------
Sergei