From 018aa65f1eebc67641be89d52fa4f508ba23050b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 24 Jan 2024 10:06:58 +0000 Subject: [PATCH] possible fix for #1363 --- CHANGELOG.md | 11 ++++++ src/Algebra/Bundles/Literals.agda | 19 +++++++++++ src/Algebra/Bundles/Pointed.agda | 50 ++++++++++++++++++++++++++++ src/Algebra/Literals.agda | 20 +++++++++++ src/Algebra/Structures/Literals.agda | 21 ++++++++++++ src/Algebra/Structures/Pointed.agda | 49 +++++++++++++++++++++++++++ 6 files changed, 170 insertions(+) create mode 100644 src/Algebra/Bundles/Literals.agda create mode 100644 src/Algebra/Bundles/Pointed.agda create mode 100644 src/Algebra/Literals.agda create mode 100644 src/Algebra/Structures/Literals.agda create mode 100644 src/Algebra/Structures/Pointed.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index c690740a1e..5ee4e8f8e6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -33,6 +33,17 @@ Deprecated names New modules ----------- +* Adding a distinguished point `•` (\bu2) to `Monoid`, and using it to define + abstract 'literals' for any `PointedMonoid`, with the intended mode-of-use + being to instantiate the point with `1#` from any (semi)ring-like structure: + ```agda + module Algebra.Bundles.Literals + module Algebra.Bundles.Pointed + module Algebra.Structures.Literals + module Algebra.Structures.Pointed + module Algebra.Literals + ``` + Additions to existing modules ----------------------------- diff --git a/src/Algebra/Bundles/Literals.agda b/src/Algebra/Bundles/Literals.agda new file mode 100644 index 0000000000..ff354e694b --- /dev/null +++ b/src/Algebra/Bundles/Literals.agda @@ -0,0 +1,19 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Algebra Literals, from a PointedMonoid bundle +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles.Pointed + +module Algebra.Bundles.Literals + {c ℓ} (pointedMonoid : PointedMonoid c ℓ) + where + +open PointedMonoid pointedMonoid + +-- Re-export `Number` instance defined in Algebra.Structures.Literals + +open import Algebra.Structures.Literals isPointedMonoid public using (number) diff --git a/src/Algebra/Bundles/Pointed.agda b/src/Algebra/Bundles/Pointed.agda new file mode 100644 index 0000000000..9d6a08c4dd --- /dev/null +++ b/src/Algebra/Bundles/Pointed.agda @@ -0,0 +1,50 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- `Pointed` intermediate between `Monoid` and `SemiringWithoutAnnihilatingZero` +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles +open import Algebra.Bundles.Raw +open import Algebra.Core +open import Algebra.Structures.Pointed as Pointed using (IsPointedMonoid) +import Algebra.Properties.Monoid.Mult as Mult +open import Data.Nat.Base as ℕ using (ℕ) +open import Data.Unit.Base +open import Level using (Level; suc; _⊔_; Lift) +open import Relation.Binary.Core using (Rel) + +module Algebra.Bundles.Pointed where + +private + variable + c ℓ : Level + +------------------------------------------------------------------------ +-- Bundles with 1 binary operation & 2 elements +------------------------------------------------------------------------ + +record PointedMonoid c ℓ : Set (suc (c ⊔ ℓ)) where + field + rawMonoid : RawMonoid c ℓ + open RawMonoid rawMonoid using (Carrier) + field + • : Carrier + isPointedMonoid : IsPointedMonoid rawMonoid • + + open IsPointedMonoid isPointedMonoid public + +------------------------------------------------------------------------ +-- instance from any SemiringWithoutAnnihilatingZero + +pointedMonoid : SemiringWithoutAnnihilatingZero c ℓ → PointedMonoid c ℓ +pointedMonoid semiringWithoutAnnihilatingZero + = record { isPointedMonoid = isPointedMonoid } + where + open SemiringWithoutAnnihilatingZero semiringWithoutAnnihilatingZero + using (1#; +-rawMonoid; +-isMonoid) + isPointedMonoid : IsPointedMonoid +-rawMonoid 1# + isPointedMonoid = record { isMonoid = +-isMonoid } + diff --git a/src/Algebra/Literals.agda b/src/Algebra/Literals.agda new file mode 100644 index 0000000000..6336c3c537 --- /dev/null +++ b/src/Algebra/Literals.agda @@ -0,0 +1,20 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Algebra Literals, from a SemiringWithoutAnnihilatingZero +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (SemiringWithoutAnnihilatingZero) + +module Algebra.Literals {c ℓ} + (semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero c ℓ) + where + +open import Algebra.Bundles.Pointed + +-- Re-export `Number` instance defined in Algebra.Bundles.Literals + +open import Algebra.Bundles.Literals + (pointedMonoid semiringWithoutAnnihilatingZero) public using (number) diff --git a/src/Algebra/Structures/Literals.agda b/src/Algebra/Structures/Literals.agda new file mode 100644 index 0000000000..844941561d --- /dev/null +++ b/src/Algebra/Structures/Literals.agda @@ -0,0 +1,21 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Algebra Literals +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles.Raw +open import Algebra.Structures.Pointed + +module Algebra.Structures.Literals + {c ℓ} {rawMonoid : RawMonoid c ℓ} {•} + (isPointedMonoid : IsPointedMonoid rawMonoid •) + where + +open import Agda.Builtin.FromNat +open IsPointedMonoid isPointedMonoid + +number : Number Carrier +number = record { Literals } diff --git a/src/Algebra/Structures/Pointed.agda b/src/Algebra/Structures/Pointed.agda new file mode 100644 index 0000000000..1dbf8b38b9 --- /dev/null +++ b/src/Algebra/Structures/Pointed.agda @@ -0,0 +1,49 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Defines `IsPointedMonoid` +-- intermediate between `Monoid` and `SemiringWithoutAnnihilatingZero` +-- +-- By contrast with the rest of `Algebra.Structures`, this is modelled +-- on an underlying `RawMonoid`, rather than a 'flattened' such signature +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles.Raw +import Algebra.Structures as Structures +open import Data.Nat.Base as ℕ using (ℕ) +open import Data.Unit.Base +open import Level using (Level; _⊔_; Lift) + +import Algebra.Definitions.RawMonoid as Definitions + +module Algebra.Structures.Pointed where + +private + variable + c ℓ : Level + + +------------------------------------------------------------------------ +-- Structures with 1 binary operation & 2 elements +------------------------------------------------------------------------ + +record IsPointedMonoid + (rawMonoid : RawMonoid c ℓ) + (• : RawMonoid.Carrier rawMonoid) : Set (c ⊔ ℓ) + where + open RawMonoid rawMonoid public + open Structures _≈_ + + field + isMonoid : IsMonoid _∙_ ε + + _ו : ℕ → Carrier + n ו = n × • where open Definitions rawMonoid + + module Literals where + Constraint : ℕ → Set c + Constraint _ = Lift c ⊤ + fromNat : ∀ n → {{Constraint n}} → Carrier + fromNat n = n ו