diff --git a/Data/Natural/Class.hs b/Data/Natural/Class.hs
new file mode 100644
--- /dev/null
+++ b/Data/Natural/Class.hs
@@ -0,0 +1,18 @@
+module Data.Natural.Class where
+
+import Data.Functor.Const
+import Data.Peano
+import Data.Proxy
+
+class Natural n where
+    natural :: f Zero -> (∀ m . Natural m => f (Succ m)) -> f n
+
+instance Natural Zero where
+    natural zf _ = zf
+
+instance Natural n => Natural (Succ n) where
+    natural _ sf = sf
+
+reify :: Natural n => Proxy n -> Peano
+reify (Proxy :: Proxy n) = getConst $ natural @n (Const Zero) (φ $ Const . Succ . reify)
+  where φ = ($ Proxy) :: ∀ f a . (Proxy a -> f a) -> f a
diff --git a/natural-induction.cabal b/natural-induction.cabal
--- a/natural-induction.cabal
+++ b/natural-induction.cabal
@@ -1,5 +1,5 @@
 name:                natural-induction
-version:             0.1.0.1
+version:             0.1.1.0
 synopsis:            Induction over natural numbers
 -- description:         
 license:             BSD3
@@ -19,6 +19,8 @@
   -- hs-source-dirs:      
   default-language:    Haskell2010
   default-extensions:  UnicodeSyntax
+                     , ScopedTypeVariables
+                     , TypeApplications
                      , RankNTypes
                      , PolyKinds
                      , DataKinds