[Agda] algebra hierarchy in library

Sergei Meshveliani mechvel at botik.ru
Thu Mar 21 11:18:41 CET 2019


On Thu, 2019-03-21 at 09:39 +0800, Matthew Daggitt wrote:
> 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?


The "proper part" can be written shorter as 

 module Semigroup≡ {α} {C : Set α} (_∙_ : Op₂ A)
                 (isMagma≡ : IsMagma (PE.setoid A) _∙_)
                 (∙assoc   : Associative' _≡_ _∙_)      where
,
where  Associative'  is the variant of Associative that takes equality
instead of a setoid. 

Still your version is simpler.
I see, thank you.

------
Sergei






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




More information about the Agda mailing list