Add Number literals for any SuccessorSet

CHANGELOG.md

@@ -116,6 +116,11 @@ New modules
   Algebra.Construct.Pointwise
   ```
 
+* `Number` literals derivable from any `SuccessorSet`:
+  ```
+  Algebra.Literals
+  ```
+
 * Raw bundles for module-like algebraic structures:
   ```
   Algebra.Module.Bundles.Raw

src/Algebra/Bundles.agda

@@ -44,7 +44,6 @@ record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) where
   rawSuccessorSet : RawSuccessorSet _ _
   rawSuccessorSet = record { _≈_ = _≈_; suc# = suc#; zero# = zero# }
 
-  open RawSuccessorSet rawSuccessorSet public
 
 ------------------------------------------------------------------------
 -- Bundles with 1 binary operation

src/Algebra/Literals.agda

@@ -0,0 +1,29 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Algebra Literals, from a SuccessorSet
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (SuccessorSet)
+
+module Algebra.Literals {c ℓ} (successorSet : SuccessorSet c ℓ) where
+
+open import Agda.Builtin.FromNat using (Number)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+open import Data.Unit.Polymorphic.Base
+
+open SuccessorSet successorSet
+
+
+------------------------------------------------------------------------
+-- Number instance
+
+fromℕ : (n : ℕ) → Carrier
+fromℕ zero    = zero#
+fromℕ (suc n) = suc# (fromℕ n)
+
+instance
+  number : Number Carrier
+  number = record { Constraint = λ _ → ⊤ ; fromNat = λ n → fromℕ n }