diff --git a/CHANGELOG.md b/CHANGELOG.md
index b025b64de8..35c634b8c3 100644
--- a/CHANGELOG.md
+++ b/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
diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda
index 88b195ec7d..fdb79e1fdd 100644
--- a/src/Algebra/Bundles.agda
+++ b/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
diff --git a/src/Algebra/Literals.agda b/src/Algebra/Literals.agda
new file mode 100644
index 0000000000..43266e5773
--- /dev/null
+++ b/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)
+