[Agda] algebra hierarchy in library

[Sergei Meshveliani]

On Sat, 2019-03-16 at 18:16 +0800, Matthew Daggitt wrote:
>[..]

>         If this is the only reason, then it occurs that `Is' structure
>         is needed only in few cases.
> 
> 
> I think your examples miss the point. For example take any binary
> operator. That binary operator may form many different
> Semigroups/Monoids/Groups etc. depending on what the underlying
> equality is. The `Is` structures allow you to expose which equality
> you're using at a particular point, whereas your suggestion would hide
> it.


A Semigroup can be only on some (magma : Magma _ _). This `magma'
already has an instance of _≈_ and of _∙_. 
What freedom has one to define  (H : Semigroup _ _)  on this particular
(magma : Magma _ _) ?
The only freedom is to choose a proof for  Associative _≈_ _∙_,
because _≈_ and _∙_ are already fixed, they are brought in by 
"open Setoid setoid ...".
So the matter here is only in the proof relevance.

For defining Magma on the given (S : Setoid), there is more freedom.
_≈_ is fixed, but _∙_ may be implemented in different ways.

 
> The `Is` structures allow you to expose which equality you're using at
> a particular point, whereas your suggestion would hide it.

No, in the experimental tower (let us call it so) the equality and all
operations are exposed by the `open' declaration:

-- experimental ------------------------------------------------------- 

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 _∙_

record Semigroup α α= :  Set (suc (α ⊔ α=))    -- non-standard
  where
  field magma : Magma α α=

  open Magma magma using (_≈_; _∙_)
  module FP≈ = FuncProp _≈_

  field ∙-assoc : FP≈.Associative _∙_
--------------------------------------------------------------------------

Here IsMagma (isMagma) is preserved as in standard, because this enables
us to define different Magmae on the same (S : Setoid).
But IsSemigroup (isSemigroup) is skipped, because it is not possible to
define different semigroups on the given (magma : Magma)
-- if only we ignore difference in proofs for FP≈.Associative _∙_.

Now I think that IsSemigroup is all right.
But repeated fields of Carrier, _≈_, and such, look strange to me.

Regards,

------
Sergei