[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