diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Andrew Martin (c) 2016
+
+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/src/Topaz/Rec.hs b/src/Topaz/Rec.hs
new file mode 100644
--- /dev/null
+++ b/src/Topaz/Rec.hs
@@ -0,0 +1,144 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# OPTIONS_GHC -Wall #-}
+
+module Topaz.Rec
+  ( Rec(..)
+  , (<:)
+  , map
+  , append
+  , traverse
+  , traverse_
+  , zipWith
+  , foldMap
+  , foldMap1
+  , foldl'
+    -- * Access
+  , get
+  , put
+  , gets
+  , puts
+    -- * Conversion
+  , fromSingList
+  , toSingList
+  , fromList
+  ) where
+
+import Prelude hiding (map,zipWith,foldMap,traverse)
+import Topaz.Types (Elem(..),type (++),Rec(..))
+import Data.Exists
+import qualified Data.Semigroup as SG
+
+-- | infix RecCons with proper fixity
+infixr 7 <:
+(<:) :: forall a (f :: a -> *) (r :: a) (rs :: [a]).  f r -> Rec f rs -> Rec f (r : rs)
+(<:) = RecCons
+
+map :: (forall x. f x -> g x) -> Rec f as -> Rec g as
+map _ RecNil = RecNil
+map f (RecCons x xs) = RecCons (f x) (map f xs)
+
+zipWith :: (forall x. f x -> g x -> h x) -> Rec f rs -> Rec g rs -> Rec h rs
+zipWith _ RecNil RecNil = RecNil
+zipWith f (RecCons a as) (RecCons b bs) =
+  RecCons (f a b) (zipWith f as bs)
+
+-- | Strict left fold over the elements of a record.
+foldl' :: forall f a rs.
+     (forall x. a -> f x -> a) -- ^ Reduction
+  -> a -- ^ Initial accumulator
+  -> Rec f rs -- ^ Record
+  -> a
+foldl' g !a0 = go a0 where
+  go :: forall ss. a -> Rec f ss -> a
+  go !a RecNil = a
+  go !a (RecCons r rs) = go (g a r) rs
+
+-- | Map each element of a record to a monoid and combine the results.
+foldMap :: forall f m rs. Monoid m
+  => (forall x. f x -> m)
+  -> Rec f rs
+  -> m
+foldMap f = go mempty
+  where
+  go :: forall ss. m -> Rec f ss -> m
+  go !m record = case record of
+    RecNil -> m
+    RecCons r rs -> go (mappend m (f r)) rs
+  {-# INLINABLE go #-}
+{-# INLINE foldMap #-}
+
+foldMap1 :: forall f m r rs. Semigroup m
+  => (forall x. f x -> m)
+  -> Rec f (r ': rs)
+  -> m
+foldMap1 f (RecCons b bs) = go (f b) bs
+  where
+  go :: forall ss. m -> Rec f ss -> m
+  go !m record = case record of
+    RecNil -> m
+    RecCons r rs -> go (m SG.<> (f r)) rs
+  {-# INLINABLE go #-}
+{-# INLINE foldMap1 #-}
+
+traverse
+  :: Applicative h
+  => (forall x. f x -> h (g x))
+  -> Rec f rs
+  -> h (Rec g rs)
+traverse _ RecNil = pure RecNil
+traverse f (RecCons x xs) = RecCons <$> f x <*> traverse f xs
+{-# INLINABLE traverse #-}
+
+traverse_
+  :: Applicative h
+  => (forall x. f x -> h b)
+  -> Rec f rs
+  -> h ()
+traverse_ _ RecNil = pure ()
+traverse_ f (RecCons x xs) = f x *> traverse_ f xs
+{-# INLINABLE traverse_ #-}
+
+get :: Elem rs r -> Rec f rs -> f r
+get ElemHere (RecCons r _) = r
+get (ElemThere ix) (RecCons _ rs) = get ix rs
+
+put :: Elem rs r -> f r -> Rec f rs -> Rec f rs
+put ElemHere r' (RecCons _ rs) = RecCons r' rs
+put (ElemThere ix) r' (RecCons r rs) = RecCons r (put ix r' rs)
+
+gets :: Rec (Elem rs) ss -> Rec f rs -> Rec f ss
+gets ixs rec = map (\e -> get e rec) ixs
+
+puts :: Rec (Elem rs) ss -> Rec f rs -> Rec f ss -> Rec f rs
+puts RecNil rs _ = rs
+puts (RecCons ix ixs) rs (RecCons s ss) = put ix s (puts ixs rs ss)
+
+append :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
+append RecNil ys = ys
+append (RecCons x xs) ys = RecCons x (append xs ys)
+
+fromSingList :: SingList as -> Rec Sing as
+fromSingList SingListNil = RecNil
+fromSingList (SingListCons r rs) = RecCons r (fromSingList rs)
+
+toSingList :: Rec Sing as -> SingList as
+toSingList RecNil = SingListNil
+toSingList (RecCons r rs) = SingListCons r (toSingList rs)
+
+fromList :: [Exists f] -> Exists (Rec f)
+fromList [] = Exists RecNil
+fromList (Exists x : xs) = case fromList xs of
+  Exists ys -> Exists (RecCons x ys)
diff --git a/src/Topaz/Types.hs b/src/Topaz/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Topaz/Types.hs
@@ -0,0 +1,276 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Topaz.Types
+  ( Elem(..)
+  , Rec(..)
+  -- , BiRec(..)
+  , NestRec(..)
+  , Fix(..)
+  , HFix(..)
+  , Nest(..)
+  , EqHetero(..)
+  , TestEqualityHetero(..)
+  , Nat(..)
+  , SingNat(..)
+  , Vector(..)
+  , type (++)
+  ) where
+
+import Control.Applicative (liftA2)
+import Data.Exists
+import Data.Foldable (foldrM)
+import Data.Hashable (Hashable(..))
+import Data.Kind (Type)
+import Data.Monoid.Lifted (Semigroup1(..), Monoid1(..), append1)
+import Data.Proxy (Proxy(..))
+import Data.Type.Coercion
+import Data.Type.Equality
+import Foreign.Ptr (castPtr,plusPtr)
+import Foreign.Storable (Storable(..))
+
+import qualified Data.Aeson as AE
+import qualified Data.Aeson.Types as AET
+import qualified Data.Semigroup as SG
+import qualified Data.Vector as V
+
+data Nat = Succ Nat | Zero
+
+data SingNat :: Nat -> Type where
+  SingZero :: SingNat 'Zero
+  SingSucc :: SingNat n -> SingNat ('Succ n)
+
+type instance Sing = SingNat
+
+data Vector :: Nat -> Type -> Type where
+  VectorNil :: Vector 'Zero a
+  VectorCons :: a -> Vector n a -> Vector ('Succ n) a
+
+instance Eq a => Eq (Vector n a) where
+  VectorNil == VectorNil = True
+  VectorCons a as == VectorCons b bs = a == b && as == bs
+
+data Elem (rs :: [k]) (r :: k) where
+  ElemHere :: Elem (r ': rs) r
+  ElemThere :: Elem rs r -> Elem (s ': rs) r
+
+type family (as :: [k]) ++ (bs :: [k]) :: [k] where
+  '[] ++ bs = bs
+  (a ': as) ++ bs = a ': (as ++ bs)
+infixr 5 ++
+
+data Rec :: forall (k :: Type). (k -> Type) -> [k] -> Type where
+  RecNil :: Rec f '[]
+  RecCons :: f r -> Rec f rs -> Rec f (r ': rs)
+
+-- data BiRec :: (k -> Type) -> (j -> Type) -> [k] -> [j] -> Type where
+--   BiRec :: Rec f ks -> Rec g js -> BiRec f g ks js
+
+data NestRec :: forall (k :: Type). (k -> Type) -> Nest k -> Type where
+  NestRec :: Rec f rs -> Rec (NestRec f) ns -> NestRec f ('Nest ns rs)
+
+data Nest a = Nest [Nest a] [a]
+newtype Fix f = Fix (f (Fix f))
+newtype HFix h a = HFix (h (HFix h) a)
+
+instance Semigroup1 f => Semigroup (Fix f) where
+  Fix a <> Fix b = Fix (append1 a b)
+
+instance Monoid1 f => Monoid (Fix f) where
+  mempty = Fix (liftEmpty mempty)
+  mappend = (SG.<>)
+
+-- Think of a better name for this typeclass
+class EqHetero h where
+  eqHetero :: (forall x. f x -> f x -> Bool) -> h f a -> h f a -> Bool
+
+instance EqHetero h => EqForall (HFix h) where
+  eqForall (HFix a) (HFix b) = eqHetero eqForall a b 
+
+instance EqHetero h => Eq (HFix h a) where
+  (==) = eqForall
+
+class TestEqualityHetero h where
+  testEqualityHetero :: (forall x y. f x -> f y -> Maybe (x :~: y)) -> h f a -> h f b -> Maybe (a :~: b)
+
+instance TestEqualityHetero h => TestEquality (HFix h) where
+  testEquality (HFix a) (HFix b) = testEqualityHetero testEquality a b
+
+instance TestEquality f => TestEquality (Rec f) where
+  testEquality RecNil RecNil = Just Refl
+  testEquality (RecCons x xs) (RecCons y ys) = do
+    Refl <- testEquality x y
+    Refl <- testEquality xs ys
+    Just Refl
+  testEquality _ _ = Nothing
+
+instance TestCoercion f => TestCoercion (Rec f) where
+  testCoercion RecNil RecNil = Just Coercion
+  testCoercion (RecCons x xs) (RecCons y ys) = do
+    Coercion <- testCoercion x y
+    Coercion <- testCoercion xs ys
+    Just Coercion
+  testCoercion _ _ = Nothing
+
+instance HashableForall f => HashableForall (Rec f) where
+  hashWithSaltForall s0 = go s0 where
+    go :: Int -> Rec f rs -> Int
+    go !s x = case x of
+      RecNil -> s
+      RecCons b bs -> go (hashWithSaltForall s b) bs
+
+instance HashableForall f => Hashable (Rec f as) where
+  hashWithSalt = hashWithSaltForall
+
+instance ShowForall f => ShowForall (Rec f) where
+  showsPrecForall p x = case x of
+    RecCons v vs -> showParen (p > 10)
+      $ showString "RecCons "
+      . showsPrecForall 11 v
+      . showString " "
+      . showsPrecForall 11 vs
+    RecNil -> showString "RecNil"
+
+instance ShowForall f => Show (Rec f as) where
+  showsPrec = showsPrecForall
+
+instance ShowForeach f => ShowForeach (Rec f) where
+  showsPrecForeach SingListNil _ RecNil = showString "RecNil"
+  showsPrecForeach (SingListCons s ss) p (RecCons v vs) = showParen (p > 10)
+    $ showString "RecCons "
+    . showsPrecForeach s 11 v
+    . showString " "
+    . showsPrecForeach ss 11 vs
+
+instance EqForall f => Eq (Rec f as) where
+  (==) = eqForall
+
+instance EqForall f => EqForall (Rec f) where
+  eqForall RecNil RecNil = True
+  eqForall (RecCons a as) (RecCons b bs) =
+    eqForall a b && eqForall as bs
+
+instance EqForeach f => EqForeach (Rec f) where
+  eqForeach SingListNil RecNil RecNil = True
+  eqForeach (SingListCons s ss) (RecCons a as) (RecCons b bs) =
+    eqForeach s a b && eqForeach ss as bs
+
+instance EqForallPoly f => EqForallPoly (Rec f) where
+  eqForallPoly RecNil RecNil = WitnessedEqualityEqual
+  eqForallPoly RecNil (RecCons _ _) = WitnessedEqualityUnequal
+  eqForallPoly (RecCons _ _) RecNil = WitnessedEqualityUnequal
+  eqForallPoly (RecCons x xs) (RecCons y ys) = case eqForallPoly x y of
+    WitnessedEqualityUnequal -> WitnessedEqualityUnequal
+    WitnessedEqualityEqual -> case eqForallPoly xs ys of
+      WitnessedEqualityUnequal -> WitnessedEqualityUnequal
+      WitnessedEqualityEqual -> WitnessedEqualityEqual
+
+instance OrdForall f => Ord (Rec f as) where
+  compare = compareForall
+
+instance OrdForall f => OrdForall (Rec f) where
+  compareForall RecNil RecNil = EQ
+  compareForall (RecCons a as) (RecCons b bs) =
+    mappend (compareForall a b) (compareForall as bs)
+
+instance OrdForeach f => OrdForeach (Rec f) where
+  compareForeach SingListNil RecNil RecNil = EQ
+  compareForeach (SingListCons s ss) (RecCons a as) (RecCons b bs) =
+    mappend (compareForeach s a b) (compareForeach ss as bs)
+
+
+instance SemigroupForall f => Semigroup (Rec f as) where
+  (<>) = recZipWith appendForall
+
+instance SemigroupForeach f => SemigroupForeach (Rec f) where
+  appendForeach SingListNil RecNil RecNil = RecNil
+  appendForeach (SingListCons s ss) (RecCons x xs) (RecCons y ys) =
+    RecCons (appendForeach s x y) (appendForeach ss xs ys)
+
+instance MonoidForeach f => MonoidForeach (Rec f) where
+  emptyForeach SingListNil = RecNil
+  emptyForeach (SingListCons s ss) = RecCons (emptyForeach s) (emptyForeach ss)
+
+instance SemigroupForall f => SemigroupForall (Rec f) where
+  appendForall = recZipWith appendForall
+
+instance ToJSONForall f => AE.ToJSON (Rec f as) where
+  toJSON = toJSONForall
+
+instance ToJSONForall f => ToJSONForall (Rec f) where
+  toJSONForall = AE.toJSON . go
+    where
+    go :: forall g xs. ToJSONForall g => Rec g xs -> [AE.Value]
+    go RecNil = []
+    go (RecCons x xs) = toJSONForall x : go xs
+
+instance (FromJSONForeach f, Reify as) => AE.FromJSON (Rec f as) where
+  parseJSON = parseJSONForeach reify
+
+instance FromJSONForeach f => FromJSONForeach (Rec f) where
+  parseJSONForeach s0 = AE.withArray "Rec" $ \vs -> do
+    let go :: SingList as -> Int -> AET.Parser (Rec f as)
+        go SingListNil !ix = if V.length vs == ix
+          then return RecNil
+          else fail "too many elements in array"
+        go (SingListCons s ss) !ix = if ix < V.length vs
+          then do
+            r <- parseJSONForeach s (vs V.! ix)
+            rs <- go ss (ix + 1)
+            return (RecCons r rs)
+          else fail "not enough elements in array"
+    go s0 0
+
+instance StorableForeach f => StorableForeach (Rec f) where
+  sizeOfForeach _ SingListNil = 0
+  sizeOfForeach _ (SingListCons s ss) =
+    sizeOfForeach (Proxy :: Proxy f) s + sizeOfForeach (Proxy :: Proxy (Rec f)) ss
+  peekForeach SingListNil _ = return RecNil
+  peekForeach (SingListCons s ss) ptr = do
+    r <- peekForeach s (castPtr ptr)
+    rs <- peekForeach ss (plusPtr ptr (sizeOfForeach (Proxy :: Proxy f) s))
+    return (RecCons r rs)
+  pokeForeach _ _ RecNil = return ()
+  pokeForeach (SingListCons s ss) ptr (RecCons r rs) = do
+    pokeForeach s (castPtr ptr) r
+    pokeForeach ss (plusPtr ptr (sizeOfForeach (Proxy :: Proxy f) s)) rs
+
+instance (StorableForeach f, Reify as) => Storable (Rec f as) where
+  sizeOf _ = sizeOfForeach (Proxy :: Proxy (Rec f)) (reify :: SingList as)
+  alignment _ = sizeOf (undefined :: Rec f as)
+  poke = pokeForeach (reify :: SingList as)
+  peek = peekForeach (reify :: SingList as)
+
+instance BinaryForeach f => BinaryForeach (Rec f) where
+  putForeach SingListNil RecNil = return ()
+  putForeach (SingListCons s ss) (RecCons r rs) = do
+    putForeach s r
+    putForeach ss rs
+  getForeach SingListNil = return RecNil
+  getForeach (SingListCons s ss) =
+    liftA2 RecCons (getForeach s) (getForeach ss)
+
+instance FromJSONExists f => FromJSONExists (Rec f) where
+  parseJSONExists = AE.withArray "Rec" $ \vs -> 
+    foldrM go (Exists RecNil) vs
+    where
+    go :: forall g. FromJSONExists g => AE.Value -> Exists (Rec g) -> AET.Parser (Exists (Rec g))
+    go v (Exists rs) = do
+      Exists r <- parseJSONExists v :: AET.Parser (Exists g)
+      return (Exists (RecCons r rs))
+
+recZipWith :: (forall x. f x -> g x -> h x) -> Rec f rs -> Rec g rs -> Rec h rs
+recZipWith _ RecNil RecNil = RecNil
+recZipWith f (RecCons a as) (RecCons b bs) =
+  RecCons (f a b) (recZipWith f as bs)
+
diff --git a/topaz.cabal b/topaz.cabal
new file mode 100644
--- /dev/null
+++ b/topaz.cabal
@@ -0,0 +1,32 @@
+cabal-version: 2.4
+name: topaz
+version: 0.6.0
+synopsis: Extensible records library
+description: Provides extensible records types built on top of the quantification library
+homepage: https://github.com/andrewthad/quantification#readme
+license: BSD-3-Clause
+license-file: LICENSE
+author: Andrew Martin
+maintainer: andrew.thaddeus@gmail.com
+copyright: 2018 Andrew Martin
+category: Web
+build-type: Simple
+
+library
+  hs-source-dirs: src
+  exposed-modules:
+    Topaz.Rec
+    Topaz.Types
+  build-depends:
+    , base >= 4.11.1 && < 5
+    , binary >= 0.8 && < 0.11
+    , hashable >= 1.2 && < 1.4
+    , aeson >= 1.0 && < 1.6
+    , vector >= 0.11 && < 0.13
+    , quantification >= 0.6.0
+  default-language: Haskell2010
+  ghc-options: -O2 -Wall
+
+source-repository head
+  type:     git
+  location: https://github.com/andrewthad/quantification