diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for natural-arithmetic
+
+## 0.1.0.0 -- 2019-09-04
+
+* Initial release.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2019, Andrew Martin
+
+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 Andrew Martin 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/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/natural-arithmetic.cabal b/natural-arithmetic.cabal
new file mode 100644
--- /dev/null
+++ b/natural-arithmetic.cabal
@@ -0,0 +1,80 @@
+cabal-version: 2.2
+name: natural-arithmetic
+version: 0.1.0.0
+synopsis: Arithmetic of natural numbers
+description:
+  A search for terms like `arithmetic` and `natural` on hackage reveals
+  no shortage of libraries for handling the arithmetic of natural
+  numbers. How is this library any different some of the others? It has
+  a particular purpose: providing a foundation on top on which other
+  libraries may define types indexed by sizes. This uses GHC's
+  non-inductively-defined `GHC.TypeNats.Nat`. As a rule, this does not
+  use `unsafeCoerce` internally anywhere.
+  .
+  Perhaps the most direct competitor to `natural-arithmetic` is a
+  typechecker plugin like
+  <https://github.com/yav/type-nat-solver type-nat-solver>. The big
+  difference is that `type-nat-solver` can really only be used in
+  application code, not in library code. This is because libraries
+  should not require the presence of typechecker plugins. Technically,
+  they can (you could document it), but many developers will not
+  use libraries that have unusual install procedures like this. 
+  .
+  This library, in places, requires users to use the 'TypeApplications`
+  language extension. This is done when a number is only need at
+  the type level (without a runtime witness).
+  .
+  This library uses a non-minimal core, providing redundant primitives
+  in `Arithmetic.Lt` and `Arithmetic.Lte`. This is done in the interest
+  of making it easy for user to assemble proofs. Recall that proof
+  assembly is done by hand rather than by an SMT solver, so removing
+  some tediousness from this is helpful to users. 
+  .
+  This library provides left and variants variants of several functions.
+  For example, `Arithmetic.Lte` provides both `substituteL` and
+  `substituteR`. This is only done when there are two variants of
+  a function. For substitution, this is the case because we have
+  `b = c, a ≤ b ==> a ≤ c` and `a = c, a ≤ b ==> c ≤ b`. So, we
+  provide both `substituteL` and `substituteR`. However,
+  for addition of inequalities, we have four possible variants:
+  `a ≤ b, c ≤ d ==> a + c ≤ b + d`, `a ≤ b, c ≤ d ==> c + a ≤ b + d`,
+  `a ≤ b, c ≤ d ==> a + c ≤ d + b`, `a ≤ b, c ≤ d ==> c + a ≤ d + b`.
+  Consequently, we only provide a single `plus` function, and users
+  must use `Arithmetic.Plus.commutative` to further manipulate the
+  inequality.
+  .
+  Here are the proof-manipulation vocabulary used by this library.
+  Many of these terms are not standard, but we try to be consistent
+  in this library:
+  .
+  * Weaken: Increase an upper bound without changing the bounded value
+  .
+  * Increment: Increase an upper bound along with the bounded value
+  .
+  * Decrement: Decrease an upper bound along with the bounded value
+  .
+  * Substitute: Replace a number with an equal number
+homepage: https://github.com/andrewthad/natural-arithmetic
+bug-reports: https://github.com/andrewthad/natural-arithmetic/issues
+license: BSD-3-Clause
+license-file: LICENSE
+author: Andrew Martin
+maintainer: andrew.thaddeus@gmail.com
+copyright: 2019 Andrew Martin
+category: Math
+extra-source-files: CHANGELOG.md
+
+library
+  exposed-modules:
+    Arithmetic.Fin
+    Arithmetic.Equal
+    Arithmetic.Lt
+    Arithmetic.Lte
+    Arithmetic.Nat
+    Arithmetic.Types
+    Arithmetic.Unsafe
+    Arithmetic.Plus
+  build-depends: base>=4.11 && <5
+  hs-source-dirs: src
+  default-language: Haskell2010
+  ghc-options: -Wall -O2
diff --git a/src/Arithmetic/Equal.hs b/src/Arithmetic/Equal.hs
new file mode 100644
--- /dev/null
+++ b/src/Arithmetic/Equal.hs
@@ -0,0 +1,22 @@
+{-# language DataKinds #-}
+{-# language ExplicitForAll #-}
+{-# language KindSignatures #-}
+{-# language TypeOperators #-}
+
+module Arithmetic.Equal
+  ( symmetric
+  , plusR
+  , plusL
+  ) where
+
+import Arithmetic.Unsafe (type (:=:)(Eq))
+import GHC.TypeNats (type (+))
+
+symmetric :: (m :=: n) -> (n :=: m)
+symmetric Eq = Eq
+
+plusL :: forall c m n. (m :=: n) -> (c + m :=: c + n)
+plusL Eq = Eq
+
+plusR :: forall c m n. (m :=: n) -> (m + c :=: n + c)
+plusR Eq = Eq
diff --git a/src/Arithmetic/Fin.hs b/src/Arithmetic/Fin.hs
new file mode 100644
--- /dev/null
+++ b/src/Arithmetic/Fin.hs
@@ -0,0 +1,176 @@
+{-# language BangPatterns #-}
+{-# language DataKinds #-}
+{-# language ExplicitNamespaces #-}
+{-# language GADTs #-}
+{-# language KindSignatures #-}
+{-# language ScopedTypeVariables #-}
+{-# language TypeApplications #-}
+{-# language TypeOperators #-}
+module Arithmetic.Fin
+  ( -- * Modification
+    incrementL
+  , incrementR
+  , weakenL
+  , weakenR
+    -- * Traverse
+  , ascend
+  , ascendM
+  , ascendM_
+  , ascending
+  , descending
+  , ascendingSlice
+    -- * Absurdities
+  , absurd
+    -- * Demote
+  , demote
+  ) where
+
+import Prelude hiding (last)
+
+import Arithmetic.Nat ((<?))
+import Arithmetic.Types (Fin(..),Difference(..),Nat,type (<), type (<=), type (:=:))
+import GHC.TypeNats (type (+))
+
+import qualified Arithmetic.Lt as Lt
+import qualified Arithmetic.Lte as Lte
+import qualified Arithmetic.Nat as Nat
+import qualified Arithmetic.Plus as Plus
+
+-- | Raise the index by @m@ and weaken the bound by @m@, adding
+-- @m@ to the right-hand side of @n@.
+incrementR :: forall n m. Nat m -> Fin n -> Fin (n + m)
+incrementR m (Fin i pf) = Fin (Nat.plus i m) (Lt.incrementR @m pf)
+
+-- | Raise the index by @m@ and weaken the bound by @m@, adding
+-- @m@ to the left-hand side of @n@.
+incrementL :: forall n m. Nat m -> Fin n -> Fin (m + n)
+incrementL m (Fin i pf) = Fin (Nat.plus m i) (Lt.incrementL @m pf)
+
+-- | Weaken the bound by one. This does not change the index.
+weakenL :: forall n m. Fin n -> Fin (m + n)
+weakenL (Fin i pf) = Fin i
+  ( Lt.substituteR
+    (Plus.commutative @n @m)
+    (Lt.plus pf (Lte.zero @m))
+  )
+
+-- side of @n@. This does not change the index.
+weakenR :: forall n m. Fin n -> Fin (n + m)
+weakenR (Fin i pf) = Fin i (Lt.plus pf Lte.zero)
+
+-- | A finite set of no values is impossible.
+absurd :: Fin 0 -> void
+absurd (Fin _ pf) = Lt.absurd pf
+
+-- | Strict fold over the numbers bounded by @n@ in ascending
+-- order. For convenince, this differs from @foldl'@ in the
+-- order of the parameters differs from @foldl@. Roughly:
+--
+-- > ascend 4 z f = f 3 (f 2 (f 1 (f 0 z)))
+ascend :: forall a n.
+     Nat n -- ^ Upper bound
+  -> a -- ^ Initial accumulator
+  -> (Fin n -> a -> a) -- ^ Update accumulator
+  -> a
+{-# inline ascend #-}
+ascend !n !b0 f = go Nat.zero b0
+  where
+  go :: Nat m -> a -> a
+  go !m !b = case m <? n of
+    Nothing -> b
+    Just lt -> go (Nat.succ m) (f (Fin m lt) b)
+
+-- | Strict monadic left fold over the numbers bounded by @n@
+-- in ascending order. Roughly:
+--
+-- > ascendM 4 z f =
+-- >   f 0 z0 >>= \z1 ->
+-- >   f 1 z1 >>= \z2 ->
+-- >   f 2 z2 >>= \z3 ->
+-- >   f 3 z3
+ascendM :: forall m a n. Monad m
+  => Nat n -- ^ Upper bound
+  -> a -- ^ Initial accumulator
+  -> (Fin n -> a -> m a) -- ^ Update accumulator
+  -> m a
+{-# inline ascendM #-}
+ascendM !n !b0 f = go Nat.zero b0
+  where
+  go :: Nat p -> a -> m a
+  go !m !b = case m <? n of
+    Nothing -> pure b
+    Just lt -> go (Nat.succ m) =<< f (Fin m lt) b
+
+-- | Monadic traversal of the numbers bounded by @n@
+-- in ascending order.
+--
+-- > ascendM_ 4 f = f 0 *> f 1 *> f 2 *> f 3
+ascendM_ :: forall m a n. Applicative m
+  => Nat n -- ^ Upper bound
+  -> (Fin n -> m a) -- ^ Effectful interpretion
+  -> m ()
+{-# inline ascendM_ #-}
+ascendM_ !n f = go Nat.zero
+  where
+  go :: Nat p -> m ()
+  go !m = case m <? n of
+    Nothing -> pure ()
+    Just lt -> f (Fin m lt) *> go (Nat.succ m)
+
+-- | Generate all values of a finite set in ascending order.
+--
+-- >>> ascending (Nat.constant @3)
+-- [0, 1, 2]
+ascending :: forall n. Nat n -> [Fin n]
+ascending !n = go Nat.zero
+  where
+  go :: Nat m -> [Fin n]
+  go !m = case m <? n of
+    Nothing -> []
+    Just lt -> Fin m lt : go (Nat.succ m)
+
+-- | Generate all values of a finite set in descending order.
+--
+-- >>> descending (Nat.constant @3)
+-- [2, 1, 0]
+descending :: forall n. Nat n -> [Fin n]
+descending n = go n Lte.reflexive
+  where
+    go :: forall m. Nat m -> (m <= n) -> [Fin n]
+    go !m !lt = case Nat.monus m Nat.one of
+      Nothing -> []
+      Just (Difference mpred eq) -> go2 lt mpred eq
+    go2 :: forall m c. (m <= n) -> Nat c -> (c + 1 :=: m) -> [Fin n]
+    go2 !lt !c !eq = 
+        let ceeLtEm :: c < m
+            ceeLtEm = id
+              $ Lt.substituteR eq
+              $ Lt.substituteL Plus.zeroL
+              $ Lt.incrementL @c Lt.zero
+         in Fin c (Lt.transitiveNonstrictR ceeLtEm lt) : go c
+              (Lte.transitive (Lte.substituteR eq (Lte.weakenR @1 (Lte.reflexive @c))) lt)
+
+-- | Generate 'len' values starting from 'off'.
+--
+-- >>> slice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)
+-- [2, 3, 4]
+ascendingSlice :: forall n off len.
+     Nat off
+  -> Nat len
+  -> (off + len < n)
+  -> [Fin n]
+ascendingSlice off len !offPlusLenLtEn = go Nat.zero
+  where
+    go :: Nat m -> [Fin n]
+    go !m = case m <? len of
+      Nothing -> []
+      Just emLtLen ->
+        let !offPlusEmLtOffPlusLen = Lt.incrementL @off emLtLen
+            !offPlusEmLtEn = Lt.transitive offPlusEmLtOffPlusLen offPlusLenLtEn
+         in Fin (Nat.plus off m) offPlusEmLtEn : go (Nat.succ m)
+
+-- | Extract the 'Int' from a 'Fin n'. This is intended to be used
+-- at a boundary where a safe interface meets the unsafe primitives
+-- on top of which it is built.
+demote :: Fin n -> Int
+demote (Fin i _) = Nat.demote i
diff --git a/src/Arithmetic/Lt.hs b/src/Arithmetic/Lt.hs
new file mode 100644
--- /dev/null
+++ b/src/Arithmetic/Lt.hs
@@ -0,0 +1,99 @@
+{-# language DataKinds #-}
+{-# language ExplicitForAll #-}
+{-# language KindSignatures #-}
+{-# language TypeFamilies #-}
+{-# language TypeOperators #-}
+
+module Arithmetic.Lt
+  ( -- * Special Inequalities
+    zero
+    -- * Substitution
+  , substituteL
+  , substituteR
+    -- * Increment
+  , incrementL
+  , incrementR
+    -- * Weaken
+  , weakenL
+  , weakenR
+    -- * Composition
+  , plus
+  , transitive
+  , transitiveNonstrictL
+  , transitiveNonstrictR
+    -- * Absurdities
+  , absurd
+    -- * Integration with GHC solver
+  , constant
+  ) where
+
+import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq))
+import Arithmetic.Unsafe (type (<=)(Lte))
+import GHC.TypeNats (CmpNat,type (+))
+
+import qualified GHC.TypeNats as GHC
+
+-- | Replace the right-hand side of a strict inequality
+-- with an equal number.
+substituteL :: (b :=: c) -> (a < b) -> (a < c)
+substituteL Eq Lt = Lt
+
+-- | Replace the right-hand side of a strict inequality
+-- with an equal number.
+substituteR :: (b :=: c) -> (a < b) -> (a < c)
+substituteR Eq Lt = Lt
+
+-- | Add a strict inequality to a nonstrict inequality.
+plus :: (a < b) -> (c <= d) -> (a + c < b + d)
+plus Lt Lte = Lt
+
+-- | Add a constant to the left-hand side of both sides of
+-- the strict inequality.
+incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a < b) -> (c + a < c + b)
+incrementL Lt = Lt
+
+-- | Add a constant to the right-hand side of both sides of
+-- the strict inequality.
+incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a < b) -> (a + c < b + c)
+incrementR Lt = Lt
+
+-- | Add a constant to the left-hand side of the right-hand side of
+-- the strict inequality.
+weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a < b) -> (a < c + b)
+weakenL Lt = Lt
+
+-- | Add a constant to the right-hand side of the right-hand side of
+-- the strict inequality.
+weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a < b) -> (a < b + c)
+weakenR Lt = Lt
+
+-- | Compose two strict inequalities using transitivity.
+transitive :: (a < b) -> (b < c) -> (a < c)
+transitive Lt Lt = Lt
+
+-- | Compose a strict inequality (the first argument) with a nonstrict
+-- inequality (the second argument).
+transitiveNonstrictR :: (a < b) -> (b <= c) -> (a < c)
+transitiveNonstrictR Lt Lte = Lt
+
+transitiveNonstrictL :: (a <= b) -> (b < c) -> (a < c)
+transitiveNonstrictL Lte Lt = Lt
+
+-- | Zero is less than one.
+zero :: 0 < 1
+zero = Lt
+
+-- | Nothing is less than zero.
+absurd :: n < 0 -> void
+absurd Lt = error "Arithmetic.Nat.absurd: n < 0"
+
+-- | Use GHC's built-in type-level arithmetic to prove
+-- that one number is less than another. The type-checker
+-- only reduces 'CmpNat' if both arguments are constants.
+constant :: forall a b. (CmpNat a b ~ 'LT) => (a < b)
+constant = Lt
+
diff --git a/src/Arithmetic/Lte.hs b/src/Arithmetic/Lte.hs
new file mode 100644
--- /dev/null
+++ b/src/Arithmetic/Lte.hs
@@ -0,0 +1,113 @@
+{-# language DataKinds #-}
+{-# language ExplicitForAll #-}
+{-# language KindSignatures #-}
+{-# language TypeFamilies #-}
+{-# language TypeOperators #-}
+
+module Arithmetic.Lte
+  ( -- * Special Inequalities
+    zero
+  , reflexive
+    -- * Substitution
+  , substituteL
+  , substituteR
+    -- * Increment
+  , incrementL
+  , incrementR
+    -- * Decrement
+  , decrementL
+  , decrementR
+    -- * Weaken
+  , weakenL
+  , weakenR
+    -- * Composition
+  , transitive
+  , plus
+    -- * Convert Strict Inequality
+  , fromStrict
+    -- * Integration with GHC solver
+  , constant
+  ) where
+
+import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq))
+import Arithmetic.Unsafe (type (<=)(Lte))
+import GHC.TypeNats (CmpNat,type (+))
+
+import qualified GHC.TypeNats as GHC
+
+-- | Replace the right-hand side of a strict inequality
+-- with an equal number.
+substituteL :: (b :=: c) -> (a <= b) -> (a <= c)
+substituteL Eq Lte = Lte
+
+-- | Replace the right-hand side of a strict inequality
+-- with an equal number.
+substituteR :: (b :=: c) -> (a <= b) -> (a <= c)
+substituteR Eq Lte = Lte
+
+-- | Add two inequalities.
+plus :: (a <= b) -> (c <= d) -> (a + c <= b + d)
+plus Lte Lte = Lte
+
+-- | Compose two inequalities using transitivity.
+transitive :: (a <= b) -> (b <= c) -> (a <= c)
+transitive Lte Lte = Lte
+
+-- | Any number is less-than-or-equal-to itself.
+reflexive :: a <= a
+reflexive = Lte
+
+-- | Add a constant to the left-hand side of both sides of
+-- the inequality.
+incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <= b) -> (c + a <= c + b)
+incrementL Lte = Lte
+
+-- | Add a constant to the right-hand side of both sides of
+-- the inequality.
+incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <= b) -> (a + c <= b + c)
+incrementR Lte = Lte
+
+-- | Add a constant to the left-hand side of the right-hand side of
+-- the inequality.
+weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <= b) -> (a <= c + b)
+weakenL Lte = Lte
+
+-- | Add a constant to the right-hand side of the right-hand side of
+-- the inequality.
+weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <= b) -> (a <= b + c)
+weakenR Lte = Lte
+
+-- | Subtract a constant from the left-hand side of both sides of
+-- the inequality. This is the opposite of 'incrementL'.
+decrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (c + a <= c + b) -> (a <= b)
+decrementL Lte = Lte
+
+-- | Subtract a constant from the right-hand side of both sides of
+-- the inequality. This is the opposite of 'incrementR'.
+decrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a + c <= b + c) -> (a <= b)
+decrementR Lte = Lte
+
+-- | Weaken a strict inequality to a non-strict inequality.
+fromStrict :: (a < b) -> (a <= b)
+fromStrict Lt = Lte
+
+-- | Zero is less-than-or-equal-to any number.
+zero :: 0 <= a
+zero = Lte
+
+-- | Use GHC's built-in type-level arithmetic to prove
+-- that one number is less-than-or-equal-to another. The type-checker
+-- only reduces 'CmpNat' if both arguments are constants.
+constant :: forall a b. (IsLte (CmpNat a b) ~ 'True) => (a <= b)
+constant = Lte
+
+type family IsLte (o :: Ordering) :: Bool where
+  IsLte 'GT = 'False
+  IsLte 'LT = 'True
+  IsLte 'EQ = 'True
diff --git a/src/Arithmetic/Nat.hs b/src/Arithmetic/Nat.hs
new file mode 100644
--- /dev/null
+++ b/src/Arithmetic/Nat.hs
@@ -0,0 +1,103 @@
+{-# language DataKinds #-}
+{-# language ExplicitForAll #-}
+{-# language KindSignatures #-}
+{-# language MagicHash #-}
+{-# language ScopedTypeVariables #-}
+{-# language TypeOperators #-}
+
+module Arithmetic.Nat
+  ( -- * Addition
+    plus
+    -- * Subtraction
+  , monus
+    -- * Successor
+  , succ
+    -- * Compare
+  , testEqual
+  , testLessThan
+  , testLessThanEqual
+  , (=?)
+  , (<?)
+  , (<=?)
+    -- * Constants
+  , zero
+  , one
+  , constant
+    -- * Demote
+  , demote
+  ) where
+
+import Prelude hiding (succ)
+
+import Arithmetic.Types
+import Arithmetic.Unsafe ((:=:)(Eq), type (<=)(Lte))
+import Arithmetic.Unsafe (Nat(Nat),type (<)(Lt))
+import GHC.Exts (Proxy#,proxy#)
+import GHC.TypeNats (type (+),KnownNat,natVal')
+
+-- | Infix synonym of 'testLessThan'.
+(<?) :: Nat a -> Nat b -> Maybe (a < b)
+(<?) = testLessThan
+
+-- | Infix synonym of 'testLessThanEqual'.
+(<=?) :: Nat a -> Nat b -> Maybe (a <= b)
+(<=?) = testLessThanEqual
+
+-- | Infix synonym of 'testEqual'.
+(=?) :: Nat a -> Nat b -> Maybe (a :=: b)
+(=?) = testEqual
+
+-- | Is the first argument strictly less than the second
+-- argument?
+testLessThan :: Nat a -> Nat b -> Maybe (a < b)
+testLessThan (Nat x) (Nat y) = if x < y
+  then Just Lt
+  else Nothing
+
+-- | Is the first argument less-than-or-equal-to the second
+-- argument?
+testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b)
+testLessThanEqual (Nat x) (Nat y) = if x <= y
+  then Just Lte
+  else Nothing
+
+-- | Are the two arguments equal to one another?
+testEqual :: Nat a -> Nat b -> Maybe (a :=: b)
+testEqual (Nat x) (Nat y) = if x == y
+  then Just Eq
+  else Nothing
+
+-- | Add two numbers.
+plus :: Nat a -> Nat b -> Nat (a + b)
+plus (Nat x) (Nat y) = Nat (x + y)
+
+-- | The successor of a number.
+succ :: Nat a -> Nat (a + 1)
+succ n = plus n one
+
+-- | Subtract the second argument from the first argument.
+monus :: Nat a -> Nat b -> Maybe (Difference a b)
+{-# inline monus #-}
+monus (Nat a) (Nat b) = let c = a - b in if c >= 0
+  then Just (Difference (Nat c) Eq)
+  else Nothing
+
+-- | The number zero.
+zero :: Nat 0
+zero = Nat 0
+
+-- | The number one.
+one :: Nat 1
+one = Nat 1
+
+-- | Use GHC's built-in type-level arithmetic to create a witness
+-- of a type-level number. This only reduces if the number is a
+-- constant.
+constant :: forall n. KnownNat n => Nat n
+constant = Nat (fromIntegral (natVal' (proxy# :: Proxy# n)))
+
+-- | Extract the 'Int' from a 'Nat'. This is intended to be used
+-- at a boundary where a safe interface meets the unsafe primitives
+-- on top of which it is built.
+demote :: Nat n -> Int
+demote (Nat n) = n
diff --git a/src/Arithmetic/Plus.hs b/src/Arithmetic/Plus.hs
new file mode 100644
--- /dev/null
+++ b/src/Arithmetic/Plus.hs
@@ -0,0 +1,31 @@
+{-# language DataKinds #-}
+{-# language TypeOperators #-}
+{-# language KindSignatures #-}
+{-# language ExplicitForAll #-}
+{-# language AllowAmbiguousTypes #-}
+
+module Arithmetic.Plus
+  ( zeroL
+  , zeroR
+  , commutative
+  , associative
+  ) where
+
+import Arithmetic.Unsafe (type (:=:)(Eq))
+import GHC.TypeNats (type (+))
+
+-- | Any number plus zero is equal to the original number.
+zeroR :: m :=: (m + 0)
+zeroR = Eq
+
+-- | Zero plus any number is equal to the original number.
+zeroL :: m :=: (0 + m)
+zeroL = Eq
+
+-- | Addition is commutative.
+commutative :: forall a b. a + b :=: b + a
+commutative = Eq
+
+-- | Addition is associative.
+associative :: forall a b c. (a + b) + c :=: a + (b + c)
+associative = Eq
diff --git a/src/Arithmetic/Types.hs b/src/Arithmetic/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Arithmetic/Types.hs
@@ -0,0 +1,46 @@
+{-# language DataKinds #-}
+{-# language ExplicitNamespaces #-}
+{-# language GADTs #-}
+{-# language KindSignatures #-}
+{-# language RankNTypes #-}
+{-# language TypeOperators #-}
+
+module Arithmetic.Types
+  ( Nat
+  , Difference(..)
+  , Fin(..)
+  , type (<)
+  , type (<=)
+  , type (:=:)
+  ) where
+
+import Arithmetic.Unsafe (Nat(getNat), type (<=))
+import Arithmetic.Unsafe (type (<), type (:=:))
+import Data.Kind (type Type)
+import GHC.TypeNats (type (+))
+
+import qualified GHC.TypeNats as GHC
+
+-- | A finite set of 'n' elements. 'Fin n = { 0 .. n - 1 }'
+data Fin :: GHC.Nat -> Type where
+  Fin :: forall m n.
+    { index :: !(Nat m)
+    , proof :: !(m < n)
+    } -> Fin n
+
+-- | Proof that the first argument can be expressed as the
+-- sum of the second argument and some other natural number.
+data Difference :: GHC.Nat -> GHC.Nat -> Type where
+  -- It is safe for users of this library to use this data constructor
+  -- freely. However, note that the interesting Difference values come
+  -- from Arithmetic.Nat.monus, which is a primitive.
+  Difference :: forall a b c. Nat c -> (c + b :=: a) -> Difference a b
+
+instance Show (Fin n) where
+  showsPrec p (Fin i _) = showString "Fin " . showsPrec p (getNat i)
+
+instance Eq (Fin n) where
+  Fin x _ == Fin y _ = getNat x == getNat y
+
+instance Ord (Fin n) where
+  Fin x _ `compare` Fin y _ = compare (getNat x) (getNat y)
diff --git a/src/Arithmetic/Unsafe.hs b/src/Arithmetic/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/src/Arithmetic/Unsafe.hs
@@ -0,0 +1,57 @@
+{-# language DataKinds #-}
+{-# language ExplicitNamespaces #-}
+{-# language GADTSyntax #-}
+{-# language KindSignatures #-}
+{-# language RoleAnnotations #-}
+{-# language TypeOperators #-}
+
+module Arithmetic.Unsafe
+  ( Nat(..)
+  , type (<)(Lt)
+  , type (<=)(Lte)
+  , type (:=:)(Eq)
+  ) where
+
+import Prelude hiding ((>=),(<=))
+
+import Control.Category (Category)
+import Data.Kind (Type)
+
+import qualified Control.Category
+import qualified GHC.TypeNats as GHC
+
+-- Do not import this module unless you enjoy pain.
+-- Using this library to implement length-indexed arrays
+-- or sized builders does not require importing this
+-- module to get the value out of the Nat data constructor.
+-- Use Arithmetic.Nat.demote for this purpose.
+
+infix 4 <
+infix 4 <=
+infix 4 :=:
+
+-- | A value-level representation of a natural number @n@.
+newtype Nat (n :: GHC.Nat) = Nat { getNat :: Int }
+type role Nat nominal
+
+-- | Proof that the first argument is strictly less than the
+-- second argument.
+data (<) :: GHC.Nat -> GHC.Nat -> Type where
+  Lt :: a < b
+
+-- | Proof that the first argument is less than or equal to the
+-- second argument.
+data (<=) :: GHC.Nat -> GHC.Nat -> Type where
+  Lte :: a <= b
+
+-- | Proof that the first argument is equal to the second argument.
+data (:=:) :: GHC.Nat -> GHC.Nat -> Type where
+  Eq :: a :=: b
+
+instance Category (<=) where
+  id = Lte
+  Lte . Lte = Lte
+
+instance Category (:=:) where
+  id = Eq
+  Eq . Eq = Eq