[Agda] algebra hierarchy in library

[Matthew Daggitt]

Would you agree that writing

module Semigroup≡ {a} {A : Set a} {_∙_ : Op₂ A} (isSemigroup : IsSemigroup
_≡_ _∙_) where

is easier than writing the "proper part" you've got above?

On Wed, Mar 20, 2019 at 10:39 PM Sergei Meshveliani <mechvel at botik.ru>
wrote:

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