diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,26 @@
+Copyright (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch and
+ SAM Group at the School of Information and Communication  Technology,
+ (Royal Institute of Technology, Stockholm, Sweden)
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+    * Redistributions in binary form must reproduce the above copyright
+      notice, this list of conditions and the following disclaimer in the
+      documentation and/or other materials provided with the distribution.
+    * Neither the name of The ForSyDe Team nor the
+      names of its contributors may be used to endorse or promote products
+      derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY
+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS TEAM BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,7 @@
+#! /usr/bin/env runhaskell
+module Main (main) where
+
+import Distribution.Simple
+
+main :: IO ()
+main = defaultMain
diff --git a/src/Data/TypeLevel.hs b/src/Data/TypeLevel.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel.hs
@@ -0,0 +1,20 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file src/Data/LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- This module is a wrapper for all the publicly usable types and functions
+-- of the type-level library.
+-- 
+-----------------------------------------------------------------------------
+module Data.TypeLevel (module Data.TypeLevel.Num, 
+                       module Data.TypeLevel.Bool) where
+
+import Data.TypeLevel.Num
+import Data.TypeLevel.Bool
diff --git a/src/Data/TypeLevel/Bool.hs b/src/Data/TypeLevel/Bool.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Bool.hs
@@ -0,0 +1,191 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies,
+             Rank2Types, DeriveDataTypeable, FlexibleInstances,
+             UndecidableInstances, FlexibleContexts,ScopedTypeVariables,
+             TypeFamilies
+  #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Bool
+-- Copyright   : (c) 2008 Benedikt Huber (port to Associative types (ghc 6.9+)) 
+--               (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental (MPTC, non-standarad instances)
+-- Portability :  non-portable
+--
+-- Type-level Booleans.
+-- 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Bool (
+    -- * Type-level boolean values
+    -- Bool, toBool,
+    False, false,
+    True, true,
+    -- reifyBool,
+    -- * Type-level boolean operations
+    Not,
+    And,
+    Or
+    -- Not, not,
+    -- And, (&&),
+    -- Or, (||),
+    -- Xor, xor,
+    -- Impl, imp,
+) where
+
+import Data.Generics (Typeable)
+import Prelude hiding (Bool, not, (&&), (||), Eq)
+import qualified Prelude as P
+
+------------------------------------
+-- Definition of type-level Booleans
+------------------------------------
+-- | True type-level value
+data True deriving Typeable
+
+instance Show True where
+ show _ = "True"
+
+-- | True value-level reflecting function
+true :: True
+true = undefined
+
+-- | False type-level value
+data False deriving Typeable
+
+instance Show False where
+ show _ = "False"
+
+
+-- | False value-level reflecting function
+false :: False
+false = undefined
+
+type family And b_0 b_1
+type instance And True True   = True
+type instance And True False  = False
+type instance And False True  = False
+type instance And False False = False
+
+type family Or b_0 b_1
+type instance Or True True   = True
+type instance Or True False  = True
+type instance Or False True  = True
+type instance Or False False = False
+
+type family Not b
+type instance Not True  = False
+type instance Not False = True
+
+#if 0
+type family Id b
+type family Const a b
+type instance Id a = a
+type instance Const b a = b
+-- | Booleans, internal version
+class BoolI b  where
+  toBool :: b -> P.Bool
+  type Not  b
+  type And  b :: * -> *
+  type Or   b :: * -> *
+  type Xor  b :: * -> *
+  type Impl b :: * -> *
+  type BoolEq b :: * -> *
+
+-- To prevent the user from adding new instances to BoolI we do NOT export 
+-- BoolI itself. Rather, we export the following proxy (Bool). 
+-- The proxy entails BoolI and so can be used to add BoolI 
+-- constraints in the signatures. However, all the constraints below
+-- are expressed in terms of BoolI rather than the proxy. Thus, even if the 
+-- user adds new instances to the proxy, it would not matter. 
+-- Besides, because the following proxy instances are most general,
+-- one may not add further instances without the overlapping instances 
+-- extension.
+
+-- | Type-level Booleans
+class BoolI b => Bool b
+  
+instance BoolI b => Bool b
+
+instance BoolI True where
+ toBool _ = True
+ type Not True = False
+ type And True = Id
+ type Or  True = Const True
+ type Xor True = Not
+ type Impl True = Id
+ type BoolEq True = Id
+ 
+instance BoolI False where
+ toBool _ = False
+ type Not False = True
+ type And False = Const False
+ type Or  False = Id
+ type Xor False = Id
+ type Impl False = Const True
+ type BoolEq False = Not
+-- | Reification function. In CPS style (best possible solution)
+reifyBool :: P.Bool -> (forall b . Bool b => b -> r) -> r
+reifyBool True  f = f true
+reifyBool False f = f false
+
+-------------
+-- Operations
+-------------
+
+
+-- | value-level reflection function for the 'Not' type-level relation
+not :: b1 -> Not b1
+not = undefined
+
+-- | 'And' type-level relation. @And b1 b2 b3@ establishes that
+--   @b1 && b2 = b3@
+
+
+-- | value-level reflection function for the 'And' type-level relation
+(&&) :: b1 -> b2 -> And b1 b2
+(&&) = undefined
+infixr 3 &&
+  
+-- | Or type-level relation. @Or b1 b2 b3@ establishes that
+--   @b1 || b2 = b3@
+
+
+-- | value-level reflection function for the 'Or' type-level relation
+(||) :: b1 -> b2 -> Or b1 b2
+(||) = undefined
+infixr 2 ||
+
+-- | Exclusive or type-level relation. @Xor b1 b2 b3@ establishes that
+--   @xor b1 b2 = b3@
+
+-- | value-level reflection function for the 'Xor' type-level relation
+xor :: b1 -> b2 -> Xor b1 b2
+xor = undefined
+
+
+-- | Implication type-level relation. @Imp b1 b2 b3@ establishes that
+-- @b1 =>b2 = b3@
+
+-- | value-level reflection function for the Imp type-level relation
+imp :: b1 -> b2 -> Impl b1 b2
+imp = undefined
+
+
+-- Although equality can be defined as the composition of Xor and Not
+-- we define it specifically
+
+-- | Boolean equality type-level relation
+
+-- FIXME: eq should be named (==) but it clashes with the (==) defined
+--        in Data.TypeLevel.Num . The chosen (and ugly) workaround was 
+--        to rename it to eq.
+
+-- | value-level reflection function for the 'Eq' type-level relation
+boolEq :: b1 -> b2 -> BoolEq b1 b2
+boolEq = undefined
+#endif
+
diff --git a/src/Data/TypeLevel/Num.hs b/src/Data/TypeLevel/Num.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Num.hs
@@ -0,0 +1,25 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Num
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- This module is a wrapper for all the publicly usable numerical types and 
+-- functions of the type-level library.
+-- 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Num 
+ (module Data.TypeLevel.Num.Reps,
+  module Data.TypeLevel.Num.Aliases,
+  module Data.TypeLevel.Num.Sets,
+  module Data.TypeLevel.Num.Ops) where
+
+import Data.TypeLevel.Num.Reps
+import Data.TypeLevel.Num.Aliases
+import Data.TypeLevel.Num.Sets
+import Data.TypeLevel.Num.Ops
diff --git a/src/Data/TypeLevel/Num/Aliases.hs b/src/Data/TypeLevel/Num/Aliases.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Num/Aliases.hs
@@ -0,0 +1,29 @@
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# LANGUAGE TemplateHaskell #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Num.Aliases
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (Template Haskell)
+--
+-- Type synonym aliases of type-level numerals and 
+-- their value-level reflecting functions. Generated for user convenience.
+-- 
+-- Aliases are generated using binary, octal, decimal and hexadecimal bases.
+-- Available aliases cover binaries up to b10000000000, octals up to
+-- o10000, decimals up to d5000 and hexadecimals up to h1000 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Num.Aliases where
+
+import Data.TypeLevel.Num.Reps
+import Data.TypeLevel.Num.Aliases.TH (genAliases)
+
+
+$(genAliases 1024 4096 5000 4096)
+
+
diff --git a/src/Data/TypeLevel/Num/Aliases/TH.hs b/src/Data/TypeLevel/Num/Aliases/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Num/Aliases/TH.hs
@@ -0,0 +1,130 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Num.Aliases
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (Template Haskell)
+--
+-- Internal template haskell functions to generate type-level numeral aliases
+-- 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Num.Aliases.TH (genAliases, dec2TypeLevel) where
+
+import Language.Haskell.TH
+
+import Data.TypeLevel.Num.Reps
+
+data Base = Bin | Oct | Dec | Hex
+
+base2Int :: Base -> Int
+base2Int Bin = 2
+base2Int Oct = 8
+base2Int Dec = 10
+base2Int Hex = 16
+
+-- This module needs to be separated from Data.TypeLevel.Num.Aliases due to
+-- a limitation in Template Haskell implementation: 
+-- "You can only run a function at compile time if it is imported from another 
+-- module." 
+
+genAliases :: Int -- how many binary aliases 
+           -> Int -- how many octal aliases
+           -> Int -- how many dec aliases
+           -> Int -- how many hex aliases
+           -> Q [Dec]
+genAliases nb no nd nh = genAliases' nb no nd nh (maximum [nb,no,nd,nh])
+
+genAliases' :: Int -- how many binary aliases 
+            -> Int -- how many octal aliases
+            -> Int -- how many dec aliases
+            -> Int -- how many hex aliases
+            -> Int -- maximum alias
+            -> Q [Dec]
+-- FIXME: genAliases' is ugly!
+genAliases' nb no nd nh curr 
+ | curr < 0 = return []
+ | otherwise = 
+    do rest <- genAliases' nb no nd nh (curr-1)
+       -- binaries
+       restb <- addAliasBase (curr > nb) ('b' : bStr) ('B' : bStr) rest
+       -- octals
+       resto <- addAliasBase (curr > no) ('o' : oStr) ('O' : oStr) restb
+       -- decimals, we don't aliases of the decimal digits
+       -- (they are alredy defined in the representation module)
+       restd <- if curr > nd then return resto             
+                else do val <- genValAlias ('d' : dStr) decRep
+                        typ <- genTypeAlias ('D' : dStr) decRep
+                        if (curr < 10) then return $ val : resto
+                         else return $ val : typ : resto
+       -- hexadicimals
+       addAliasBase (curr > no) ('h' : hStr) ('H' : hStr) restd
+ 
+ where  -- Add aliases of certain base to the rest of aliases
+        addAliasBase cond vStr tStr rest =
+          if cond then return rest
+          else  do val <- genValAlias vStr decRep
+                   typ <- genTypeAlias tStr decRep
+                   return $ val : typ : rest
+
+        decRep = dec2TypeLevel curr        
+
+        bStr = toBase Bin curr
+        oStr = toBase Oct curr
+        dStr = toBase Dec curr
+        hStr = toBase Hex curr
+
+-- | Generate the type-level decimal representation for a value-level 
+--   natural number. 
+-- NOTE: This function could be useful by itself avoiding to generate 
+-- aliases. However, type-splicing is not yet supported by template haskell.
+dec2TypeLevel :: Int -> Q Type
+dec2TypeLevel n
+ | n <  0 = error "natural number expected"
+ | n < 10 = let name = case n of
+                  0 -> ''D0; 1 -> ''D1; 2 -> ''D2; 3 -> ''D3; 4 -> ''D4
+                  5 -> ''D5; 6 -> ''D6; 7 -> ''D7; 8 -> ''D8; 9 -> ''D9
+            in conT name          
+ | otherwise = let (quotient, reminder) = n `quotRem` 10 
+                   remType  = dec2TypeLevel reminder
+                   quotType = dec2TypeLevel quotient
+               in (conT ''(:*)) `appT` quotType `appT` remType
+
+
+-- | Generate a decimal type synonym alias
+genTypeAlias :: String -> Q Type -> Q Dec
+genTypeAlias str t = tySynD name [] t
+ where name = mkName $ str
+
+-- | Generate a decimal value-level reflected alias
+genValAlias :: String -> Q Type -> Q Dec
+genValAlias str t = body
+ where name = mkName $ str
+       body = valD (varP name) 
+                   (normalB (sigE [| undefined |] t)) []
+
+
+-- | Print an integer in certain base
+toBase :: Base  -- base 
+       -> Int  -- Number to print
+       -> String
+toBase Dec n = show n
+toBase b n
+  | n < 0 = '-' : toBase b (- n)
+  | n < bi = [int2Char n]
+  | otherwise = (toBase b rest) ++ [int2Char currDigit]
+   where bi = base2Int b 
+         (rest, currDigit) = n `quotRem` bi
+
+-- | print the corresponding character of a digit
+int2Char ::  Int  -- Number to print
+          -> Char
+int2Char i 
+ | i' < 10 = toEnum (i'+ 48)
+ | otherwise = toEnum (i' + 55)
+ where i' = abs i
diff --git a/src/Data/TypeLevel/Num/Ops.hs b/src/Data/TypeLevel/Num/Ops.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Num/Ops.hs
@@ -0,0 +1,734 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, TypeOperators,
+             FlexibleInstances, FlexibleContexts, UndecidableInstances,
+             EmptyDataDecls, TypeFamilies #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Num.Ops
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (MPTC, non-standard instances)
+--
+-- Type-level numerical operations and its value-level reflection functions.
+-- 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Num.Ops 
+(
+  -- * Successor/Predecessor
+  Succ, succ,
+  Pred, pred,
+  -- * Addition/Subtraction
+  Add, (+),
+  Sub, (-),
+  -- * Multiplication/Division
+  Mul, (*),
+  Div, div,
+  Mod, mod,
+  --DivMod, divMod,
+  IsDivBy, isDivBy,
+  -- ** Special efficiency cases
+  Mul10, mul10,
+  Div10, div10,
+  DivMod10, divMod10,
+  -- * Exponientiation/Logarithm
+  ExpBase, (^),
+  -- Not implemented
+  -- LogBase, logBase,
+  -- LogBaseF, logBaseF,
+  -- IsPowOf, isPowOf,
+  -- ** Special efficiency cases
+  Exp10, exp10,
+  Log10, log10,
+  -- * Comparison assertions
+  -- ** General comparison assertion
+  Trich, trich,
+  -- *** Type-level values denoting comparison results
+  LT, EQ, GT,
+  OrderingEq, NatEq,
+  -- ** Abbreviated comparison assertions
+  (:>:), (:<:), (:>=:), (:<=:),
+  (>)  , (<)  , (>=)  , (<=), 
+  -- * Maximum/Minimum
+  Max, max,
+  Min, min,
+  -- * Greatest Common Divisor
+  GCD, gcd
+) 
+where
+
+import Data.TypeLevel.Num.Reps
+import Data.TypeLevel.Num.Sets
+import Data.TypeLevel.Bool
+
+import Prelude hiding 
+ (succ, pred, (+), (-), (*), div, mod, divMod, (^), logBase,
+  (==), (>), (<), (<), (>=), (<=), max, min, gcd, Bool)
+
+-------------------------
+-- Successor, Predecessor
+-------------------------
+
+-- | Successor type-level relation. @Succ x y@ establishes
+--  that @succ x = y@.
+-- Assoc notes: Cannot avoid malformed types
+type family Succ n
+type instance Succ D0 = D1
+type instance Succ D1 = D2
+type instance Succ D2 = D3
+type instance Succ D3 = D4
+type instance Succ D4 = D5
+type instance Succ D5 = D6
+type instance Succ D6 = D7
+type instance Succ D7 = D8
+type instance Succ D8 = D9
+type instance Succ D9 = (D1 :* D0)
+type instance Succ (x:*D0) = (x:*D1)
+type instance Succ (x:*D1) = (x:*D2)
+type instance Succ (x:*D2) = (x:*D3)
+type instance Succ (x:*D3) = (x:*D4)
+type instance Succ (x:*D4) = (x:*D5)
+type instance Succ (x:*D5) = (x:*D6)
+type instance Succ (x:*D6) = (x:*D7)
+type instance Succ (x:*D7) = (x:*D8)
+type instance Succ (x:*D8) = (x:*D9)
+type instance Succ (x:*D9) = (Succ x:*D0)
+
+
+
+
+-- | value-level reflection function for the 'Succ' type-level relation
+succ :: x -> Succ x
+succ = undefined
+
+type family Pred n
+type instance Pred D1 = D0
+type instance Pred D2 = D1
+type instance Pred D3 = D2
+type instance Pred D4 = D3
+type instance Pred D5 = D4
+type instance Pred D6 = D5
+type instance Pred D7 = D6
+type instance Pred D8 = D7
+type instance Pred D9 = D8
+type instance Pred (D1:*D0) = D9
+type instance Pred (D2:*D0) = (D1:*D9)
+type instance Pred (D3:*D0) = (D2:*D9)
+type instance Pred (D4:*D0) = (D3:*D9)
+type instance Pred (D5:*D0) = (D4:*D9)
+type instance Pred (D6:*D0) = (D5:*D9)
+type instance Pred (D7:*D0) = (D6:*D9)
+type instance Pred (D8:*D0) = (D7:*D9)
+type instance Pred (D9:*D0) = (D8:*D9)
+type instance Pred (xd:*xm:*D0) = Pred(xd:*xm):*D9
+type instance Pred (xd:*D1) = (xd:*D0)
+type instance Pred (xd:*D2) = (xd:*D1)
+type instance Pred (xd:*D3) = (xd:*D2)
+type instance Pred (xd:*D4) = (xd:*D3)
+type instance Pred (xd:*D5) = (xd:*D4)
+type instance Pred (xd:*D6) = (xd:*D5)
+type instance Pred (xd:*D7) = (xd:*D6)
+type instance Pred (xd:*D8) = (xd:*D7)
+type instance Pred (xd:*D9) = (xd:*D8)
+
+pred :: x -> Pred x
+pred = undefined
+
+--
+----------------------
+---- Add and Subtract
+----------------------
+--
+type family Div10 m 
+type instance Div10 D0 = D0
+type instance Div10 D1 = D0
+type instance Div10 D2 = D0
+type instance Div10 D3 = D0
+type instance Div10 D4 = D0
+type instance Div10 D5 = D0
+type instance Div10 D6 = D0
+type instance Div10 D7 = D0
+type instance Div10 D8 = D0
+type instance Div10 D9 = D0
+type instance Div10 (x:*D0) = x
+type instance Div10 (x:*D1) = x
+type instance Div10 (x:*D2) = x
+type instance Div10 (x:*D3) = x
+type instance Div10 (x:*D4) = x
+type instance Div10 (x:*D5) = x
+type instance Div10 (x:*D6) = x
+type instance Div10 (x:*D7) = x
+type instance Div10 (x:*D8) = x
+type instance Div10 (x:*D9) = x
+div10 :: x -> Div10 x
+div10 = undefined
+
+type family Mod10 n
+type instance Mod10 D0 = D0
+type instance Mod10 D1 = D1
+type instance Mod10 D2 = D2
+type instance Mod10 D3 = D3
+type instance Mod10 D4 = D4
+type instance Mod10 D5 = D5
+type instance Mod10 D6 = D6
+type instance Mod10 D7 = D7
+type instance Mod10 D8 = D8
+type instance Mod10 D9 = D9
+type instance Mod10 (xd:*xm) = xm
+mod10 :: x -> Mod10 x
+mod10 = undefined
+
+type family DivMod10 n
+type instance DivMod10 n = (Div10 n, Mod10 n)
+
+type family Add m n :: *
+type instance Add D0 x = x
+type instance Add D1 x = (Succ x)
+type instance Add D2 x = Add D1 (Succ x)
+type instance Add D3 x = Add D2 (Succ x)
+type instance Add D4 x = Add D3 (Succ x)
+type instance Add D5 x = Add D4 (Succ x)
+type instance Add D6 x = Add D5 (Succ x)
+type instance Add D7 x = Add D6 (Succ x)
+type instance Add D8 x = Add D7 (Succ x)
+type instance Add D9 x = Add D8 (Succ x)
+type instance Add (xd :* xm) y = Add xm ((Add xd (Div10 y)) :* (Mod10 y))
+
+
+-- | value-level reflection function for the 'Add' type-level relation 
+(+) :: x -> y -> Add x y
+(+) = undefined
+
+
+-- --| Subtraction type-level relation. @Sub x y z@ establishes
+-- -- that @x - y = z@ 
+type family Sub x y
+type instance Sub x D0 = x
+type instance Sub x D1 = (Pred x) 
+type instance Sub x D2 = Sub (Pred x) D1
+type instance Sub x D3 = Sub (Pred x) D2
+type instance Sub x D4 = Sub (Pred x) D3
+type instance Sub x D5 = Sub (Pred x) D4
+type instance Sub x D6 = Sub (Pred x) D5
+type instance Sub x D7 = Sub (Pred x) D6
+type instance Sub x D8 = Sub (Pred x) D7
+type instance Sub x D9 = Sub (Pred x) D8
+type instance Sub x (xd :* xm) = Sub (Pred x) (Pred (xd:*xm))
+
+-- | value-level reflection function for the 'Sub' type-level relation 
+(-) :: x -> y -> Sub x y
+(-) = undefined
+--
+--------------------------------
+---- Multiplication and Division
+--------------------------------
+--
+-------------------
+---- Multiplication
+-------------------
+--
+---- | Multiplication type-level relation. @Mul x y z@ establishes
+----  that @x * y = z@.
+type family Mul m n
+type instance Mul D0 y = D0
+type instance Mul D1 y = y
+type instance Mul D2 y = Add y y
+type instance Mul D3 y = Add y (Mul D2 y)
+type instance Mul D4 y = Add y (Mul D3 y)
+type instance Mul D5 y = Add y (Mul D4 y)
+type instance Mul D6 y = Add y (Mul D5 y)
+type instance Mul D7 y = Add y (Mul D6 y)
+type instance Mul D8 y = Add y (Mul D7 y)
+type instance Mul D9 y = Add y (Mul D8 y)
+-- Note that this is only valid if xd is positive.
+type instance Mul (xd :* xm) y = Add (Mul xm y) ((Mul xd y) :* D0)
+
+-- | value-level reflection function for the multiplication type-level relation 
+(*) :: x -> y -> Mul x y
+(*) = undefined
+
+
+--
+--
+-------------
+---- Division
+-------------
+
+-- | Division and Remainder type-level relation. @DivMod x y q r@ establishes
+--  that @x/y = q + r/y@
+
+-- division + modulo
+-- x/y | y > x = (0,x)
+-- x/y | y <= x = ( 1 + (x-y / y), mod (x - y))
+
+-- This doesn't work
+--type instance Div x y = Cond (y :>: x) D0 (Succ (Div (Sub x y) y))
+--type instance Mod x y = Cond (y :>: x) x  (Mod (Sub x y) y)
+
+type family Div' x y x_gt_y
+type instance Div' x y False = D0
+type instance Div' x y True = Succ (Div' (Sub x y) y ((Sub x y) :>=: y)) 
+type family Div x y
+type instance Div x y = Div' x y (Trich x y)
+
+type family Mod' x y x_gt_y
+type instance Mod' x y False = x
+type instance Mod' x y True = Mod' (Sub x y) y ((Sub x y) :>=: y)
+type family Mod x y
+type instance Mod x y = Mod' x y (x :>=: y)
+
+
+-- | value-level reflection function for the 'DivMod' type-level relation
+divMod :: x -> y -> (Div x y, Mod x y)
+divMod _ _ = (undefined)
+
+-- | value-level reflection function for the 'Div' type-level relation 
+div :: x -> y -> Div x y
+div = undefined
+
+-- | value-level reflection function for the 'Mod' type-level relation 
+mod :: x -> y -> Mod x y
+mod = undefined
+
+
+------------------------------------------
+---- Multiplication/Division special cases
+------------------------------------------
+
+-- | Multiplication by 10 type-level relation (based on 'DivMod10').
+--   @Mul10 x y@ establishes that @10 * x = y@.
+type family Mul10 n
+type instance Mul10 x = (x :* D0)
+
+-- | value-level reflection function for 'Mul10' 
+mul10 :: x -> Mul10 x
+mul10 = undefined
+
+
+---- | value-level reflection function for DivMod10 
+divMod10 :: x -> (Div10 x, Mod10 x)
+divMod10 _ = (undefined, undefined)
+
+--
+------------------------------
+---- Is-Divisible-By assertion
+------------------------------
+
+-- | Is-divisible-by type-level assertion. e.g @IsDivBy d x@ establishes that
+--   @x@ is divisible by @d@.
+
+-- here we use a class for demonstration purposes
+class (Pos d, Nat x) => IsDivBy d x
+instance (Pos d, Nat x, Mod x d ~ D0) => IsDivBy d x
+
+-- | value-level reflection function for IsDivBy
+isDivBy :: IsDivBy d x => d -> x -> ()
+isDivBy _ _ = ()
+
+-----------------------------
+---- Exponentiation/Logarithm
+-----------------------------
+--
+---- | Exponentation type-level relation. @ExpBase b e r@ establishes
+----  that @b^e = r@
+type family ExpBase b e
+type instance ExpBase b D0 = D1
+type instance ExpBase b D1 = b
+type instance ExpBase b D2 = (Mul b b)
+type instance ExpBase b D3 = (Mul b (ExpBase b D2))
+type instance ExpBase b D4 = (Mul b (ExpBase b D3))
+type instance ExpBase b D5 = (Mul b (ExpBase b D4))
+type instance ExpBase b D6 = (Mul b (ExpBase b D5))
+type instance ExpBase b D7 = (Mul b (ExpBase b D6))
+type instance ExpBase b D8 = (Mul b (ExpBase b D7))
+type instance ExpBase b D9 = (Mul b (ExpBase b D8))
+type instance ExpBase b (ei :* el) = Mul b (ExpBase b (Pred (ei:* el)))
+
+-- | value-level reflection function for the ExpBase type-level relation
+(^) :: b -> e -> ExpBase b e
+(^) = undefined
+
+---------------- LEFT OUT FOR NOW ---------------------------------
+
+-- Logarithm type-level relation. @LogBase b x e@ establishes that 
+-- @log_base_b x = e@
+--  Note it is not relational (i.e. cannot be used to express exponentiation)
+--class (Pos b, b :>=: D2, Pos x, Nat e) =>  LogBase b x e  | b x -> e 
+--instance  LogBaseF b x e f => LogBase b x e
+--
+--
+---- | value-level reflection function for LogBase
+--logBase :: LogBaseF b x e f => b -> x -> e
+--logBase = undefined 
+--
+--
+---- | Version of LogBase which also outputs if the logarithm
+---- calculated was exact.
+---- f indicates if the resulting logarithm has no fractional part (i.e.
+---- tells if the result provided is exact)
+--class (Pos b, b :>=: D2, Pos x, Nat e, Bool f) 
+--     =>  LogBaseF b x e f | b x -> e f
+--instance (Trich x b cmp, LogBaseF' b x e f cmp) => LogBaseF b x e f
+--
+--
+--class (Pos b, b :>=: D2, Pos x, Nat e, Bool f)
+--     => LogBaseF' b x e f cmp | b x cmp -> e f 
+--instance (Pos b, b :>=: D2, Pos x) => LogBaseF' b x D0 False LT
+--instance (Pos b, b :>=: D2) => LogBaseF' b b D1 True  EQ
+--instance (Pos b, b :>=: D2, Pos x, DivMod x b q r, IsZero r rz, And rz f' f, 
+--          Pred e e', LogBaseF b q e' f') => LogBaseF' b x e f GT
+--
+---- | value-level reflection function for LogBaseF
+--logBaseF :: LogBaseF b x e f => b -> x -> (e,f)
+--logBaseF _ _ = (undefined, undefined) 
+--
+
+-- We could reuse LogBaseF for IsPowOf but it would be inneficient.
+-- LogBaseF continues calculating the logarithm even if after knowing its
+-- not exact. Thus, it is desirable to include a custom definition of
+-- IsPowOf which can "abort" the calculation forcing the Divisions to be
+-- exact
+
+
+-- | Assert that a number (@x@) can be expressed as the power of another one
+--   (@b@) (i.e. the fractional part of @log_base_b x = 0@, or, 
+--   in a different way, @exists y . b\^y = x@). 
+--
+--class (Pos b, b :>=: D2, Pos x) =>  IsPowOf b x
+--instance (Trich x b cmp, IsPowOf' b x cmp) => IsPowOf b x
+--class (Pos b, b :>=: D2, Pos x) => IsPowOf' b x cmp
+---- If lower (x < b), then the logarithm is not exact  
+---- instance (Pos b, b :>=: D2, Pos x) => IsPowOf' b x LT
+--instance (Pos b, b :>=: D2) => IsPowOf' b b EQ
+--instance (Pos b, b :>=: D2, Pos x, DivMod x b q D0, IsPowOf b q) 
+--         => IsPowOf' b x  GT
+---- | 
+--isPowOf :: IsPowOf b x => b -> x -> ()
+--isPowOf = undefined
+
+-------------------------------------
+---- Base-10 Exponentiation/Logarithm
+-------------------------------------
+
+type family Exp10 x
+type instance Exp10 D0 = D1
+type instance Exp10 D1 = (D1 :* D0)
+type instance Exp10 D2 = (D1 :* D0 :* D0)
+type instance Exp10 D3 = (D1 :* D0 :* D0 :* D0)
+type instance Exp10 D4 = (D1 :* D0 :* D0 :* D0 :* D0)
+type instance Exp10 D5 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0)
+type instance Exp10 D6 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
+type instance Exp10 D7 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
+type instance Exp10 D8 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
+type instance Exp10 D9 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
+type instance Exp10 (xi :* xl) = (Exp10 (Pred (xi:*xl)) :* D0)
+
+-- | value-level reflection function for Exp10
+exp10 :: x -> Exp10 x
+exp10 = undefined
+
+-- | Base-10 logarithm type-level relation
+--   Note it is not relational (cannot be used to express Exponentation to 10)
+--   However, it works with any positive numeral (not just powers of 10)
+type family Log10 x 
+type instance Log10 D1 = D0
+type instance Log10 D2 = D0
+type instance Log10 D3 = D0
+type instance Log10 D4 = D0
+type instance Log10 D5 = D0
+type instance Log10 D6 = D0
+type instance Log10 D7 = D0
+type instance Log10 D8 = D0
+type instance Log10 D9 = D0
+type instance Log10 (xi :* xl) = Pred (Log10 xi)
+
+-- | value-level reflection function for 'Log10'
+log10 :: x -> Log10 x
+log10 = undefined
+--
+--{- Log10': Alternative implementation of Log10
+--
+--Relational, but it only works for results of Exp10 (i.e. powers of 10).
+--
+--class (Pos x, Nat y) => Log10' x y | x -> y, y -> x
+--instance Exp10 x y => Log10' y x
+---}
+--
+--
+---------------
+---- Comparison
+---------------
+
+-- type-level values denoting comparison results
+-- | Lower than 
+data LT
+-- | Equal
+data EQ
+-- | Greater than
+data GT
+
+type family OrderingEq o1 o2
+type instance OrderingEq LT LT = True
+type instance OrderingEq LT EQ = False
+type instance OrderingEq LT GT = False
+type instance OrderingEq EQ EQ = True
+type instance OrderingEq EQ LT = False
+type instance OrderingEq EQ GT = False
+type instance OrderingEq GT GT = True
+type instance OrderingEq GT LT = False
+type instance OrderingEq GT EQ = False
+
+-- | Trichotomy type-level relation. 'Trich x y r' establishes
+--   the relation (@r@) between @x@ and @y@. The obtained relation (@r@)
+--   Can be 'LT' (if @x@ is lower than @y@), 'EQ' (if @x@ equals @y@) or
+--   'GT' (if @x@ is greater than @y@)
+type family Trich x y
+
+-- | value-level reflection function for the comparison type-level assertion 
+trich :: x -> y -> Trich x y
+trich = undefined
+
+-- by structural induction on the first, and then the second argument
+-- D0
+type instance Trich D0 D0 = EQ
+type instance Trich D0 D1 = LT
+type instance Trich D0 D2 = LT
+type instance Trich D0 D3 = LT
+type instance Trich D0 D4 = LT
+type instance Trich D0 D5 = LT
+type instance Trich D0 D6 = LT
+type instance Trich D0 D7 = LT
+type instance Trich D0 D8 = LT
+type instance Trich D0 D9 = LT
+type instance Trich D0 (yi :* yl) = LT
+type instance Trich (yi :* yl) D0 = GT
+-- D1
+type instance Trich D1 D0 = GT
+type instance Trich D1 D1 = EQ
+type instance Trich D1 D2 = LT
+type instance Trich D1 D3 = LT 
+type instance Trich D1 D4 = LT
+type instance Trich D1 D5 = LT 
+type instance Trich D1 D6 = LT
+type instance Trich D1 D7 = LT 
+type instance Trich D1 D8 = LT
+type instance Trich D1 D9 = LT
+type instance Trich D1 (yi :* yl) = LT
+type instance Trich (yi :* yl) D1 = GT
+-- D2
+type instance Trich D2 D0 = GT
+type instance Trich D2 D1 = GT
+type instance Trich D2 D2 = EQ
+type instance Trich D2 D3 = LT
+type instance Trich D2 D4 = LT
+type instance Trich D2 D5 = LT
+type instance Trich D2 D6 = LT
+type instance Trich D2 D7 = LT
+type instance Trich D2 D8 = LT
+type instance Trich D2 D9 = LT
+type instance Trich D2 (yi :* yl) = LT
+type instance Trich (yi :* yl) D2 = GT
+-- D3
+type instance Trich D3 D0 = GT
+type instance Trich D3 D1 = GT
+type instance Trich D3 D2 = GT
+type instance Trich D3 D3 = EQ
+type instance Trich D3 D4 = LT
+type instance Trich D3 D5 = LT
+type instance Trich D3 D6 = LT
+type instance Trich D3 D7 = LT
+type instance Trich D3 D8 = LT
+type instance Trich D3 D9 = LT
+type instance Trich D3 (yi :* yl) = LT
+type instance Trich (yi :* yl) D3 = GT
+-- D4
+type instance Trich D4 D0 = GT
+type instance Trich D4 D1 = GT
+type instance Trich D4 D2 = GT
+type instance Trich D4 D3 = GT
+type instance Trich D4 D4 = EQ
+type instance Trich D4 D5 = LT
+type instance Trich D4 D6 = LT
+type instance Trich D4 D7 = LT
+type instance Trich D4 D8 = LT
+type instance Trich D4 D9 = LT
+type instance Trich D4 (yi :* yl) = LT
+type instance Trich (yi :* yl) D4 = GT
+-- D5
+type instance Trich D5 D0 = GT
+type instance Trich D5 D1 = GT
+type instance Trich D5 D2 = GT
+type instance Trich D5 D3 = GT
+type instance Trich D5 D4 = GT
+type instance Trich D5 D5 = EQ
+type instance Trich D5 D6 = LT
+type instance Trich D5 D7 = LT
+type instance Trich D5 D8 = LT
+type instance Trich D5 D9 = LT
+type instance Trich D5 (yi :* yl) = LT
+type instance Trich (yi :* yl) D5 = GT
+-- D6
+type instance Trich D6 D0 = GT
+type instance Trich D6 D1 = GT
+type instance Trich D6 D2 = GT
+type instance Trich D6 D3 = GT
+type instance Trich D6 D4 = GT
+type instance Trich D6 D5 = GT
+type instance Trich D6 D6 = EQ
+type instance Trich D6 D7 = LT
+type instance Trich D6 D8 = LT
+type instance Trich D6 D9 = LT
+type instance Trich D6 (yi :* yl) = LT
+type instance Trich (yi :* yl) D6 = GT
+-- D7
+type instance Trich D7 D0 = GT
+type instance Trich D7 D1 = GT
+type instance Trich D7 D2 = GT
+type instance Trich D7 D3 = GT
+type instance Trich D7 D4 = GT
+type instance Trich D7 D5 = GT
+type instance Trich D7 D6 = GT
+type instance Trich D7 D7 = EQ
+type instance Trich D7 D8 = LT
+type instance Trich D7 D9 = LT
+type instance Trich D7 (yi :* yl) = LT
+type instance Trich (yi :* yl) D7 = GT
+-- D8
+type instance Trich D8 D0 = GT
+type instance Trich D8 D1 = GT
+type instance Trich D8 D2 = GT
+type instance Trich D8 D3 = GT
+type instance Trich D8 D4 = GT
+type instance Trich D8 D5 = GT
+type instance Trich D8 D6 = GT
+type instance Trich D8 D7 = GT
+type instance Trich D8 D8 = EQ
+type instance Trich D8 D9 = LT
+type instance Trich D8 (yi :* yl) = LT
+type instance Trich (yi :* yl) D8 = GT
+-- D9
+type instance Trich D9 D0 = GT
+type instance Trich D9 D1 = GT
+type instance Trich D9 D2 = GT
+type instance Trich D9 D3 = GT
+type instance Trich D9 D4 = GT
+type instance Trich D9 D5 = GT
+type instance Trich D9 D6 = GT
+type instance Trich D9 D7 = GT
+type instance Trich D9 D8 = GT
+type instance Trich D9 D9 = EQ
+type instance Trich D9 (yi :* yl) = LT
+type instance Trich (yi :* yl) D9 = GT
+
+
+-- multidigit comparison
+type instance Trich (xd :* xm) (yd :* ym) = CS (Trich xd yd) (Trich xm ym)
+
+-- strengthen the comparison relation
+type family CS c1 c2
+type instance CS EQ r = r
+type instance CS GT r = GT
+type instance CS LT r = LT
+
+-- Abbreviated comparison assertions
+
+-- | Equality abbreviated type-level assertion
+type family NatEq x y
+type instance NatEq x y = OrderingEq (Trich x y) EQ
+
+-- | Greater-than abbreviated type-level assertion
+type family x :>: y
+type instance x :>: y = OrderingEq (Trich x y) GT
+
+-- | value-level reflection function for >
+(>) :: x -> y -> x :>: y
+(>) = undefined
+
+-- | Lower-than abbreviated type-level assertion
+type family x :<: y
+type instance x :<: y = OrderingEq (Trich x y) LT
+
+-- | value-level reflection function for >
+(<) :: x -> y -> x :<: y
+(<) = undefined
+
+-- | Greater-than or equal abbreviated type-level assertion
+type family x :>=: y
+type instance x :>=: y = (Succ x) :>: y
+
+-- | value-level reflection function for >=
+(>=) :: x -> y -> x :>=: y
+(>=) = undefined
+
+-- | Less-than or equal abbreviated type-level assertion
+type family x :<=: y
+type instance x :<=: y = x :<: (Succ y)
+
+-- | value-level reflection function for >=
+(<=) :: x -> y -> x :<=: y
+(<=) = undefined
+
+
+--------------------
+---- Maximum/Minimum
+--------------------
+type family Max x y
+type instance Max x y = Cond (x :>: y) x y
+type family Min x y
+type instance Min x y = Cond (x :<=: y) x y
+
+-- | value-level reflection function for the maximum type-level relation
+max :: x -> y -> Max x y
+max = undefined
+
+-- | value-level reflection function for the minimum type-level relation
+min :: x -> y -> Min x y
+min = undefined
+
+---------
+---- GCD
+---------
+
+-- | Greatest Common Divisor type-level relation
+type family GCD x y
+type instance GCD x y = GCD' x y (IsZero y) (Trich x y)
+
+---- Euclidean algorithm 
+--class (Nat x, Nat y, Nat gcd) => GCD' x y yz cmp gcd | x y yz cmp -> gcd
+type family GCD' x y ys cmp
+type instance GCD' x D0 True cmp = D0
+type instance GCD' x y False LT = GCD y x
+type instance GCD' x y False EQ = x
+type instance GCD' x y False GT = GCD (Sub x y) y
+
+-- | value-level reflection function for the GCD type-level relation
+gcd :: x -> y -> GCD x y
+gcd = undefined
+
+-----------------------
+---- Internal functions
+-----------------------
+--
+-- classify a natural as positive or zero
+type family IsZero n
+type instance IsZero D0 = True
+type instance IsZero D1 = False
+type instance IsZero D2 = False
+type instance IsZero D3 = False
+type instance IsZero D4 = False
+type instance IsZero D5 = False
+type instance IsZero D6 = False
+type instance IsZero D7 = False
+type instance IsZero D8 = False
+type instance IsZero D9 = False
+-- debatable
+type instance IsZero (xd:*xm) = And (IsZero xd) (IsZero xm)
+
+-- 
+-- The cond TF
+type family Cond b x y
+type instance Cond True  x y = x
+type instance Cond False x y = y
+
diff --git a/src/Data/TypeLevel/Num/Reps.hs b/src/Data/TypeLevel/Num/Reps.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Num/Reps.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE EmptyDataDecls, TypeOperators, DeriveDataTypeable,
+             ScopedTypeVariables, TemplateHaskell #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Num.Reps
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (TypeOperators)
+--
+-- Type-level numerical representations. Currently, only decimals are 
+-- supported.
+-- 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Num.Reps (
+ -- * Decimal representation
+ --   $decdescription
+ --  ** Digits
+ D0, D1, D2, D3, D4, D5, D6, D7, D8, D9,
+ --  ** Connective
+ (:*)(..),
+ ) where
+
+import Data.List
+import Data.Typeable (Typeable)
+import Language.Haskell.TH.Syntax (Lift(..)) 
+
+-------------------------
+-- Decimal Representation
+-------------------------
+
+-- $decdescription 
+-- Decimals are represented using a different type (@Dx@) for each digit and a 
+-- binary infix connective (@:*@) to enable forming arbitrary precision 
+-- multidigit numbers. For example @D0@ represents number 0, @D4 :* D2@ 
+-- represents number 42, @D1 :* D0 :* D0@ represents 100, etc ... Obviously, 
+-- negative numbers cannot be represented.
+
+-- | Decimal digit zero
+data D0 deriving Typeable
+instance Show D0 where show _ = "0"
+instance Lift D0 where lift _ = [| undefined :: D0 |]
+-- | Decimal digit one
+data D1 deriving Typeable
+instance Show D1 where show _ = "1"
+instance Lift D1 where lift _ = [| undefined :: D1 |]
+-- | Decimal digit two
+data D2 deriving Typeable
+instance Show D2 where show _ = "2"
+instance Lift D2 where lift _ = [| undefined :: D2 |]
+-- | Decimal digit three 
+data D3 deriving Typeable
+instance Show D3 where show _ = "3"
+instance Lift D3 where lift _ = [| undefined :: D3 |]
+-- | Decimal digit four 
+data D4 deriving Typeable
+instance Show D4 where show _ = "4"
+instance Lift D4 where lift _ = [| undefined :: D4 |]
+-- | Decimal digit five
+data D5 deriving Typeable
+instance Show D5 where show _ = "5"
+instance Lift D5 where lift _ = [| undefined :: D5 |]
+-- | Decimal digit six
+data D6 deriving Typeable
+instance Lift D6 where lift _ = [| undefined :: D6 |]
+instance Show D6 where show _ = "6"
+-- | Decimal digit seven
+data D7 deriving Typeable
+instance Show D7 where show _ = "7"
+instance Lift D7 where lift _ = [| undefined :: D7 |]
+-- | Decimal digit eight
+data D8 deriving Typeable
+instance Show D8 where show _ = "8"
+instance Lift D8 where lift _ = [| undefined :: D8 |]
+-- | Decimal digit nine
+data D9 deriving Typeable
+instance Show D9 where show _ = "9"
+instance Lift D9 where lift _ = [| undefined :: D9 |]
+
+-- | Connective to glue digits together.
+--   For example, @D1 :* D0 :* D0@ represents the decimal number 100
+data a :* b = a :* b deriving Typeable
+
+instance (Show a, Show b) => Show (a :* b) where
+  show _ = (show (undefined :: a)) ++ (show (undefined :: b))
+
+instance (Lift a, Lift b) => Lift (a :* b) where
+  lift _ = [| $(lift (undefined ::a)) :* $(lift (undefined :: b) ) |]
diff --git a/src/Data/TypeLevel/Num/Sets.hs b/src/Data/TypeLevel/Num/Sets.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Num/Sets.hs
@@ -0,0 +1,172 @@
+{-# LANGUAGE TypeOperators, FlexibleInstances, FlexibleContexts,
+             UndecidableInstances, ScopedTypeVariables,
+             Rank2Types #-}
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-name-shadowing #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Num.Sets
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (non-standard instances)
+--
+-- Type-level numerical sets. Currently there is only support for Naturals and 
+-- Positives.
+-- 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Num.Sets (Pos, Nat, toNum, toInt, reifyIntegral) where 
+
+import Data.TypeLevel.Num.Reps
+
+-----------
+-- Naturals
+-----------
+
+
+-- The well-formedness condition, the kind predicate.
+-- These classes are internal, denoted by the ending "I", which is removed in 
+-- the exported proxies (read below)
+
+-- | Naturals (Positives and zero), internal version
+class NatI n where 
+ -- | Reflecting function
+ toNum :: Num a => n -> a
+
+
+-- | Less generic reflecting function (Int)
+toInt :: Nat n => n -> Int
+toInt =  toNum
+
+
+
+-- | Positives (Naturals without zero), internal version
+class NatI n => PosI n
+
+-- To prevent the user from adding new instances to NatI and especially
+-- to PosI (e.g., to prevent the user from adding the instance |Pos D0|)
+-- we do NOT export NatI and PosI. Rather, we export the following proxies.
+-- The proxies entail PosI and NatI and so can be used to add PosI and NatI
+-- constraints in the signatures. However, all the constraints below
+-- are expressed in terms of NatI and PosI rather than proxies. Thus,
+-- even if the user adds new instances to proxies, it would not matter.
+-- Besides, because the following proxy instances are most general,
+-- one may not add further instances without overlapping instance extension.
+
+-- | Naturals (Positives and zero)
+class    (NatI n) => Nat n
+instance (NatI n) => Nat n
+
+-- | Positives (Naturals without zero)
+class    PosI n => Pos n
+instance PosI n => Pos n
+
+--------------------
+-- Natural Instances
+--------------------
+
+-- Note: TH would be helpful to sistematically define instances 
+--       (our type level operations)
+--       However, type-splicing is not yet implemented in GHC :S
+
+-- monodigit naturals
+instance NatI D0 where toNum _ = fromInteger 0
+instance NatI D1 where toNum _ = fromInteger 1
+instance NatI D2 where toNum _ = fromInteger 2
+instance NatI D3 where toNum _ = fromInteger 3
+instance NatI D4 where toNum _ = fromInteger 4
+instance NatI D5 where toNum _ = fromInteger 5
+instance NatI D6 where toNum _ = fromInteger 6
+instance NatI D7 where toNum _ = fromInteger 7
+instance NatI D8 where toNum _ = fromInteger 8
+instance NatI D9 where toNum _ = fromInteger 9
+
+-- multidigit naturals
+-- Note: The PosI constraint guarantees that all valid representations are 
+-- normalized (i.e. D0 :* D1 will lead to a compiler error)
+-- Note as well that ill-formed representations such as
+-- (D1 :* D2) :* (D3 :* D4) are not recognized as instances of
+-- naturals nor positives.
+instance PosI x => NatI (x :* D0) where toNum n = subLastDec n
+instance PosI x => NatI (x :* D1) where toNum n = subLastDec n + fromInteger 1
+instance PosI x => NatI (x :* D2) where toNum n = subLastDec n + fromInteger 2
+instance PosI x => NatI (x :* D3) where toNum n = subLastDec n + fromInteger 3
+instance PosI x => NatI (x :* D4) where toNum n = subLastDec n + fromInteger 4
+instance PosI x => NatI (x :* D5) where toNum n = subLastDec n + fromInteger 5
+instance PosI x => NatI (x :* D6) where toNum n = subLastDec n + fromInteger 6
+instance PosI x => NatI (x :* D7) where toNum n = subLastDec n + fromInteger 7
+instance PosI x => NatI (x :* D8) where toNum n = subLastDec n + fromInteger 8
+instance PosI x => NatI (x :* D9) where toNum n = subLastDec n + fromInteger 9
+
+-- monodigit positives
+instance PosI D1
+instance PosI D2
+instance PosI D3
+instance PosI D4
+instance PosI D5
+instance PosI D6
+instance PosI D7
+instance PosI D8
+instance PosI D9
+
+-- multidigit positives
+-- Note: The PosI constraint guarantees that all valid representations are 
+-- normalized (i.e. D0 :* D1 will lead to a compiler error)
+instance PosI x => PosI (x :* D0)
+instance PosI x => PosI (x :* D1)
+instance PosI x => PosI (x :* D2)
+instance PosI x => PosI (x :* D3)
+instance PosI x => PosI (x :* D4)
+instance PosI x => PosI (x :* D5)
+instance PosI x => PosI (x :* D6)
+instance PosI x => PosI (x :* D7)
+instance PosI x => PosI (x :* D8)
+instance PosI x => PosI (x :* D9)
+
+
+-- | Reification function. In CPS style (best possible solution)
+reifyIntegral :: Integral i => i -> (forall n . Nat n => n -> r) -> r
+reifyIntegral i f 
+ | i < 0     = error "reifyIntegral: integral < 0"
+ | i == 0    = f (undefined :: D0)
+ | otherwise = reifyIntegralp i f 
+       -- reifyIntegral for positives
+ where reifyIntegralp :: Integral i => i -> (forall n . Pos n => n -> r) -> r
+       reifyIntegralp i f 
+         | i < 10 = case i of
+                     1 -> f (undefined :: D1)
+                     2 -> f (undefined :: D2); 3 -> f (undefined :: D3)
+                     4 -> f (undefined :: D4); 5 -> f (undefined :: D5)
+                     6 -> f (undefined :: D6); 7 -> f (undefined :: D7)
+                     8 -> f (undefined :: D8); 9 -> f (undefined :: D9)
+         | otherwise =  
+            case m of
+              0 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D0)) 
+              1 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D1))
+              2 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D2))
+              3 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D3))
+              4 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D4))
+              5 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D5))
+              6 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D6))
+              7 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D7))
+              8 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D8))
+              9 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D9))      
+           where (d,m) = divMod i 10
+
+
+---------------------
+-- Internal functions
+---------------------
+
+-- substract the last digit of a decimal type-level numeral and obtain 
+-- the result's reflected value 
+{-# INLINE subLastDec #-}
+subLastDec :: (Num a, NatI (x :* d), NatI x) => x :* d -> a
+subLastDec = (10*).toNum.div10Dec
+
+-- Divide a decimal type-level numeral by 10 
+{-# INLINE div10Dec #-} 
+div10Dec :: NatI (x :* d) => x :* d -> x
+div10Dec _ = undefined
diff --git a/type-level-tf.cabal b/type-level-tf.cabal
new file mode 100644
--- /dev/null
+++ b/type-level-tf.cabal
@@ -0,0 +1,53 @@
+name:           type-level-tf
+version:        0.2.1
+license:        BSD3
+license-file:   LICENSE
+copyright:      
+ Copyright (c) 2010 Corey O'Connor
+ Copyright (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+                    and KTH's SAM group
+               2008 Benedikt Huber (Rewrite using type families)
+author:         Corey O'Connor, Alfonso Acosta
+homepage:       https://github.com/coreyoconnor/type-level-tf
+maintainer:     coreyoconnor@gmail.com
+stability:      alpha
+synopsis:       Type-level programming library (type families)
+description:
+
+ This library permits performing computations on the type-level. Type-level 
+ functions are implemented using functional dependencies of multi
+ parameter type classes. 
+
+ To date, Booleans and Numerals (Naturals and Positives) are
+ supported. With regard to Numerals, there is support for common
+ arithmetic operations (addition, substraction, multiplication,
+ division, exponientation, logarithm, maximum, comparison, GCD) 
+ over natural numbers (using a decimal representation to make 
+ compile-time errors friendlier).
+
+ Although making use of type-level computations might seem devious and
+ obfuscated at first sight, it is indeed useful in practice to implement 
+ lightweight dependent types such us number-parameterized types (e.g. an array 
+ type parameterized by the array's size or a modular group type Zn 
+ parameterized by the modulus).
+
+category:       Data
+tested-with:    GHC==6.9.0, GHC==6.12.0, GHC==7.2.1
+cabal-version:  >= 1.6
+build-type:     Simple
+
+source-repository head
+    type:       git
+    location:   git://github.com/coreyoconnor/type-level-tf.git
+
+Library
+  build-depends:   base == 4.*, template-haskell > 2.0, syb
+  hs-source-dirs:  src
+  exposed-modules: Data.TypeLevel,
+                   Data.TypeLevel.Bool,
+                   Data.TypeLevel.Num,
+                   Data.TypeLevel.Num.Reps,
+                   Data.TypeLevel.Num.Aliases,
+                   Data.TypeLevel.Num.Sets,
+                   Data.TypeLevel.Num.Ops,
+                   Data.TypeLevel.Num.Aliases.TH