<div dir="ltr"><div>Would you agree that writing</div><div><br></div><div>module Semigroup≡ {a} {A : Set a} {_∙_ : Op₂ A} (isSemigroup : IsSemigroup _≡_ _∙_) where</div><div><br></div><div>is easier than writing the "proper part" you've got above?</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Mar 20, 2019 at 10:39 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On Wed, 2019-03-20 at 11:44 +0800, Matthew Daggitt wrote:<br>
> Say you have a module and you want to parameterise it by a semigroup<br>
> that must use propositional equality. How would you do that using your<br>
> hierarchy?<br>
<br>
<br>
Let me try. <br>
The prelude is the definition of Magma and Semigroup by the approach II:<br>
a) with isMagma, b) without isSemigroup, <br>
     c) without repeating fields. <br>
<br>
Then,  module Semigroup≡  is a submodule in  module Magma≡.<br>
But it can be also declared as a top level module, with joining<br>
parameters C, _∙_, isMagma≡.<br>
<br>
What is wrong here?<br>
<br>
--<br>
SM<br>
<br>
<br>
--====================================================================<br>
open import Level using (suc; _⊔_) <br>
open import Algebra.FunctionProperties as FuncProp using (Op₂)<br>
open import Relation.Binary using (_Preserves₂_⟶_⟶_; Setoid) <br>
open import Relation.Binary.PropositionalEquality as PE using (_≡_)<br>
<br>
record IsMagma {α α=} (S : Setoid α α=) (_∙_ : Op₂ (Setoid.Carrier S)) :<br>
                                                           Set (α ⊔ α=)<br>
  where<br>
  open Setoid S using (_≈_; Carrier)<br>
  field<br>
    ∙-cong : _∙_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_<br>
<br>
record Magma α α= :  Set (suc (α ⊔ α=))  <br>
  where                            -- non-standard but with `isMagma'<br>
  constructor magma′<br>
<br>
  field  setoid : Setoid α α=<br>
<br>
  open Setoid setoid public<br>
  infixl 7 _∙_<br>
<br>
  field  _∙_     : Op₂ Carrier<br>
         isMagma : IsMagma setoid _∙_<br>
<br>
<br>
record Semigroup α α= :  Set (suc (α ⊔ α=))  -- without `isSemigroup'<br>
  where                                         <br>
  constructor semigroup′<br>
<br>
  field magma : Magma α α=<br>
<br>
  open Magma magma using (_≈_; _∙_)<br>
  module FP≈ = FuncProp _≈_<br>
<br>
  field ∙-assoc : FP≈.Associative _∙_  <br>
<br>
<br>
-- The proper part =================================================<br>
-- Magma≡  is parameterized by a certain representation of arbitrary <br>
--         magma over _≡_.<br>
<br>
module Magma≡ {α} (C : Set α) (_∙_ : Op₂ C)<br>
                  (let setoid≡ = PE.setoid C)<br>
                  (isMagma≡ : IsMagma setoid≡ _∙_)<br>
  where<br>
  magma≡ :  Magma α _<br>
  magma≡ =  magma′ setoid≡ _∙_ isMagma≡<br>
<br>
  module FP≡ =  FuncProp (_≡_ {A = C})<br>
<br>
  -------------------------------------------------------------------<br>
  -- Semigroup≡  is parameterized by a certain representation of<br>
  --             arbitrary semigroup over _≡_,<br>
  -- and  semigroup≡  below is an arbitrary semigroup over _≡_. <br>
<br>
  module Semigroup≡ (∙assoc : FP≡.Associative _∙_)<br>
    where<br>
    semigroup≡ :  Semigroup α _<br>
    semigroup≡ =  semigroup′ magma≡ ∙assoc<br>
<br>
    {-<br>
    ...<br>
    -}<br>
--------------------------------------------------------------------<br>
<br>
<br>
<br>
<br>
<br>
<br>
> On Sun, Mar 17, 2019 at 2:52 AM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>><br>
> wrote:<br>
> <br>
>         On Sat, 2019-03-16 at 18:16 +0800, Matthew Daggitt wrote:<br>
>         >[..]<br>
>         <br>
>         >         If this is the only reason, then it occurs that `Is'<br>
>         structure<br>
>         >         is needed only in few cases.<br>
>         > <br>
>         > <br>
>         > I think your examples miss the point. For example take any<br>
>         binary<br>
>         > operator. That binary operator may form many different<br>
>         > Semigroups/Monoids/Groups etc. depending on what the<br>
>         underlying<br>
>         > equality is. The `Is` structures allow you to expose which<br>
>         equality<br>
>         > you're using at a particular point, whereas your suggestion<br>
>         would hide<br>
>         > it.<br>
>         <br>
>         <br>
>         A Semigroup can be only on some (magma : Magma _ _). This<br>
>         `magma'<br>
>         already has an instance of _≈_ and of _∙_. <br>
>         What freedom has one to define  (H : Semigroup _ _)  on this<br>
>         particular<br>
>         (magma : Magma _ _) ?<br>
>         The only freedom is to choose a proof for  Associative _≈_<br>
>         _∙_,<br>
>         because _≈_ and _∙_ are already fixed, they are brought in by <br>
>         "open Setoid setoid ...".<br>
>         So the matter here is only in the proof relevance.<br>
>         <br>
>         For defining Magma on the given (S : Setoid), there is more<br>
>         freedom.<br>
>         _≈_ is fixed, but _∙_ may be implemented in different ways.<br>
>         <br>
>         <br>
>         > The `Is` structures allow you to expose which equality<br>
>         you're using at<br>
>         > a particular point, whereas your suggestion would hide it.<br>
>         <br>
>         No, in the experimental tower (let us call it so) the equality<br>
>         and all<br>
>         operations are exposed by the `open' declaration:<br>
>         <br>
>         -- experimental<br>
>         ------------------------------------------------------- <br>
>         <br>
>         record IsMagma {α α=} (S : Setoid α α=) (_∙_ : Op₂<br>
>         (Setoid.Carrier S)) :<br>
>                                                                    Set<br>
>         (α ⊔ α=)<br>
>           where<br>
>           open Setoid S using (_≈_; Carrier)<br>
>           field<br>
>             ∙-cong : _∙_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_<br>
>         <br>
>         record Magma α α= :  Set (suc (α ⊔ α=))<br>
>           where<br>
>           field  setoid : Setoid α α=<br>
>         <br>
>           open Setoid setoid public<br>
>           infixl 7 _∙_<br>
>         <br>
>           field  _∙_     : Op₂ Carrier<br>
>                  isMagma : IsMagma setoid _∙_<br>
>         <br>
>         record Semigroup α α= :  Set (suc (α ⊔ α=))    -- non-standard<br>
>           where<br>
>           field magma : Magma α α=<br>
>         <br>
>           open Magma magma using (_≈_; _∙_)<br>
>           module FP≈ = FuncProp _≈_<br>
>         <br>
>           field ∙-assoc : FP≈.Associative _∙_<br>
>         --------------------------------------------------------------------------<br>
>         <br>
>         Here IsMagma (isMagma) is preserved as in standard, because<br>
>         this enables<br>
>         us to define different Magmae on the same (S : Setoid).<br>
>         But IsSemigroup (isSemigroup) is skipped, because it is not<br>
>         possible to<br>
>         define different semigroups on the given (magma : Magma)<br>
>         -- if only we ignore difference in proofs for FP≈.Associative<br>
>         _∙_.<br>
>         <br>
>         Now I think that IsSemigroup is all right.<br>
>         But repeated fields of Carrier, _≈_, and such, look strange to<br>
>         me.<br>
>         <br>
>         Regards,<br>
>         <br>
>         ------<br>
>         Sergei<br>
>         <br>
>         <br>
>         <br>
<br>
<br>
</blockquote></div>