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