diff --git a/quantification.cabal b/quantification.cabal
--- a/quantification.cabal
+++ b/quantification.cabal
@@ -1,10 +1,10 @@
-cabal-version: 2.0
+cabal-version: 2.4
 name: quantification
-version: 0.5.2
+version: 0.6.0
 synopsis: Rage against the quantification
 description: Data types and typeclasses to deal with universally and existentially quantified types
 homepage: https://github.com/andrewthad/quantification#readme
-license: BSD3
+license: BSD-3-Clause
 license-file: LICENSE
 author: Andrew Martin
 maintainer: andrew.thaddeus@gmail.com
@@ -18,14 +18,11 @@
     Data.Binary.Lifted
     Data.Exists
     Data.Monoid.Lifted
-    Topaz.Rec
-    Topaz.Types
   build-depends:
-      base >= 4.11.1 && < 5
-    , binary >= 0.8 && < 0.10
-    , ghc-prim >= 0.5 && < 0.7
+    , base >= 4.11.1 && < 5
+    , binary >= 0.8 && < 0.11
     , hashable >= 1.2 && < 1.4
-    , aeson >= 1.0 && < 1.5
+    , aeson >= 1.0 && < 1.6
     , text >= 1.0 && < 2.0
     , path-pieces >= 0.2 && < 0.3
     , vector >= 0.11 && < 0.13
diff --git a/src/Topaz/Rec.hs b/src/Topaz/Rec.hs
deleted file mode 100644
--- a/src/Topaz/Rec.hs
+++ /dev/null
@@ -1,144 +0,0 @@
-{-# 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
deleted file mode 100644
--- a/src/Topaz/Types.hs
+++ /dev/null
@@ -1,276 +0,0 @@
-{-# 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 :: (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 :: (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)
-