diff --git a/TypeLevel/Number/Int.hs b/TypeLevel/Number/Int.hs
--- a/TypeLevel/Number/Int.hs
+++ b/TypeLevel/Number/Int.hs
@@ -1,3 +1,8 @@
+{-# OPTIONS_GHC  -fno-warn-orphans #-}
+
+{-# LANGUAGE DeriveDataTypeable    #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE EmptyDataDecls        #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE FlexibleContexts      #-}
@@ -26,11 +31,15 @@
                         , D0
                         , D1
                         , IntT(..)
+                          -- ** Lifting
+                        , SomeInt
+                        , withInt
                           -- * Template haskell utilities
                         , intT
                         , module TypeLevel.Number.Classes
                         ) where
 
+import Data.Typeable (Typeable)
 import Language.Haskell.TH
 
 import TypeLevel.Number.Classes
@@ -43,8 +52,9 @@
 splitToTrits x | n == 0 =  0 : splitToTrits  rest
                | n == 1 =  1 : splitToTrits  rest
                | n == 2 = -1 : splitToTrits (rest + 1)
-                 where
-                   (rest,n) = divMod x 3
+               where
+                 (rest,n) = divMod x 3
+splitToTrits _ = error "Internal error"
 
 -- | Generate type for integer number.
 intT :: Integer -> TypeQ
@@ -84,9 +94,51 @@
 
 
 instance                Show    ZZ  where show _ = "[0:Z]"
-instance IntT (Dn n) => Show (Dn n) where show n = "["++show (toInt n)++":Z]"
-instance IntT (D0 n) => Show (D0 n) where show n = "["++show (toInt n)++":Z]"
-instance IntT (D1 n) => Show (D1 n) where show n = "["++show (toInt n)++":Z]"
+instance IntT (Dn n) => Show (Dn n) where show n = "["++show (toInt n :: Integer)++":Z]"
+instance IntT (D0 n) => Show (D0 n) where show n = "["++show (toInt n :: Integer)++":Z]"
+instance IntT (D1 n) => Show (D1 n) where show n = "["++show (toInt n :: Integer)++":Z]"
+
+
+-- | Some natural number
+data SomeInt where
+  SomeInt :: IntT n => n -> SomeInt
+  deriving Typeable
+
+instance Show SomeInt where
+  showsPrec d (SomeInt n) = showParen (d > 10) $
+    showString "withInt SomeInt " . shows (toInt n :: Integer)
+
+
+
+-- | Apply function which could work with any 'Nat' value only know at runtime.
+withInt :: forall i a. (Integral i) => (forall n. IntT n => n -> a) -> i -> a
+withInt f i0
+  | i0 == 0   = f (undefined :: ZZ)
+  | otherwise = cont (fromIntegral i0) f f f
+  where
+    cont :: Integer -> (forall n m. (IntT n, n ~ Dn m) => n -> a)
+                    -> (forall n m. (IntT n, n ~ D0 m) => n -> a)
+                    -> (forall n m. (IntT n, n ~ D1 m) => n -> a) -> a
+    cont (-1) kN _  _  = kN (undefined :: Dn ZZ)
+    cont   1  _  _  k1 = k1 (undefined :: D1 ZZ)
+    cont   i  kN k0 k1 = cont i' kN' k0' k1'
+      where
+        (i',bit) = case divMod i 3 of
+                     (x,2) -> (x+1,-1)
+                     x     -> x
+        kN' :: forall n m. (IntT n, n ~ Dn m) => n -> a
+        kN' _ | bit == -1 = kN (undefined :: Dn n)
+              | bit ==  0 = k0 (undefined :: D0 n)
+              | otherwise = k1 (undefined :: D1 n)
+        k0' :: forall n m. (IntT n, n ~ D0 m) => n -> a
+        k0' _ | bit == -1 = kN (undefined :: Dn n)
+              | bit ==  0 = k0 (undefined :: D0 n)
+              | otherwise = k1 (undefined :: D1 n)
+
+        k1' :: forall n m. (IntT n, n ~ D1 m) => n -> a
+        k1' _ | bit == -1 = kN (undefined :: Dn n)
+              | bit ==  0 = k0 (undefined :: D0 n)
+              | otherwise = k1 (undefined :: D1 n)
 
 ----------------------------------------------------------------
 -- Number normalization
diff --git a/TypeLevel/Number/Nat.hs b/TypeLevel/Number/Nat.hs
--- a/TypeLevel/Number/Nat.hs
+++ b/TypeLevel/Number/Nat.hs
@@ -1,3 +1,6 @@
+{-# OPTIONS_GHC  -fno-warn-orphans #-}
+
+{-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE EmptyDataDecls        #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE FlexibleContexts      #-}
@@ -7,6 +10,8 @@
 {-# LANGUAGE TemplateHaskell       #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE DeriveDataTypeable    #-}
 -- |
 -- Module      : TypeLevel.Number.Nat
 -- Copyright   : Alexey Khudyakov
@@ -48,6 +53,9 @@
                         , O
                         , Z
                         , Nat(..)
+                          -- ** Lifting
+                        , SomeNat(..)
+                        , withNat
                           -- * Template haskell utilities
                           -- $TH
                         , natT
@@ -55,8 +63,9 @@
                         , module TypeLevel.Number.Classes
                         ) where
 
-import Data.Word (Word8,Word16,Word32,Word64)
-import Data.Int  (Int8, Int16, Int32, Int64 )
+import Data.Word     (Word8,Word16,Word32,Word64)
+import Data.Int      (Int8, Int16, Int32, Int64 )
+import Data.Typeable (Typeable)
 
 import TypeLevel.Number.Classes
 import TypeLevel.Number.Nat.Types
@@ -97,6 +106,38 @@
 instance (Nat n, Positive n) => Pos n
 
 
+-- | Some natural number
+data SomeNat where
+  SomeNat :: Nat n => n -> SomeNat
+  deriving Typeable
+
+instance Show SomeNat where
+  showsPrec d (SomeNat n) = showParen (d > 10) $
+    showString "withNat SomeNat " . shows (toInt n :: Integer)
+
+
+
+-- | Apply function which could work with any 'Nat' value only know at runtime.
+withNat :: forall i a. (Integral i) => (forall n. Nat n => n -> a) -> i -> a
+withNat f i0
+  | i0 <  0   = error "TypeLevel.Number.Nat.withNat: negative number"
+  | i0 == 0   = f (undefined :: Z)
+  | otherwise = cont (fromIntegral i0) f f
+  where
+    cont :: Integer -> (forall n m. (Nat n, n ~ O m) => n -> a)
+                    -> (forall n m. (Nat n, n ~ I m) => n -> a) -> a
+    cont 1 _  k1 = k1 (undefined :: I Z)
+    cont i k0 k1 = cont (i `quot` 2) k0' k1'
+      where
+        k0' :: forall n m. (Nat n, n ~ O m) => n -> a
+        k0' _ | odd i     = k1 (undefined :: I n)
+              | otherwise = k0 (undefined :: O n)
+        k1' :: forall n m. (Nat n, n ~ I m) => n -> a
+        k1' _ | odd i     = k1 (undefined :: I n)
+              | otherwise = k0 (undefined :: O n)
+
+
+
 ----------------------------------------------------------------
 -- Data conversion
 
@@ -167,8 +208,8 @@
 -- Show instances.
 -- Nat contexts are used to ensure correctness of numbers.
 instance              Show    Z  where show _ = "[0:N]"
-instance Nat (O n) => Show (O n) where show n = "["++show (toInt n)++":N]"
-instance Nat (I n) => Show (I n) where show n = "["++show (toInt n)++":N]"
+instance Nat (O n) => Show (O n) where show n = "["++show (toInt n :: Integer)++":N]"
+instance Nat (I n) => Show (I n) where show n = "["++show (toInt n :: Integer)++":N]"
 
 ----------------------------------------------------------------
 -- Next number.
diff --git a/TypeLevel/Number/Nat/TH.hs b/TypeLevel/Number/Nat/TH.hs
--- a/TypeLevel/Number/Nat/TH.hs
+++ b/TypeLevel/Number/Nat/TH.hs
@@ -1,8 +1,5 @@
 {-# LANGUAGE TemplateHaskell #-}
-module TypeLevel.Number.Nat.TH ( nat
-                               , natT
-                               ) where
-
+module TypeLevel.Number.Nat.TH where
 
 import Language.Haskell.TH
 import TypeLevel.Number.Nat.Types
diff --git a/TypeLevel/Reify.hs b/TypeLevel/Reify.hs
--- a/TypeLevel/Reify.hs
+++ b/TypeLevel/Reify.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE DeriveDataTypeable    #-}
 -- |
 -- Module      : TypeLevel.Reify
 -- Copyright   : Alexey Khudyakov
@@ -11,9 +12,12 @@
                        , Reify(..)
                        ) where
 
+import Data.Data (Data,Typeable)
 
+
+-- | Value with type tag
 data Witness t a = Witness { getValue :: a }
-                   deriving Show
+                   deriving (Show,Eq,Typeable,Data)
 
 -- | Convert type level into value level using 
 class Reify t a where
diff --git a/type-level-numbers.cabal b/type-level-numbers.cabal
--- a/type-level-numbers.cabal
+++ b/type-level-numbers.cabal
@@ -1,5 +1,5 @@
 Name:           type-level-numbers
-Version:        0.1.0.4
+Version:        0.1.1.0
 Synopsis:       
   Type level numbers implemented using type families.
 Description:
@@ -22,6 +22,10 @@
   So far comparison of numbers, subtraction and multiplication of
   numbers are supported.
   .
+  Changes in 0.1.1.0
+  .
+  * @withNat@, @withInt@, @SomeNat and @SomeInt@ added.
+  .
   Changes in 0.1.0.3
   .
   * Fix build for GHC 7.4
@@ -53,7 +57,7 @@
 
 
 Library
-  ghc-options:     -Wall -fno-warn-orphans
+  ghc-options:     -Wall
   Build-Depends:   base >=3 && <5,
                    template-haskell > 2.0
   Exposed-modules: TypeLevel.Number.Classes