[Agda] algebra hierarchy in library

[Sergei Meshveliani]

On Wed, 2019-03-20 at 11:44 +0800, Matthew Daggitt wrote:
> Say you have a module and you want to parameterise it by a semigroup
> that must use propositional equality. How would you do that using your
> hierarchy?


Let me try. 
The prelude is the definition of Magma and Semigroup by the approach II:
a) with isMagma, b) without isSemigroup, 
     c) without repeating fields. 

Then,  module Semigroup≡  is a submodule in  module Magma≡.
But it can be also declared as a top level module, with joining
parameters C, _∙_, isMagma≡.

What is wrong here?

--
SM
 

--====================================================================
open import Level using (suc; _⊔_) 
open import Algebra.FunctionProperties as FuncProp using (Op₂)
open import Relation.Binary using (_Preserves₂_⟶_⟶_; Setoid) 
open import Relation.Binary.PropositionalEquality as PE using (_≡_)

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

record Magma α α= :  Set (suc (α ⊔ α=))  
  where                            -- non-standard but with `isMagma'
  constructor magma′
  
  field  setoid : Setoid α α=

  open Setoid setoid public
  infixl 7 _∙_

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


record Semigroup α α= :  Set (suc (α ⊔ α=))  -- without `isSemigroup'
  where                                         
  constructor semigroup′
  
  field magma : Magma α α=

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

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


-- The proper part =================================================
-- Magma≡  is parameterized by a certain representation of arbitrary 
--         magma over _≡_.

module Magma≡ {α} (C : Set α) (_∙_ : Op₂ C)
                  (let setoid≡ = PE.setoid C)
                  (isMagma≡ : IsMagma setoid≡ _∙_)
  where
  magma≡ :  Magma α _
  magma≡ =  magma′ setoid≡ _∙_ isMagma≡

  module FP≡ =  FuncProp (_≡_ {A = C})
 
  -------------------------------------------------------------------
  -- Semigroup≡  is parameterized by a certain representation of
  --             arbitrary semigroup over _≡_,
  -- and  semigroup≡  below is an arbitrary semigroup over _≡_. 
  
  module Semigroup≡ (∙assoc : FP≡.Associative _∙_)
    where
    semigroup≡ :  Semigroup α _
    semigroup≡ =  semigroup′ magma≡ ∙assoc

    {-
    ...
    -}
--------------------------------------------------------------------






> On Sun, Mar 17, 2019 at 2:52 AM Sergei Meshveliani <mechvel at botik.ru>
> wrote:
> 
>         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
>         
>         
>