<div dir="ltr">Say you have a module and you want to parameterise it by a semigroup that <b>must</b> use propositional equality. How would you do that using your hierarchy?</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Mar 17, 2019 at 2:52 AM 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 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' structure<br>
>         is needed only in few cases.<br>
> <br>
> <br>
> I think your examples miss the point. For example take any binary<br>
> operator. That binary operator may form many different<br>
> Semigroups/Monoids/Groups etc. depending on what the underlying<br>
> equality is. The `Is` structures allow you to expose which equality<br>
> you're using at a particular point, whereas your suggestion would hide<br>
> it.<br>
<br>
<br>
A Semigroup can be only on some (magma : Magma _ _). This `magma'<br>
already has an instance of _≈_ and of _∙_. <br>
What freedom has one to define  (H : Semigroup _ _)  on this particular<br>
(magma : Magma _ _) ?<br>
The only freedom is to choose a proof for  Associative _≈_ _∙_,<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 freedom.<br>
_≈_ is fixed, but _∙_ may be implemented in different ways.<br>
<br>
<br>
> The `Is` structures allow you to expose which equality 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 and all<br>
operations are exposed by the `open' declaration:<br>
<br>
-- experimental ------------------------------------------------------- <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<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 this enables<br>
us to define different Magmae on the same (S : Setoid).<br>
But IsSemigroup (isSemigroup) is skipped, because it is not possible to<br>
define different semigroups on the given (magma : Magma)<br>
-- if only we ignore difference in proofs for FP≈.Associative _∙_.<br>
<br>
Now I think that IsSemigroup is all right.<br>
But repeated fields of Carrier, _≈_, and such, look strange to me.<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
</blockquote></div>