diff --git a/Data/Numeric/Witness/Peano.hs b/Data/Numeric/Witness/Peano.hs
new file mode 100644
--- /dev/null
+++ b/Data/Numeric/Witness/Peano.hs
@@ -0,0 +1,78 @@
+{- |
+Module      :  Data.Numeric.Witness.Peano
+Description :  Peano-style natural numbers paired with type-level naturals.
+Copyright   :  Copyright (c) 2014 Kenneth Foner
+
+Maintainer  :  kenneth.foner@gmail.com
+Stability   :  experimental
+Portability :  non-portable
+
+This module defines GADT type witnesses for Peano-style natural numbers.
+-}
+
+{-# LANGUAGE ConstraintKinds     #-}
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving  #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE TypeOperators       #-}
+
+module Data.Numeric.Witness.Peano where
+
+data Zero
+data Succ n
+
+-- | Natural numbers paired with type-level natural numbers. These terms act as witnesses of a particular natural.
+data Natural n where
+   Zero :: Natural Zero
+   Succ :: Natural n -> Natural (Succ n)
+deriving instance Show (Natural n)
+
+-- | Given a context expecting a particular natural, we can manufacture it from the aether.
+class ReifyNatural n                               where reifyNatural :: Natural n
+instance ReifyNatural Zero                         where reifyNatural = Zero
+instance (ReifyNatural n) => ReifyNatural (Succ n) where reifyNatural = Succ (reifyNatural :: Natural n)
+
+-- | Type level less-than-or-equal test.
+type family LessThanOrEqual a b where
+   LessThanOrEqual Zero     Zero     = True
+   LessThanOrEqual Zero     (Succ m) = True
+   LessThanOrEqual (Succ n) (Succ m) = LessThanOrEqual n m
+   LessThanOrEqual x y               = False
+
+-- | This constraint is a more succinct way of requiring that @a@ be less than or equal to @b@.
+type a <= b = (LessThanOrEqual a b ~ True)
+
+-- | Type level less-than test.
+type family LessThan a b where
+   LessThan Zero     (Succ m) = True
+   LessThan (Succ n) (Succ m) = LessThan n m
+   LessThan x        y        = False
+
+-- | This constraint is a more succinct way of requiring that @a@ be less than @b@.
+type a < b = (LessThan a b ~ True)
+
+-- | Type level addition.
+type family x + y where
+   x + Zero     = x
+   x + (Succ y) = Succ (x + y)
+
+-- | Type level subtraction.
+type family x - y where
+   x        - Zero     = x
+   (Succ x) - (Succ y) = x - y
+
+-- | Addition of naturals at the term and type levels simultaneously.
+plus :: Natural a -> Natural b -> Natural (a + b)
+plus x Zero     = x
+plus x (Succ y) = Succ (plus x y)
+
+-- | Subtraction of naturals at the term and type level simultaneously. Note that it is statically prohibited to subtract
+--   a number larger than the number from which it is being subtracted.
+minus :: (b <= a) => Natural a -> Natural b -> Natural (a - b)
+minus x        Zero     = x
+minus (Succ x) (Succ y) = minus x y
+minus _ _ = error "minus: the impossible occurred" -- GHC can't prove this is unreachable
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014, Kenneth Foner
+
+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 Kenneth Foner nor the names of other
+      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 AND CONTRIBUTORS
+"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
+OWNER OR CONTRIBUTORS 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/PeanoWitnesses.cabal b/PeanoWitnesses.cabal
new file mode 100644
--- /dev/null
+++ b/PeanoWitnesses.cabal
@@ -0,0 +1,24 @@
+-- Initial PeanoWitnesses.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                PeanoWitnesses
+version:             0.1.0.0
+synopsis:            GADT type witnesses for Peano-style natural numbers.
+description:         Witnesses for Peano naturals are unary natural numbers paired with a natural number type index. These terms act as witnesses of a particular natural; we can recover the type information by examining the terms.
+license:             BSD3
+license-file:        LICENSE
+author:              Kenneth Foner
+maintainer:          kenny.foner@gmail.com
+-- copyright:           
+category:            Data
+build-type:          Simple
+-- extra-source-files:  
+cabal-version:       >=1.10
+
+library
+  exposed-modules:     Data.Numeric.Witness.Peano
+  -- other-modules:       
+  other-extensions:    ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances, GADTs, ScopedTypeVariables, StandaloneDeriving, TypeFamilies, TypeOperators
+  build-depends:       base >=4.7 && <4.8
+  -- hs-source-dirs:      
+  default-language:    Haskell2010
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain