diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+The MIT License
+
+Copyright (c) 2013-2017 Front Row Education, Inc. www.frontrowed.com
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.
diff --git a/README.lhs b/README.lhs
new file mode 100644
--- /dev/null
+++ b/README.lhs
@@ -0,0 +1,201 @@
+# closed: Integers bounded by a closed interval
+
+## Build
+
+  ```plaintext
+  stack build
+  ```
+
+## Tutorial
+
+### Overview
+
+This package exports one core data type `Closed (n :: Nat) (m :: Nat)`
+for describing integers bounded by a closed interval. That is, given
+`cx :: Closed n m`, `getClosed cx` is an integer `x` where `n <= x <= m`.
+
+We also export a type family `Bounds` for describing open and half-open
+intervals in terms of closed intervals.
+
+  ```plaintext
+  Bounds (Inclusive 0) (Inclusive 10) => Closed 0 10
+  Bounds (Inclusive 0) (Exclusive 10) => Closed 0 9
+  Bounds (Exclusive 0) (Inclusive 10) => Closed 1 10
+  Bounds (Exclusive 0) (Exclusive 10) => Closed 1 9
+  ```
+
+### Preamble
+
+  For most uses of `closed`, you'll only need `DataKinds` and maybe
+  `TypeFamilies`. The other extensions below just make some of the
+  tests concise.
+
+  ```haskell
+  {-# LANGUAGE TypeFamilies #-}
+  {-# LANGUAGE DataKinds #-}
+  {-# LANGUAGE OverloadedStrings #-}
+  {-# LANGUAGE OverloadedLists #-}
+  {-# LANGUAGE TypeApplications #-}
+  {-# LANGUAGE ScopedTypeVariables #-}
+  {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+
+  module Main where
+
+  import Closed
+  import Control.Exception
+  import Data.Aeson
+  import qualified Data.Csv as CSV
+  import Data.Vector
+  import Data.Proxy
+  import GHC.TypeLits
+  import Test.Hspec
+  import Test.Hspec.QuickCheck
+
+  main :: IO ()
+  main = hspec $ do
+  ```
+
+### Construction
+
+  The safe constructor `closed` uses `Maybe` to indicate failure. There is
+  also an unsafe constructor `unsafeClosed` as well as a `Num` instance that implements
+  `fromInteger`.
+
+  ```haskell
+    describe "safe construction" $ do
+
+      it "should successfully construct values in the specified bounds" $ do
+        let result = closed 2 :: Maybe (Bounds (Inclusive 2) (Exclusive 5))
+        getClosed <$> result `shouldBe` Just 2
+
+      it "should fail to construct values outside the specified bounds" $ do
+        let result = closed 1 :: Maybe (Bounds (Inclusive 2) (Exclusive 5))
+        getClosed <$> result `shouldBe` Nothing
+
+    describe "unsafe construction" $ do
+
+      it "should successfully construct values in the specified bounds" $ do
+        let result = unsafeClosed 2 :: Bounds (Inclusive 2) (Exclusive 5)
+        getClosed result `shouldBe` 2
+
+      it "should fail to construct values outside the specified bounds" $ do
+        let result = unsafeClosed 1 :: Bounds (Inclusive 2) (Exclusive 5)
+        evaluate (getClosed result) `shouldThrow` anyErrorCall
+
+    describe "unsafe literal construction" $ do
+
+      it "should successfully construct values in the specified bounds" $ do
+        let result = 2 :: Bounds (Inclusive 2) (Exclusive 5)
+        getClosed result `shouldBe` 2
+
+      it "should fail to construct values outside the specified bounds" $ do
+        let result = 1 :: Bounds (Inclusive 2) (Exclusive 5)
+        evaluate (getClosed result) `shouldThrow` anyErrorCall
+  ```
+
+### Elimination
+
+  Use `getClosed` to extract the `Integer` from a `Closed` value.
+
+  ```haskell
+    describe "elimination" $ do
+
+      it "should allow the integer value to be extracted" $ do
+        let result = 1 :: Bounds (Inclusive 0) (Exclusive 10)
+        getClosed result `shouldBe` 1
+  ```
+
+### Bounds Manipulation
+
+  The upper and lower bounds can be queried, strengthened, and weakened.
+
+  ```haskell
+    describe "bounds manipulation" $ do
+
+      let cx = 4 :: Bounds (Inclusive 2) (Exclusive 10)
+
+      it "should allow querying the bounds" $ do
+        upperBound cx `shouldBe` (Proxy :: Proxy 9)
+        lowerBound cx `shouldBe` (Proxy :: Proxy 2)
+
+      it "should allow weakening the bounds" $ do
+        upperBound (weakenUpper cx) `shouldBe` (Proxy :: Proxy 10)
+        lowerBound (weakenLower cx) `shouldBe` (Proxy :: Proxy 1)
+
+      it "should allow weakening the bounds by more than one" $ do
+        upperBound (weakenUpper cx) `shouldBe` (Proxy :: Proxy 20)
+        lowerBound (weakenLower cx) `shouldBe` (Proxy :: Proxy 0)
+
+      it "should allow strengthening the bounds" $ do
+        upperBound <$> strengthenUpper cx `shouldBe` Just (Proxy :: Proxy 8)
+        lowerBound <$> strengthenLower cx `shouldBe` Just (Proxy :: Proxy 3)
+
+      it "should allow strengthening the bounds by more than one" $ do
+        upperBound <$> strengthenUpper cx `shouldBe` Just (Proxy :: Proxy 7)
+        lowerBound <$> strengthenLower cx `shouldBe` Just (Proxy :: Proxy 4)
+  ```
+
+### Arithmetic
+
+  Arithmetic gets stuck at the upper and lower bounds instead of wrapping.
+
+  ```haskell
+    describe "arithmetic" $ do
+
+      it "addition to the maxBound should have no effect" $ do
+        let result = maxBound :: Bounds (Inclusive 1) (Exclusive 10)
+        result + 1 `shouldBe` result
+
+      it "subtraction from the minBound should have no effect" $ do
+        let result = minBound :: Bounds (Inclusive 1) (Exclusive 10)
+        result - 1 `shouldBe` result
+  ```
+
+### Serialization
+
+  Parsing of closed values is strict.
+
+  ```haskell
+    describe "json" $ do
+
+      it "should successfully parse values in the specified bounds" $ do
+        let result = eitherDecode "1" :: Either String (Bounds (Inclusive 1) (Exclusive 10))
+        result `shouldBe` Right 1
+
+      it "should fail to parse values outside the specified bounds" $ do
+        let result = eitherDecode "0" :: Either String (Bounds (Inclusive 1) (Exclusive 10))
+        result `shouldBe` Left "Error in $: parseJSON: Integer 0 is not representable in Closed 1 9"
+
+    describe "csv" $ do
+
+      it "should successfully parse values in the specified bounds" $ do
+        let result = CSV.decode CSV.NoHeader "1" :: Either String (Vector (CSV.Only (Bounds (Inclusive 1) (Exclusive 10))))
+        result `shouldBe` Right [CSV.Only 1]
+
+      it "should fail to parse values outside the specified bounds" $ do
+        let result = CSV.decode CSV.NoHeader "0" :: Either String (Vector (CSV.Only (Bounds (Inclusive 1) (Exclusive 10))))
+        result `shouldBe` Left "parse error (Failed reading: conversion error: parseField: Integer 0 is not representable in Closed 1 9) at \"\""
+  ```
+
+### Testing
+
+  Closed values can be generated with QuickCheck
+
+  ```haskell
+    describe "quickcheck" $ do
+
+      prop "should always generate values in the specified bounds" $
+        \(cx :: Closed 0 1000) ->
+          natVal (lowerBound cx) <= getClosed cx &&
+          getClosed cx <= natVal (upperBound cx)
+  ```
+
+## Remarks
+
+This library was inspired by [finite-typelits](https://hackage.haskell.org/package/finite-typelits)
+and [finite-typelits-bounded](https://github.com/pseudonom/finite-typelits-bounded). The differences
+are summarized below:
+
+* `finite-typelits` - A value of `Finite (n :: Nat)` is in the half-open interval `[0, n)`. Uses modular arithmetic.
+* `finite-typelits-bounded` - A value of `Finite (n :: Nat)` is in the half-open interval `[0, n)`. Uses bounded arithmetic.
+* `closed` - A value of `Closed (n :: Nat) (m :: Nat)` is in the closed interval `[n, m]`. Uses bounded arithmetic.
diff --git a/closed.cabal b/closed.cabal
new file mode 100644
--- /dev/null
+++ b/closed.cabal
@@ -0,0 +1,57 @@
+-- This file has been generated from package.yaml by hpack version 0.17.1.
+--
+-- see: https://github.com/sol/hpack
+
+name:           closed
+version:        0.1.0
+synopsis:       Integers bounded by a closed interval
+description:    Integers bounded by a closed interval
+category:       Data
+homepage:       https://github.com/frontrowed/closed#readme
+bug-reports:    https://github.com/frontrowed/closed/issues
+author:         Chris Parks <chris@frontrowed.com>
+maintainer:     Front Row Education <engineering@frontrowed.com>
+license:        MIT
+license-file:   LICENSE
+build-type:     Simple
+cabal-version:  >= 1.10
+
+extra-source-files:
+    README.lhs
+
+source-repository head
+  type: git
+  location: https://github.com/frontrowed/closed
+
+library
+  hs-source-dirs:
+      library
+  build-depends:
+      base >= 4.9 && < 5
+    , deepseq
+    , aeson
+    , cassava
+    , hashable
+    , QuickCheck
+  exposed-modules:
+      Closed
+      Closed.Internal
+  default-language: Haskell2010
+
+test-suite readme
+  type: exitcode-stdio-1.0
+  main-is: README.lhs
+  ghc-options: -Wall -pgmL markdown-unlit
+  build-depends:
+      base >= 4.9 && < 5
+    , deepseq
+    , aeson
+    , cassava
+    , hashable
+    , QuickCheck
+    , base
+    , closed
+    , hspec
+    , markdown-unlit
+    , vector
+  default-language: Haskell2010
diff --git a/library/Closed.hs b/library/Closed.hs
new file mode 100644
--- /dev/null
+++ b/library/Closed.hs
@@ -0,0 +1,25 @@
+module Closed
+  ( Endpoint(..)
+  , Closed
+  , Bounds
+  , Single
+  , FiniteNat
+  , closed
+  , unsafeClosed
+  , getClosed
+  , lowerBound
+  , upperBound
+  , equals
+  , cmp
+  , natToClosed
+  , weakenUpper
+  , weakenLower
+  , strengthenUpper
+  , strengthenLower
+  , add
+  , sub
+  , multiply
+  , isValidClosed
+  ) where
+
+import Closed.Internal
diff --git a/library/Closed/Internal.hs b/library/Closed/Internal.hs
new file mode 100644
--- /dev/null
+++ b/library/Closed/Internal.hs
@@ -0,0 +1,221 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+module Closed.Internal where
+
+import Data.Aeson
+import qualified Data.Csv as CSV
+import Data.Hashable
+import Data.Maybe
+import Data.Proxy
+import Data.Ratio
+import Control.DeepSeq
+import Control.Monad
+import GHC.Generics
+import GHC.Stack
+import GHC.TypeLits
+import Test.QuickCheck
+
+newtype Closed (n :: Nat) (m :: Nat)
+  = Closed { getClosed :: Integer }
+  deriving (Generic)
+
+-- | Describe whether the endpoint of a 'Bounds' includes
+-- or excludes its argument
+data Endpoint
+  -- | Endpoint includes its argument
+  = Inclusive Nat
+  -- | Endpoint excludes its argument
+  | Exclusive Nat
+
+-- | Syntactic sugar to express open and half-open intervals using
+-- the 'Closed' type
+type family Bounds (lhs :: Endpoint) (rhs :: Endpoint) :: * where
+  Bounds (Inclusive n) (Inclusive m) = Closed  n       m
+  Bounds (Inclusive n) (Exclusive m) = Closed  n      (m - 1)
+  Bounds (Exclusive n) (Inclusive m) = Closed (n + 1)  m
+  Bounds (Exclusive n) (Exclusive m) = Closed (n + 1) (m - 1)
+
+-- | Syntactic sugar to express a value that has only one non-bottom
+-- inhabitant using the 'Closed' type
+type Single (n :: Nat) = Bounds ('Inclusive n) ('Inclusive n)
+
+-- | Syntactic sugar to express a value whose lower bound is zero
+type FiniteNat (rhs :: Endpoint) = Bounds ('Inclusive 0) rhs
+
+-- | Proxy for the lower bound of a 'Closed' value
+lowerBound :: Closed n m -> Proxy n
+lowerBound _ = Proxy
+
+-- | Proxy for the upper bound of a 'Closed' value
+upperBound :: Closed n m -> Proxy m
+upperBound _ = Proxy
+
+-- | Safely create a 'Closed' value using the specified argument
+closed :: forall n m. (n <= m, KnownNat n, KnownNat m) => Integer -> Maybe (Closed n m)
+closed x = result
+ where
+  extracted = fromJust result
+  result = do
+    guard $ x >= natVal (lowerBound extracted) && x <= natVal (upperBound extracted)
+    pure $ Closed x
+
+-- | Create a 'Closed' value throwing an error if the argument is not in range
+unsafeClosed :: forall n m. (HasCallStack, n <= m, KnownNat n, KnownNat m) => Integer -> Closed n m
+unsafeClosed x = result
+ where
+  result =
+    if x >= natVal (lowerBound result) && x <= natVal (upperBound result)
+      then Closed x
+      else error $ unrepresentable x result "unsafeClosed"
+
+-- | Test equality on 'Closed' values in the same range
+instance Eq (Closed n m) where
+  Closed x == Closed y = x == y
+
+-- | Compare 'Closed' values in the same range
+instance Ord (Closed n m) where
+  Closed x `compare` Closed y = x `compare` y
+
+-- | Generate the lowest and highest inhabitant of a given 'Closed' type
+instance (n <= m, KnownNat n, KnownNat m) => Bounded (Closed n m) where
+  maxBound = result
+   where
+    result = Closed (natVal (upperBound result))
+
+  minBound = result
+   where
+    result = Closed (natVal (lowerBound result))
+
+-- | Enumerate values in the range of a given 'Closed' type
+instance (n <= m, KnownNat n, KnownNat m) => Enum (Closed n m) where
+  fromEnum = fromEnum . getClosed
+  toEnum = unsafeClosed . toEnum
+  enumFrom x = enumFromTo x maxBound
+  enumFromThen x y = enumFromThenTo x y (if x >= y then minBound else maxBound)
+
+instance Show (Closed n m) where
+  showsPrec d (Closed x) = showParen (d > 9) $ showString "unsafeClosed " . showsPrec 10 x
+
+-- | Bounded arithmetic, e.g. maxBound + 1 == maxBound
+instance (n <= m, KnownNat n, KnownNat m) => Num (Closed n m) where
+  Closed x + Closed y = Closed $ min (x + y) (fromIntegral (maxBound :: Closed n m))
+  Closed x - Closed y = Closed $ max (x - y) (fromIntegral (minBound :: Closed n m))
+  Closed x * Closed y = Closed $ min (x * y) (fromIntegral (maxBound :: Closed n m))
+  abs = id
+  signum = const 1
+  fromInteger x = result
+   where
+    result =
+      if x >= natVal (lowerBound result) && x <= natVal (upperBound result)
+        then Closed x
+        else error $ unrepresentable x result "fromInteger"
+
+instance (n <= m, KnownNat n, KnownNat m) => Real (Closed n m) where
+  toRational (Closed x) = x % 1
+
+instance (n <= m, KnownNat n, KnownNat m) => Integral (Closed n m) where
+  quotRem (Closed x) (Closed y) = (Closed $ x `quot` y, Closed $ x `rem` y)
+  toInteger (Closed x) = x
+
+instance NFData (Closed n m)
+
+instance Hashable (Closed n m)
+
+instance ToJSON (Closed n m) where
+  toEncoding = toEncoding . getClosed
+  toJSON = toJSON . getClosed
+
+instance (n <= m, KnownNat n, KnownNat m) => FromJSON (Closed n m) where
+  parseJSON v = do
+    x <- parseJSON v
+    case closed x of
+      Just cx -> pure cx
+      n -> fail $ unrepresentable x (fromJust n) "parseJSON"
+
+instance CSV.ToField (Closed n m) where
+  toField = CSV.toField . getClosed
+
+instance (n <= m, KnownNat n, KnownNat m) => CSV.FromField (Closed n m) where
+  parseField s = do
+    x <- CSV.parseField s
+    case closed x of
+      Just cx -> pure cx
+      n -> fail $ unrepresentable x (fromJust n) "parseField"
+
+instance (n <= m, KnownNat n, KnownNat m) => Arbitrary (Closed n m) where
+  arbitrary =
+    Closed <$> choose (natVal @n Proxy, natVal @m Proxy)
+
+unrepresentable :: (KnownNat n, KnownNat m) => Integer -> Closed n m -> String -> String
+unrepresentable x cx prefix =
+  prefix ++ ": Integer " ++ show x ++
+  " is not representable in Closed " ++ show (natVal $ lowerBound cx) ++
+  " " ++ show (natVal $ upperBound cx)
+
+-- | Convert a type-level literal into a 'Closed' value
+natToClosed :: forall n m x proxy. (n <= x, x <= m, KnownNat x, KnownNat n, KnownNat m) => proxy x -> Closed n m
+natToClosed p = Closed $ natVal p
+
+-- | Add inhabitants at the end
+weakenUpper :: forall k n m. (n <= m, m <= k) => Closed n m -> Closed n k
+weakenUpper (Closed x) = Closed x
+
+-- | Add inhabitants at the beginning
+weakenLower :: forall k n m. (n <= m, k <= n) => Closed n m -> Closed k m
+weakenLower (Closed x) = Closed x
+
+-- | Remove inhabitants from the end. Returns 'Nothing' if the input was removed
+strengthenUpper :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed n k)
+strengthenUpper (Closed x) = result
+ where
+  result = do
+    guard $ x <= natVal (upperBound $ fromJust result)
+    pure $ Closed x
+
+-- | Remove inhabitants from the beginning. Returns 'Nothing' if the input was removed
+strengthenLower :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed k m)
+strengthenLower (Closed x) = result
+ where
+  result = do
+    guard $ x >= natVal (lowerBound $ fromJust result)
+    pure $ Closed x
+
+-- | Test two different types of 'Closed' values for equality.
+equals :: Closed n m -> Closed o p -> Bool
+equals (Closed x) (Closed y) = x == y
+infix 4 `equals`
+
+-- | Compare two different types of 'Closed' values
+cmp :: Closed n m -> Closed o p -> Ordering
+cmp (Closed x) (Closed y) = x `compare` y
+
+-- | Add two different types of 'Closed' values
+add :: Closed n m -> Closed o p -> Closed (n + o) (m + p)
+add (Closed x) (Closed y) = Closed $ x + y
+
+-- | Subtract two different types of 'Closed' values
+-- Returns 'Left' for negative results, and 'Right' for positive results.
+sub :: Closed n m -> Closed o p -> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))
+sub (Closed x) (Closed y)
+  | x >= y = Right $ Closed $ x - y
+  | otherwise = Left $ Closed $ y - x
+
+-- | Multiply two different types of 'Closed' values
+multiply :: Closed n m -> Closed o p -> Closed (n * o) (m * p)
+multiply (Closed x) (Closed y) = Closed $ x * y
+
+-- | Verifies that a given 'Closed' value is valid.
+-- Should always return 'True' unles you bring the @Closed.Internal.Closed@ constructor into scope,
+-- or use 'Unsafe.Coerce.unsafeCoerce' or other nasty hacks
+isValidClosed :: (KnownNat n, KnownNat m) => Closed n m -> Bool
+isValidClosed cx@(Closed x) =
+  natVal (lowerBound cx) <= x && x <= natVal (upperBound cx)