[Agda] algebra hierarchy in library

[Matthew Daggitt]

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?

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
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190320/7e3a2dd8/attachment.html>