[fixes #1363] Add Algebra.Literals

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
+  ```
+
 * `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures
 
 Additions to existing modules

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)

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

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)

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 }

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 ו