diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
index 1cf2634..58fd4a7 100644
--- a/src/Data/Nat.hs
+++ b/src/Data/Nat.hs
@@ -75,6 +75,10 @@ singletons [d|
   max Z        n  = n
   max n        Z  = n
   max (S n) (S m) = S (max n m)
+
+  fact ∷ ℕ → ℕ
+  fact Z     = S Z
+  fact (S n) = (S n) × (fact n)
   |]