diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
index e53f1aa..95aef0d 100644
--- a/src/Data/Nat.hs
+++ b/src/Data/Nat.hs
@@ -55,6 +55,11 @@ singletons [d|
   Z     × m = Z
   (S n) × m = (n × m) + m
 
+  -- | Exponentiation
+  (^) ∷ ℕ → ℕ → ℕ
+  n ^ Z     = (S Z)
+  n ^ (S m) = n × (n ^ m)
+
   -- | Ordering relation <
   (<) ∷ ℕ → ℕ → 𝔹
   Z     < Z     = F