diff --git a/Test.hs b/Test.hs
--- a/Test.hs
+++ b/Test.hs
@@ -1,12 +1,13 @@
 module Main where
 
+import qualified Test.QuickCheck as Q
+
 import qualified Prelude
+import Data.Char (intToDigit)
+import Control.Monad (when)
 
-import Types.Data.Ord
-import Types.Data.Num
+import Types
 import Types.Data.Num.Decimal.Literals.TH
-import Types.Data.Bool
-import Data.SizedWord
 
 testIsPositive1 :: IsPositive D1 -> True
 testIsPositive1 = Prelude.id
@@ -55,6 +56,14 @@
 testSucc6 = Prelude.id
 testSucc7 :: Succ DN101 -> DN100
 testSucc7 = Prelude.id
+testSucc8 :: Succ D0 -> D1 :+: D0
+testSucc8 = Prelude.id
+testSucc9 :: Succ D0 -> D0 :+: D1
+testSucc9 = Prelude.id
+testSucc10 :: Succ D9 -> D1 :+: D9
+testSucc10 = Prelude.id
+testSucc11 :: Succ D9 -> D9 :+: D1
+testSucc11 = Prelude.id
 
 testPred1 :: Pred D1 -> D0
 testPred1 = Prelude.id
@@ -70,6 +79,28 @@
 testPred6 = Prelude.id
 testPred7 :: Pred D100 -> D99
 testPred7 = Prelude.id
+testPred8 :: Pred D0 -> D0 :-: D1
+testPred8 = Prelude.id
+testPred9 :: Pred D10 -> D10 :-: D1
+testPred9 = Prelude.id
+testPred10 :: Pred D9 -> D8
+testPred10 = Prelude.id
+testPred11 :: Pred D8 -> D7
+testPred11 = Prelude.id
+testPred12 :: Pred D7 -> D6
+testPred12 = Prelude.id
+testPred13 :: Pred D6 -> D5
+testPred13 = Prelude.id
+testPred14 :: Pred D5 -> D4
+testPred14 = Prelude.id
+testPred15 :: Pred D4 -> D3
+testPred15 = Prelude.id
+testPred16 :: Pred D3 -> D2
+testPred16 = Prelude.id
+testPred17 :: Pred D2 -> D1
+testPred17 = Prelude.id
+testPred18 :: Pred D1 -> D0
+testPred18 = Prelude.id
 
 testAdd1 :: D0 :+: D0 -> D0
 testAdd1 = Prelude.id
@@ -148,8 +179,65 @@
 testFac4 :: Fac D10 -> D3628800
 testFac4 = Prelude.id
 
-f :: n -> (n :+: D5)
-f _ = Prelude.undefined
+testEQ1 :: D0 :==: D0 -> True
+testEQ1 = Prelude.id
+testEQ2 :: D0 :==: Pred D1 -> True
+testEQ2 = Prelude.id
+testEQ3 :: (D1 :+: D9) :==: D10 -> True
+testEQ3 = Prelude.id
+testEQ4 :: (D1 :+: D9) :==: D11 -> False
+testEQ4 = Prelude.id
+testEQ5 :: D9 :==: D0 -> False
+testEQ5 = Prelude.id
+testEQ6 :: D8 :==: D0 -> False
+testEQ6 = Prelude.id
+testEQ7 :: D7 :==: D0 -> False
+testEQ7 = Prelude.id
+testEQ8 :: D6 :==: D0 -> False
+testEQ8 = Prelude.id
+testEQ9 :: D5 :==: D0 -> False
+testEQ9 = Prelude.id
+testEQ10 :: D4 :==: D0 -> False
+testEQ10 = Prelude.id
+testEQ11 :: D3 :==: D0 -> False
+testEQ11 = Prelude.id
+testEQ12 :: D2 :==: D0 -> False
+testEQ12 = Prelude.id
+testEQ13 :: D1 :==: D0 -> False
+testEQ13 = Prelude.id
 
-main :: Prelude.IO ()
-main = Prelude.return ()
+testMin1 :: Min D0 D5 -> D0
+testMin1 = Prelude.id
+testMin2 :: Min D5 D0 -> D0
+testMin2 = Prelude.id
+testMin3 :: Min DN5 D5 -> DN5
+testMin3 = Prelude.id
+
+testMax1 :: Max D1 D6 -> D6
+testMax1 = Prelude.id
+testMax2 :: Max DN6 D6 -> D6
+testMax2 = Prelude.id
+testMax3 :: Max D6 D1 -> D6
+testMax3 = Prelude.id
+
+class TestIter n zero where
+    testIter :: n -> zero -> Prelude.String
+
+instance ( NaturalT n
+         , (n :==: D0) ~ True )
+  => TestIter n True where
+    testIter _ _ = ""
+
+instance ( NaturalT n
+         , (n :==: D0) ~ False
+         , TestIter (Pred n) ((Pred n) :==: D0) )
+  => TestIter n False where
+    testIter n _ =
+        intToDigit (fromIntegerT n) : testIter (_T :: (Pred n)) (_T :: ((Pred n) :==: D0))
+
+main = do
+  let testIterResult = testIter d9 (_T :: False)
+  when (testIterResult Prelude./= "987654321") (Prelude.putStrLn ("testIter failed, got: " Prelude.++ testIterResult))
+  Q.quickCheck prop_reifyIntegral
+
+prop_reifyIntegral i = reifyIntegral (Prelude.undefined :: Decimal) i fromIntegerT Prelude.== i
diff --git a/Types/Data/Num.hs b/Types/Data/Num.hs
--- a/Types/Data/Num.hs
+++ b/Types/Data/Num.hs
@@ -15,7 +15,14 @@
 module Types.Data.Num
     ( module Types.Data.Num.Ops
     , module Types.Data.Num.Decimal
+    , reifyIntegralD
+    , reifyPositiveD
+    , reifyNegativeD
     ) where
 
 import Types.Data.Num.Ops
 import Types.Data.Num.Decimal
+
+reifyIntegralD = reifyIntegral decimal
+reifyPositiveD = reifyPositive decimal
+reifyNegativeD = reifyNegative decimal
diff --git a/Types/Data/Num/Decimal/Digits.hs b/Types/Data/Num/Decimal/Digits.hs
--- a/Types/Data/Num/Decimal/Digits.hs
+++ b/Types/Data/Num/Decimal/Digits.hs
@@ -20,6 +20,10 @@
 import Types.Data.List
 import Types.Data.Num.Ops
 
+-- | Representation name for decimal type level numbers.
+data Decimal
+decimal = undefined :: Decimal
+
 -- | The wrapper type for decimal type level numbers.
 data Dec x
 data Neg' x
diff --git a/Types/Data/Num/Decimal/Literals/TH.hs b/Types/Data/Num/Decimal/Literals/TH.hs
--- a/Types/Data/Num/Decimal/Literals/TH.hs
+++ b/Types/Data/Num/Decimal/Literals/TH.hs
@@ -2,11 +2,27 @@
 
 import Language.Haskell.TH
 
+import qualified Types.Data.Num.Decimal.Digits as D
+import qualified Types.Data.Num.Ops as O
+
 decLiteralT :: Integer -> Q Type
-decLiteralT n = appT (conT (mkName "Dec")) (decLiteralT' n)
-    where decLiteralT' n | n < 0     = appT (conT (mkName "Neg'")) (decLiteralT' (-n))
-                         | n == 0    = conT (mkName "DecN")
-                         | otherwise = appT (appT (conT (mkName ":.")) (decLiteralT' (n `div` 10))) (conT (mkName ("Dec" ++ show (n `mod` 10))))
+decLiteralT n = appT (conT (''D.Dec)) (decLiteralT' n)
+    where decLiteralT' n | n < 0     = appT (conT ''D.Neg') (decLiteralT' (-n))
+                         | n == 0    = conT ''D.DecN
+                         | otherwise = appT (appT (conT ''(O.:.)) (decLiteralT' (n `div` 10))) (conT (case n `mod` 10 of
+                                                  0 -> ''D.Dec0 
+                                                  1 -> ''D.Dec1
+                                                  2 -> ''D.Dec2
+                                                  3 -> ''D.Dec3
+                                                  4 -> ''D.Dec4
+                                                  5 -> ''D.Dec5
+                                                  6 -> ''D.Dec6
+                                                  7 -> ''D.Dec7
+                                                  8 -> ''D.Dec8
+                                                  9 -> ''D.Dec9))
+
+decLiteralV :: Integer -> Q Exp
+decLiteralV n = sigE [| undefined |] (decLiteralT n)
 
 decLiteralD :: String
             -> String
diff --git a/Types/Data/Num/Decimal/Ops.hs b/Types/Data/Num/Decimal/Ops.hs
--- a/Types/Data/Num/Decimal/Ops.hs
+++ b/Types/Data/Num/Decimal/Ops.hs
@@ -22,8 +22,30 @@
 import Types.Data.Num.Decimal.Literals
 import Types.Data.Num.Decimal.Digits
 
+instance IntegerR Decimal where
+    reifyIntegral _ i k = reifyIntegral' i (\(_ :: s) -> k (undefined :: Dec s))
+
+reifyIntegral' :: Integer -> (forall s. IntegerT' s => s -> w) -> w
+reifyIntegral' i k | i <  0    = go (negate i) (\(_ :: s) -> k (undefined :: Neg' s)) 
+                   | otherwise = go i k
+  where
+   go :: Integer -> (forall s. IntegerT' s => s -> w) -> w
+   go 0 k = k (undefined :: DecN)
+   go i k = let (j, d) =  quotRem i 10 in case d of
+     0 -> go j (\(_ :: s) -> k (undefined :: s :. Dec0))
+     1 -> go j (\(_ :: s) -> k (undefined :: s :. Dec1))
+     2 -> go j (\(_ :: s) -> k (undefined :: s :. Dec2))
+     3 -> go j (\(_ :: s) -> k (undefined :: s :. Dec3))
+     4 -> go j (\(_ :: s) -> k (undefined :: s :. Dec4))
+     5 -> go j (\(_ :: s) -> k (undefined :: s :. Dec5))
+     6 -> go j (\(_ :: s) -> k (undefined :: s :. Dec6))
+     7 -> go j (\(_ :: s) -> k (undefined :: s :. Dec7))
+     8 -> go j (\(_ :: s) -> k (undefined :: s :. Dec8))
+     9 -> go j (\(_ :: s) -> k (undefined :: s :. Dec9))
+
 instance IntegerT' x => IntegerT (Dec x) where
     fromIntegerT _ = fromIntegerT' (undefined :: x)
+    type Repr (Dec x) = Decimal
 
 class IntegerT' x where
     fromIntegerT' :: Num y => x -> y
diff --git a/Types/Data/Num/Ops.hs b/Types/Data/Num/Ops.hs
--- a/Types/Data/Num/Ops.hs
+++ b/Types/Data/Num/Ops.hs
@@ -50,10 +50,13 @@
     , div2T
     , Fac
     , facT
+    , IntegerR (..)
     , IntegerT (..)
     , NaturalT
     , PositiveT
     , NegativeT
+    , reifyPositive
+    , reifyNegative
     ) where
 
 import Types.Data.Bool
@@ -144,5 +147,39 @@
 class IntegerT x => NegativeT x
 instance (IntegerT x, IsNegative x ~ True) => NegativeT x
 
-class IntegerT x where
+class (IntegerR (Repr x)) => IntegerT x where
     fromIntegerT :: Num y => x -> y
+    type Repr x
+
+class IntegerR r where
+    reifyIntegral :: r -> Integer -> (forall s. (IntegerT s, Repr s ~ r) => s -> a) -> a
+
+
+--- positive and negative assertions: unsafe, in a trusted kernel
+data AssertPos x
+data AssertNeg x
+
+assertPos :: x -> AssertPos x
+assertPos _ = undefined
+
+assertNeg :: x -> AssertNeg x
+assertNeg _ = undefined
+
+type instance IsPositive (AssertPos x) = True
+type instance IsNegative (AssertNeg x) = True
+
+instance IntegerT x => IntegerT (AssertPos x) where 
+    fromIntegerT _ = fromIntegerT (undefined :: x)
+    type Repr (AssertPos x) = Repr x
+
+instance IntegerT x => IntegerT (AssertNeg x) where
+    fromIntegerT _ = fromIntegerT (undefined :: x)
+    type Repr (AssertNeg x) = Repr x
+
+reifyPositive :: IntegerR r => r -> Integer -> (forall s. (PositiveT s, Repr s ~ r) => s -> a) -> Maybe a
+reifyPositive r n k | n > 0     = Just (reifyIntegral r n (k . assertPos))
+                    | otherwise = Nothing
+
+reifyNegative :: IntegerR r => r -> Integer -> (forall s. (NegativeT s, Repr s ~ r) => s -> a) -> Maybe a
+reifyNegative r n k | n < 0     = Just (reifyIntegral r n (k . assertNeg))
+                    | otherwise = Nothing
diff --git a/Types/Data/Ord.hs b/Types/Data/Ord.hs
--- a/Types/Data/Ord.hs
+++ b/Types/Data/Ord.hs
@@ -34,6 +34,10 @@
     , geT
     , (:>:)
     , gtT
+    , Min
+    , minT
+    , Max
+    , maxT
     ) where
 
 import qualified Prelude
@@ -107,6 +111,16 @@
 type instance x :>: y = IsGT (Compare x y)
 gtT :: x -> y -> x :>: y
 gtT _ _ = Prelude.undefined
+
+type family Min x y
+type instance Min x y = If (x :<=: y) x y
+minT :: x -> y -> Min x y
+minT _ _ = Prelude.undefined
+
+type family Max x y
+type instance Max x y = If (x :>=: y) x y
+maxT :: x -> y -> Max x y
+maxT _ _ = Prelude.undefined
 
 type instance Compare False False = EQ
 type instance Compare False True  = LT
diff --git a/tfp.cabal b/tfp.cabal
--- a/tfp.cabal
+++ b/tfp.cabal
@@ -1,5 +1,5 @@
 name:           tfp
-version:        0.1
+version:        0.2
 cabal-version:  >= 1.2
 build-type:     Simple
 license:        BSD3
@@ -25,7 +25,8 @@
   extensions:     TypeFamilies, UndecidableInstances, TypeOperators,
                   EmptyDataDecls, DeriveDataTypeable, ScopedTypeVariables,
                   FlexibleInstances, TemplateHaskell, TypeSynonymInstances,
-                  MultiParamTypeClasses, GeneralizedNewtypeDeriving
+                  MultiParamTypeClasses, GeneralizedNewtypeDeriving,
+                  Rank2Types, FlexibleContexts
   build-depends:  base >= 3.0, template-haskell >= 2.0
   exposed-modules:
     Data.SizedInt,
@@ -55,7 +56,8 @@
   extensions:     TypeFamilies, UndecidableInstances, TypeOperators,
                   EmptyDataDecls, DeriveDataTypeable, ScopedTypeVariables,
                   FlexibleInstances, TemplateHaskell, TypeSynonymInstances,
-                  MultiParamTypeClasses, GeneralizedNewtypeDeriving
+                  MultiParamTypeClasses, GeneralizedNewtypeDeriving,
+                  FunctionalDependencies, Rank2Types, FlexibleContexts
   main-is: Test.hs
-  build-depends:  base >= 3.0, template-haskell >= 2.0
+  build-depends:  base >= 3.0, template-haskell >= 2.0, QuickCheck >= 1.2.0.0
 }