Add Number literals for any SuccessorSet

CHANGELOG.md

@@ -90,6 +90,11 @@ Deprecated names
 New modules
 -----------
 
+* `Number` literals derivable from any `RawSuccessorSet`:
+  ```agda
+  Algebra.Literals
+  ```
+
 * Bundled morphisms between (raw) algebraic structures:
   ```
   Algebra.Morphism.Bundles

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.Raw using (RawSuccessorSet)
+
+module Algebra.Literals {c ℓ} (rawSuccessorSet : RawSuccessorSet c ℓ) where
+
+open import Agda.Builtin.FromNat using (Number)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+open import Data.Unit.Polymorphic.Base using (⊤)
+
+open RawSuccessorSet rawSuccessorSet
+
+
+------------------------------------------------------------------------
+-- Number instance
+
+number : Number Carrier
+number = record { Constraint = λ _ → ⊤ ; fromNat = λ n → fromℕ n }
+  where
+  fromℕ : (n : ℕ) → Carrier
+  fromℕ zero    = zero#
+  fromℕ (suc n) = suc# (fromℕ n)
+