diff --git a/Data/Vinyl.hs b/Data/Vinyl.hs
--- a/Data/Vinyl.hs
+++ b/Data/Vinyl.hs
@@ -1,16 +1,16 @@
 module Data.Vinyl
-  ( module Data.Vinyl.Lens
+  ( module Data.Vinyl.Core
+  , module Data.Vinyl.Derived
+  , module Data.Vinyl.Operators
+  , module Data.Vinyl.Lens
   , module Data.Vinyl.Witnesses
-  , module Data.Vinyl.Field
-  , module Data.Vinyl.Rec
-  , module Data.Vinyl.Relation
-  , module Data.Vinyl.Classes
+  , module Data.Vinyl.Constraint
   ) where
 
-import           Data.Vinyl.Classes
-import           Data.Vinyl.Field
-import           Data.Vinyl.Lens
-import           Data.Vinyl.Rec
-import           Data.Vinyl.Relation
-import           Data.Vinyl.Witnesses
+import Data.Vinyl.Core
+import Data.Vinyl.Derived
+import Data.Vinyl.Operators
+import Data.Vinyl.Lens
+import Data.Vinyl.Constraint
+import Data.Vinyl.Witnesses
 
diff --git a/Data/Vinyl/Classes.hs b/Data/Vinyl/Classes.hs
deleted file mode 100644
--- a/Data/Vinyl/Classes.hs
+++ /dev/null
@@ -1,26 +0,0 @@
-{-# LANGUAGE KindSignatures        #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PolyKinds             #-}
-{-# LANGUAGE TypeOperators         #-}
-
-module Data.Vinyl.Classes where
-
-import Control.Applicative
-import Data.Vinyl.Idiom.Identity
-
--- | This class is a generalized, but non-pointed version of 'Applicative'. This
--- is useful for types which range over functors rather than sets.
-class Apply (arr :: k -> k -> k) (f :: k -> *) where
-  (<<*>>) :: f (arr a b) -> f a -> f b
-
--- | To accumulate effects distributed over a data type, you 'dist' it.
-class Dist t where
-  dist :: Applicative f => t f -> f (t Identity)
-
--- | If a record is homogenous, you can fold over it.
-class FoldRec r a where
-  foldRec :: (a -> b -> b) -> b -> r -> b
-
--- | '(~>)' is a morphism between functors.
-newtype (f ~> g) x = NT { runNT :: f x -> g x }
-
diff --git a/Data/Vinyl/Constraint.hs b/Data/Vinyl/Constraint.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Constraint.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+
+module Data.Vinyl.Constraint
+  ( (<:)(..)
+  , (:~:)
+  , (~=)
+  , RecAll
+  ) where
+
+import Data.Vinyl.Core
+import Data.Vinyl.Witnesses
+import Data.Vinyl.TyFun
+import GHC.Prim (Constraint)
+
+-- | One record is a subtype of another if the fields of the latter are a
+-- subset of the fields of the former.
+class (xs :: [k]) <: (ys :: [k]) where
+  cast :: Rec el f xs -> Rec el f ys
+
+instance xs <: '[] where
+  cast _ = RNil
+
+instance (y ∈ xs, xs <: ys) => xs <: (y ': ys) where
+  cast xs = ith (implicitly :: Elem y xs) xs :& cast xs
+    where
+      ith :: Elem r rs -> Rec el f rs -> f (el $ r)
+      ith Here (a :& _) = a
+      ith (There p) (_ :& as) = ith p as
+
+-- | If two records types are subtypes of each other, that means that they
+-- differ only in order of fields.
+type r1 :~: r2 = (r1 <: r2, r2 <: r1)
+
+-- | Term-level record congruence.
+(~=) :: (Eq (Rec el f xs), xs :~: ys) => Rec el f xs -> Rec el f ys -> Bool
+x ~= y = x == (cast y)
+
+type family RecAll (el :: TyFun k l -> *) (f :: * -> *) (rs :: [k]) (c :: * -> Constraint) :: Constraint
+type instance RecAll el f '[] c = ()
+type instance RecAll el f (r ': rs) c = (c (f (el $ r)), RecAll el f rs c)
+
diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Core.hs
@@ -0,0 +1,80 @@
+{-# LANGUAGE BangPatterns        #-}
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE PolyKinds           #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE TypeOperators       #-}
+
+module Data.Vinyl.Core where
+
+import Data.Vinyl.TyFun
+import Control.Applicative
+import Data.Monoid
+import Data.Vinyl.Idiom.Identity
+import Foreign.Ptr (castPtr, plusPtr)
+import Foreign.Storable (Storable(..))
+
+-- | A record is parameterized by a universe @u@, list of rows @rs@, a large
+-- elimination @el@, and a type constructor @f@ to be applied to the
+-- interpretation @el r@ of each of those @r@.
+data Rec :: (TyFun u * -> *) -> (* -> *) -> [u] -> * where
+  RNil :: Rec el f '[]
+  (:&) :: !(f (el $ r)) -> !(Rec el f rs) -> Rec el f (r ': rs)
+infixr :&
+
+-- | Shorthand for a record with a single field. Lifts the field's
+-- value into the chosen functor automatically.
+(=:) :: Applicative f => sing k -> el $ k -> Rec el f '[ k ]
+_ =: x = pure x :& RNil
+
+-- | Shorthand for a record with a single field. This is useful for
+-- @Applicative@ or @Monad@ic intialization of records as in the idiom:
+--
+-- > dist $ myField <-: someIO <+> yourField <-: otherIO
+(<-:) :: sing r -> f (el $ r) -> Rec el f '[r]
+_ <-: x = x :& RNil
+infixr 6 <-:
+
+-- | Records constructed using the above combinators will often be polymorphic
+-- in their interpreter @el@. To avoid providing a type annotation, one can
+-- provide their interpreters with a singleton tag and pass that in.
+withUniverse :: (forall x. el x) -> Rec el f rs -> Rec el f rs
+withUniverse _ x = x
+{-# INLINE withUniverse #-}
+
+instance Monoid (Rec el f '[]) where
+  mempty = RNil
+  RNil `mappend` RNil = RNil
+
+instance (Monoid (el $ r), Monoid (Rec el f rs), Applicative f) => Monoid (Rec el f (r ': rs)) where
+  mempty = pure mempty :& mempty
+  (x :& xs) `mappend` (y :& ys) = liftA2 mappend x y :& (xs `mappend` ys)
+
+instance Eq (Rec el f '[]) where
+  _ == _ = True
+instance (Eq (f (el $ r)), Eq (Rec el f rs)) => Eq (Rec el f (r ': rs)) where
+  (x :& xs) == (y :& ys) = (x == y) && (xs == ys)
+
+instance Storable (Rec el Identity '[]) where
+  sizeOf _    = 0
+  alignment _ = 0
+  peek _      = return RNil
+  poke _ RNil = return ()
+
+instance (Storable (el $ r), Storable (Rec el Identity rs)) => Storable (Rec el Identity (r ': rs)) where
+  sizeOf _ = sizeOf (undefined :: el $ r) + sizeOf (undefined :: Rec el Identity rs)
+  {-# INLINABLE sizeOf #-}
+  alignment _ =  alignment (undefined :: el $ r)
+  {-# INLINABLE alignment #-}
+  peek ptr = do !x <- peek (castPtr ptr)
+                !xs <- peek (ptr `plusPtr` sizeOf (undefined :: el $ r))
+                return $ Identity x :& xs
+  {-# INLINABLE peek #-}
+  poke ptr (Identity !x :& xs) = poke (castPtr ptr) x >>
+                                 poke (ptr `plusPtr` sizeOf (undefined :: el $ r)) xs
+  {-# INLINEABLE poke #-}
+
diff --git a/Data/Vinyl/Field.hs b/Data/Vinyl/Field.hs
deleted file mode 100644
--- a/Data/Vinyl/Field.hs
+++ /dev/null
@@ -1,26 +0,0 @@
-{-# LANGUAGE CPP                 #-}
-{-# LANGUAGE DataKinds           #-}
-{-# LANGUAGE GADTs               #-}
-{-# LANGUAGE KindSignatures      #-}
-{-# LANGUAGE PolyKinds           #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeOperators       #-}
-
-module Data.Vinyl.Field where
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-import           Data.Proxy
-#endif
-import           GHC.TypeLits
-
--- | A field contains a key and a type.
-data (:::) :: Symbol -> * -> * where
-  Field :: sy ::: t
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-instance KnownSymbol sy => Show (sy ::: t) where
-  show Field = symbolVal (Proxy :: Proxy sy)
-#else
-instance SingI sy => Show (sy ::: t) where
-  show Field = fromSing (sing :: Sing sy)
-#endif
diff --git a/Data/Vinyl/Functor.hs b/Data/Vinyl/Functor.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Functor.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE FlexibleInstances #-}
+
+module Data.Vinyl.Functor where
+
+import Control.Applicative
+
+class Presheaf f where
+  contramap :: (a -> b) -> (f b -> f a)
+
+newtype Lift op f g x = Lift { runLift :: op (f x) (g x) }
+
+instance (Functor f, Functor g) => Functor (Lift (,) f g) where
+  fmap f (Lift (x, y)) = Lift (fmap f x, fmap f y)
+
+instance (Functor f, Functor g) => Functor (Lift Either f g) where
+  fmap f (Lift (Left x)) = Lift . Left . fmap f $ x
+  fmap f (Lift (Right x)) = Lift . Right . fmap f $ x
+
+instance (Presheaf f, Presheaf g) => Presheaf (Lift (,) f g) where
+  contramap f (Lift (x, y)) = Lift (contramap f x, contramap f y)
+
+instance (Presheaf f, Presheaf g) => Presheaf (Lift Either f g) where
+  contramap f (Lift (Left x)) = Lift . Left . contramap f $ x
+  contramap f (Lift (Right x)) = Lift . Right . contramap f $ x
+
+instance (Applicative f, Applicative g) => Applicative (Lift (,) f g) where
+  pure x = Lift (pure x, pure x)
+  Lift (f, g) <*> Lift (x, y) = Lift (f <*> x, g <*> y)
+
+instance (Presheaf f, Functor g) => Functor (Lift (->) f g) where
+  fmap f (Lift ηx) = Lift $ fmap f . ηx . contramap f
+
+instance (Functor f, Presheaf g) => Presheaf (Lift (->) f g) where
+  contramap f (Lift ηx) = Lift $ contramap f . ηx . fmap f
+
diff --git a/Data/Vinyl/Idiom/LazyIdentity.hs b/Data/Vinyl/Idiom/LazyIdentity.hs
deleted file mode 100644
--- a/Data/Vinyl/Idiom/LazyIdentity.hs
+++ /dev/null
@@ -1,25 +0,0 @@
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveTraversable #-}
-
-module Data.Vinyl.Idiom.LazyIdentity where
-
-import Control.Applicative
-import Data.Foldable
-import Data.Traversable
-
-data LazyIdentity a
-  = LazyIdentity
-  { runLazyIdentity :: a
-  } deriving (Functor, Foldable, Traversable)
-
-instance Applicative LazyIdentity where
-  pure = LazyIdentity
-  (LazyIdentity f) <*> (LazyIdentity x) = LazyIdentity (f x)
-
-instance Monad LazyIdentity where
-  return = LazyIdentity
-  (LazyIdentity x) >>= f = f x
-
-instance Show a => Show (LazyIdentity a) where
-  show (LazyIdentity x) = show x
diff --git a/Data/Vinyl/Idiom/Thunk.hs b/Data/Vinyl/Idiom/Thunk.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Idiom/Thunk.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
+
+module Data.Vinyl.Idiom.Thunk where
+
+import Control.Applicative
+import Data.Foldable
+import Data.Traversable
+
+data Thunk a
+  = Thunk
+  { runThunk :: a
+  } deriving (Functor, Foldable, Traversable)
+
+instance Applicative Thunk where
+  pure = Thunk
+  (Thunk f) <*> (Thunk x) = Thunk (f x)
+
+instance Monad Thunk where
+  return = Thunk
+  (Thunk x) >>= f = f x
+
+instance Show a => Show (Thunk a) where
+  show (Thunk x) = show x
diff --git a/Data/Vinyl/Idiom/Validation.hs b/Data/Vinyl/Idiom/Validation.hs
--- a/Data/Vinyl/Idiom/Validation.hs
+++ b/Data/Vinyl/Idiom/Validation.hs
@@ -2,10 +2,11 @@
 
 module Data.Vinyl.Idiom.Validation where
 
+import Data.Vinyl.Idiom.Identity
+import Data.Vinyl.Functor
+
 import Control.Applicative
 import Data.Monoid
-import Data.Vinyl.Classes
-import Data.Vinyl.Idiom.Identity
 
 -- | A type which is similar to 'Either', except that it has a
 -- slightly different Applicative instance.
@@ -15,17 +16,17 @@
   deriving (Show, Eq)
 
 -- | Validators transform identities into results.
-type Validator e = Identity ~> Result e
+type Validator e = Lift (->) Identity (Result e)
 
 instance Functor (Result e) where
   fmap f (Success x) = Success $ f x
-  fmap f (Failure e) = Failure e
+  fmap _ (Failure e) = Failure e
 
 -- | The 'Applicative' instance to 'Result' relies on its error type
 -- being a 'Monoid'. That way, it can accumulate errors.
 instance Monoid e => Applicative (Result e) where
   pure = Success
   (Success f) <*> (Success x)  = Success $ f x
-  (Failure e) <*> (Success x)  = Failure e
-  (Success f) <*> (Failure e)  = Failure e
+  (Failure e) <*> (Success _)  = Failure e
+  (Success _) <*> (Failure e)  = Failure e
   (Failure e) <*> (Failure e') = Failure $ e <> e'
diff --git a/Data/Vinyl/Lens.hs b/Data/Vinyl/Lens.hs
--- a/Data/Vinyl/Lens.hs
+++ b/Data/Vinyl/Lens.hs
@@ -1,40 +1,44 @@
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE TypeOperators         #-}
+
 -- | A small, /en passant/ lens implementation to provide accessors
 -- for record fields. Lenses produced with 'rLens' are fully
 -- compatible with the @lens@ package.
 module Data.Vinyl.Lens where
-import Control.Applicative
-import Data.Vinyl.Idiom.Identity
-import Data.Vinyl.Field
-import Data.Vinyl.Rec
+
+import Data.Vinyl.Core
+import Data.Vinyl.Derived
+import Data.Vinyl.TyFun
 import Data.Vinyl.Witnesses
+import Data.Vinyl.Idiom.Identity
 
+import Control.Applicative
+
 -- | Project a field from a 'Rec'.
-rGet' :: IElem (sy ::: t) rs => (sy ::: t) -> Rec rs f -> f t
+rGet' :: (r ∈ rs) => sing r -> Rec el f rs -> f (el $ r)
 rGet' r = getConst . rLens' r Const
 {-# INLINE rGet' #-}
 
 -- | Project a field from a 'PlainRec'.
-rGet :: IElem (sy ::: t) rs => (sy ::: t) -> PlainRec rs -> t
+rGet :: (r ∈ rs) => sing r -> PlainRec el rs -> el $ r
 rGet = (runIdentity .) . rGet'
 {-# INLINE rGet #-}
 
 -- | Set a field in a 'Rec' over an arbitrary functor.
-rPut' :: IElem (sy ::: t) rs => (sy ::: t) -> f t -> Rec rs f -> Rec rs f
+rPut' :: (r ∈ rs) => sing r -> f (el $ r) -> Rec el f rs -> Rec el f rs
 rPut' r x = runIdentity . rLens' r (Identity . const x)
 {-# INLINE rPut' #-}
 
 -- | Set a field in a 'PlainRec'.
-rPut :: IElem (sy:::t) rs => (sy:::t) -> t -> PlainRec rs -> PlainRec rs
+rPut :: (r ∈ rs) => sing r -> el $ r -> PlainRec el rs -> PlainRec el rs
 rPut r x = rPut' r (Identity x)
 {-# INLINE rPut #-}
 
 -- | Modify a field.
-rMod :: (IElem (sy:::t) rs, Functor f)
-     => (sy:::t) -> (t -> t) -> Rec rs f -> Rec rs f
+rMod :: (r ∈ rs , Functor f) => sing r -> (el $ r -> el $ r) -> Rec el f rs -> Rec el f rs
 rMod r f = runIdentity . rLens' r (Identity . fmap f)
 {-# INLINE rMod #-}
 
@@ -45,11 +49,10 @@
 -- does not support polymorphic update. In the parlance of the @lens@
 -- package,
 --
--- > rLens' :: IElem (sy:::t) rs => (sy:::t) -> Lens' (Rec rs f) (f t)
-rLens' :: forall r rs sy t f g. (r ~ (sy:::t), IElem r rs, Functor g)
-       => r -> (f t -> g (f t)) -> Rec rs f -> g (Rec rs f)
+-- > rLens' :: (r ∈ rs) => Sing r -> Lens' (Rec el f rs) (f (el $ r))
+rLens' :: forall r rs f g el sing. (r ∈ rs , Functor g) => sing r -> (f (el $ r) -> g (f (el $ r))) -> Rec el f rs -> g (Rec el f rs)
 rLens' _ f = go implicitly
-  where go :: Elem r rr -> Rec rr f -> g (Rec rr f)
+  where go :: Elem r rr -> Rec el f rr -> g (Rec el f rr)
         go Here (x :& xs) = fmap (:& xs) (f x)
         go (There Here) (a :& x :& xs) = fmap ((a :&) . (:& xs)) (f x)
         go (There (There Here)) (a :& b :& x :& xs) =
@@ -62,7 +65,7 @@
           fmap (\xs' -> a :& b :& c :& d :& xs') (go' p xs)
         {-# INLINE go #-}
 
-        go' :: Elem r rr -> Rec rr f -> g (Rec rr f)
+        go' :: Elem r rr -> Rec el f rr -> g (Rec el f rr)
         go' Here (x :& xs) = fmap (:& xs) (f x)
         go' (There p) (x :& xs) = fmap (x :&) (go p xs)
         {-# INLINABLE go' #-}
@@ -72,9 +75,8 @@
 -- from the @lens@ package. Note that polymorphic update is not
 -- supported. In the parlance of the @lens@ package,
 --
--- > rLens :: IElem (sy:::t) rs => (sy:::t) -> Lens' (PlainRec rs) t
-rLens :: forall r rs sy t g. (r ~ (sy:::t), IElem r rs, Functor g)
-      => r -> (t -> g t) -> PlainRec rs -> g (PlainRec rs)
+-- > rLens :: (r ∈ rs) => sing r -> Lens' (PlainRec el rs) (el $ r)
+rLens :: forall r rs g el sing. (r ∈ rs , Functor g) => sing r -> (el $ r -> g (el $ r)) -> PlainRec el rs -> g (PlainRec el rs)
 rLens r = rLens' r . lenser runIdentity (const Identity)
   where lenser sa sbt afb s = sbt s <$> afb (sa s)
 {-# INLINE rLens #-}
diff --git a/Data/Vinyl/Operators.hs b/Data/Vinyl/Operators.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Operators.hs
@@ -0,0 +1,99 @@
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+
+module Data.Vinyl.Operators
+  ( (<<$>>)
+  , (<<*>>)
+  , (<+>)
+  , rpure
+  , rtraverse
+  , rdist
+  , rdistLazy
+  , foldRec
+  , recToList
+  , showWithNames
+  , rshow
+  ) where
+
+import Data.Vinyl.Core
+import Data.Vinyl.Functor
+import Data.Vinyl.TyFun
+import Data.Vinyl.Witnesses
+import Data.Vinyl.Constraint
+import Data.Vinyl.Derived
+import qualified Data.Vinyl.Idiom.Identity as I
+import qualified Data.Vinyl.Idiom.Thunk as I
+import qualified Data.Vinyl.Universe.Const as U
+
+import Control.Applicative
+import qualified Data.List as L (intercalate)
+
+-- | Append for records.
+(<+>) :: Rec el f as -> Rec el f bs -> Rec el f (as ++ bs)
+RNil      <+> xs = xs
+(x :& xs) <+> ys =  x :& (xs <+> ys)
+infixr 5  <+>
+
+-- | Append for type-level lists.
+type family (as :: [k]) ++ (bs :: [k]) :: [k]
+type instance '[] ++ bs = bs
+type instance (a ': as) ++ bs  = a ': (as ++ bs)
+
+(<<$>>) :: (forall x. f x -> g x) -> Rec el f rs -> Rec el g rs
+_   <<$>> RNil    = RNil
+eta <<$>> x :& xs = eta x :& (eta <<$>> xs)
+infixl 8 <<$>>
+{-# INLINE (<<$>>) #-}
+
+(<<*>>) :: Rec el (Lift (->) f g) rs -> Rec el f rs -> Rec el g rs
+RNil    <<*>> RNil    = RNil
+f :& fs <<*>> x :& xs = runLift f x :& (fs <<*>> xs)
+infixl 8 <<*>>
+{-# INLINE (<<*>>) #-}
+
+class RecApplicative rs where
+  rpure :: (forall x. f x) -> Rec el f rs
+instance RecApplicative '[] where
+  rpure _ = RNil
+instance RecApplicative rs => RecApplicative (f ': rs) where
+  rpure s = s :& rpure s
+
+class FoldRec r a where
+  foldRec :: (a -> b -> b) -> b -> r -> b
+instance FoldRec (Rec el f '[]) a where
+  foldRec _ z RNil = z
+instance (t ~ (el $ r), FoldRec (Rec el f rs) (f t)) => FoldRec (Rec el f (r ': rs)) (f t) where
+  foldRec f z (x :& xs) = f x (foldRec f z xs)
+
+-- | Accumulates a homogenous record into a list
+recToList :: FoldRec (Rec el f rs) (f t) => Rec el f rs -> [f t]
+recToList = foldRec (\e a -> [e] ++ a) []
+
+rtraverse :: Applicative h => (forall x. f x -> h (g x)) -> Rec el f rs -> h (Rec el g rs)
+rtraverse _ RNil      = pure RNil
+rtraverse f (x :& xs) = (:&) <$> f x <*> rtraverse f xs
+
+rdist :: Applicative f => Rec el f rs -> f (PlainRec el rs)
+rdist = rtraverse $ fmap I.Identity
+
+rdistLazy :: Applicative f => Rec el f rs -> f (LazyPlainRec el rs)
+rdistLazy = rtraverse $ fmap I.Thunk
+
+showWithNames :: RecAll el f rs Show => PlainRec (U.Const String) rs -> Rec el f rs -> String
+showWithNames names rec = "{ " ++ L.intercalate ", " (go names rec []) ++ " }"
+  where
+    go :: RecAll el f rs Show => PlainRec (U.Const String) rs -> Rec el f rs -> [String] -> [String]
+    go RNil RNil ss = ss
+    go (I.Identity n :& ns) (x :& xs) ss = (n ++ " =: " ++ show x) : go ns xs ss
+
+rshow :: (Implicit (PlainRec (U.Const String) rs), RecAll el f rs Show) => Rec el f rs -> String
+rshow = showWithNames implicitly
+
diff --git a/Data/Vinyl/Rec.hs b/Data/Vinyl/Rec.hs
deleted file mode 100644
--- a/Data/Vinyl/Rec.hs
+++ /dev/null
@@ -1,146 +0,0 @@
-{-# LANGUAGE BangPatterns              #-}
-{-# LANGUAGE CPP                       #-}
-{-# LANGUAGE ConstraintKinds           #-}
-{-# LANGUAGE DataKinds                 #-}
-{-# LANGUAGE FlexibleContexts          #-}
-{-# LANGUAGE FlexibleInstances         #-}
-{-# LANGUAGE GADTs                     #-}
-{-# LANGUAGE InstanceSigs              #-}
-{-# LANGUAGE KindSignatures            #-}
-{-# LANGUAGE MultiParamTypeClasses     #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE PolyKinds                 #-}
-{-# LANGUAGE RankNTypes                #-}
-{-# LANGUAGE ScopedTypeVariables       #-}
-{-# LANGUAGE TypeFamilies              #-}
-{-# LANGUAGE TypeOperators             #-}
-
-module Data.Vinyl.Rec
-  ( Rec(..)
-  , PlainRec
-  , LazyPlainRec
-  , (=:)
-  , (<+>)
-  , (<-:)
-  , type (++)
-  , fixRecord
-  ) where
-
-import Data.Vinyl.Classes
-import Control.Applicative
-import Data.Vinyl.Idiom.Identity
-import Data.Vinyl.Idiom.LazyIdentity
-import Data.Vinyl.Field
-import Foreign.Ptr (castPtr, plusPtr)
-import Foreign.Storable (Storable(..))
-import GHC.TypeLits
-import Data.Monoid
-
--- | A record is parameterized by a list of fields and a functor
--- to be applied to each of those fields.
-data Rec :: [*] -> (* -> *) -> * where
-  RNil :: Rec '[] f
-  (:&) :: !(f t) -> !(Rec rs f) -> Rec ((sy ::: t) ': rs) f
-infixr :&
-
--- | Fixes a polymorphic record into the 'Identity' functor.
-fixRecord :: (forall f. Applicative f => Rec rs f) -> PlainRec rs
-fixRecord xs = xs
-
-fixRecordLazy :: (forall f. Applicative f => Rec rs f) -> LazyPlainRec rs
-fixRecordLazy xs = xs
-
--- | Fields of plain records are in the 'Identity' functor.
-type PlainRec rs = Rec rs Identity
-type LazyPlainRec rs = Rec rs LazyIdentity
-
--- | Append for records.
-(<+>) :: Rec as f -> Rec bs f -> Rec (as ++ bs) f
-RNil      <+> xs = xs
-(x :& xs) <+> ys =  x :& (xs <+> ys)
-infixr 5  <+>
-
--- | Shorthand for a record with a single field. Lifts the field's
--- value into the chosen functor automatically.
-(=:) :: Applicative f => sy ::: t -> t -> Rec '[sy ::: t] f
-_ =: b = pure b :& RNil
-
--- | Shorthand for a record with a single field of an 'Applicative'
--- type. This is useful for @Applicative@ or @Monad@ic intialization
--- of records as in the idiom:
---
--- > dist $ myField <-: someIO <+> yourField <-: otherIO
-(<-:) :: Applicative f => sy ::: t -> f t -> Rec '[sy ::: t] f
-_ <-: b = b :& RNil
-infixr 6 <-:
-
--- | Append for type-level lists.
-type family (as :: [*]) ++ (bs :: [*]) :: [*]
-type instance '[] ++ bs = bs
-type instance (a ': as) ++ bs  = a ': (as ++ bs)
-
-
-instance Show (Rec '[] f) where
-  show RNil = "{}"
-instance (
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-    KnownSymbol sy,
-#else
-    SingI sy,
-#endif
-    Show (g t), Show (Rec fs g)) => Show (Rec ((sy ::: t) ': fs) g) where
-  show (x :& xs) = show (Field :: sy ::: t) ++ " :=: " ++ show x ++ ", " ++ show xs
-
-
-instance Eq (Rec '[] f) where
-  _ == _ = True
-instance (Eq (g t), Eq (Rec fs g)) => Eq (Rec ((s ::: t) ': fs) g) where
-  (x :& xs) == (y :& ys) = (x == y) && (xs == ys)
-
-
-instance Monoid (Rec '[] f) where
-  mempty = RNil
-  RNil `mappend` RNil = RNil
-instance (Monoid t, Monoid (Rec fs g), Applicative g) => Monoid (Rec ((s ::: t) ': fs) g) where
-  mempty = pure mempty :& mempty
-  (x :& xs) `mappend` (y :& ys) = liftA2 mappend x y :& (xs `mappend` ys)
-
-
--- | Records can be applied to each other.
-instance Apply (~>) (Rec rs) where
-  RNil <<*>> RNil = RNil
-  (f :& fs) <<*>> (x :& xs) = runNT f x :& (fs <<*>> xs)
-
--- | Records may be distributed to accumulate the effects of their fields.
-instance Dist (Rec rs) where
-  dist RNil      = pure RNil
-  dist (x :& xs) = (:&) <$> (pure <$> x) <*> dist xs
-
-instance FoldRec (Rec '[] f) a where
-  foldRec _ z RNil = z
-
-instance FoldRec (Rec fs g) (g t) => FoldRec (Rec ((s ::: t) ': fs) g) (g t) where
-  foldRec f z (x :& xs) = f x (foldRec f z xs)
-
--- | Accumulates a homogenous record into a list
-recToList :: FoldRec (Rec fs g) (g t) => Rec fs g -> [g t]
-recToList = foldRec (\e a -> [e] ++ a) []
-
-instance Storable (PlainRec '[]) where
-  sizeOf _    = 0
-  alignment _ = 0
-  peek _      = return RNil
-  poke _ RNil = return ()
-
-instance (Storable t, Storable (PlainRec rs)) => Storable (PlainRec ((sy:::t) ': rs)) where
-  sizeOf _ = sizeOf (undefined :: t) + sizeOf (undefined :: PlainRec rs)
-  {-# INLINABLE sizeOf #-}
-  alignment _ =  alignment (undefined :: t)
-  {-# INLINABLE alignment #-}
-  peek ptr = do !x <- peek (castPtr ptr)
-                !xs <- peek (ptr `plusPtr` sizeOf (undefined :: t))
-                return $ Identity x :& xs
-  {-# INLINABLE peek #-}
-  poke ptr (Identity !x :& xs) = poke (castPtr ptr) x >>
-                                 poke (ptr `plusPtr` sizeOf (undefined :: t)) xs
-  {-# INLINEABLE poke #-}
diff --git a/Data/Vinyl/Relation.hs b/Data/Vinyl/Relation.hs
deleted file mode 100644
--- a/Data/Vinyl/Relation.hs
+++ /dev/null
@@ -1,57 +0,0 @@
-{-# LANGUAGE ConstraintKinds       #-}
-{-# LANGUAGE DataKinds             #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE GADTs                 #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PolyKinds             #-}
-{-# LANGUAGE ScopedTypeVariables   #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE UndecidableInstances  #-}
-
-module Data.Vinyl.Relation
-  ( (<:)(..)
-  , (:~:)
-  , (~=)
-  -- , rIso
-  ) where
-
-import           Data.Vinyl.Field
-import           Data.Vinyl.Lens
-import           Data.Vinyl.Rec
-import           Data.Vinyl.Witnesses
-
-import           GHC.Prim             (Constraint)
-
--- | A subtyping relation.
-class (IsSubtype r1 r2) => r1 <: r2 where
-  cast :: r1 -> r2
-
--- | One record is a subtype of another if the fields of the latter are a
--- subset of the fields of the former.
-type family IsSubtype r1 r2 :: Constraint
-type instance IsSubtype (Rec ss f) (Rec ts f) = ISubset ts ss
-
--- | If two records types are subtypes of each other, that means that they
--- differ only in order of fields.
-type r1 :~: r2 = (r1 <: r2, r2 <: r1)
-
--- | Term-level record congruence.
-(~=) :: (Eq a, a :~: b) => a -> b -> Bool
-x ~= y = x == (cast y)
-
-instance Rec xs f <: Rec '[] f where
-  cast _ = RNil
-
-instance (y ~ (sy ::: t), IElem y xs, Rec xs f <: Rec ys f) => Rec xs f <: Rec (y ': ys) f where
-  cast r = rGet' field r :& cast r
-    where field = lookupField (implicitly :: Elem y xs) r
-
-lookupField :: Elem x xs -> Rec xs f -> x
-lookupField Here      (_ :& _)  = Field
-lookupField (There p) (_ :& xs) = lookupField p xs
-
--- rIso :: (r1 :~: r2) => Iso' r1 r2
--- rIso = iso cast cast
-
diff --git a/Data/Vinyl/TH.hs b/Data/Vinyl/TH.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/TH.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+module Data.Vinyl.TH
+  ( makeUniverse
+  , makeUniverse'
+  , Semantics(..)
+  , semantics
+  ) where
+
+import Language.Haskell.TH
+import Data.Vinyl.TyFun
+
+makeUniverse :: Name -> Q [Dec]
+makeUniverse u = makeUniverse' u ("El" ++ nameBase u)
+
+makeUniverse' :: Name -> String -> Q [Dec]
+makeUniverse' u elName = do
+  let elu = mkName elName
+  u' <- conT u
+
+  tvs <- do
+    el <- newName "el"
+    tyfun <- conT ''TyFun
+    return [KindedTV el (AppT (AppT tyfun u') StarT)]
+
+  let cons = [NormalC elu []]
+  return [DataD [] elu tvs cons []]
+
+class TyRep r where
+  asType :: r -> TypeQ
+instance TyRep Name where
+  asType = conT
+instance TyRep (Q Type) where
+  asType = id
+
+data Semantics = forall s t. (TyRep t, TyRep s) => t :~> s
+
+semantics :: Name -> [Semantics] -> Q [Dec]
+semantics elu sems = sequence (map inst sems)
+  where
+    inst :: Semantics -> Q Dec
+    inst (u :~> t) = do
+      elu' <- conT elu
+      u' <- asType u
+      t' <- asType t
+      return $ TySynInstD ''App (TySynEqn [elu',u'] t')
diff --git a/Data/Vinyl/TyFun.hs b/Data/Vinyl/TyFun.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/TyFun.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Vinyl.TyFun where
+
+data TyFun :: * -> * -> *
+type family App (f :: TyFun k l -> *) (a :: k) :: l
+
+data TC :: (k -> *) -> TyFun k * -> *
+type instance App (TC t) x = t x
+type f $ x = App f x
+
diff --git a/Data/Vinyl/Unicode.hs b/Data/Vinyl/Unicode.hs
deleted file mode 100644
--- a/Data/Vinyl/Unicode.hs
+++ /dev/null
@@ -1,16 +0,0 @@
-{-# LANGUAGE ConstraintKinds           #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE TypeOperators             #-}
-{-# LANGUAGE UnicodeSyntax             #-}
-
-module Data.Vinyl.Unicode where
-
-import           Data.Vinyl.Rec
-import           Data.Vinyl.Relation
-import           Data.Vinyl.Witnesses
-
-type x ∈ xs = IElem x xs
-type xs ⊆ ys = ISubset xs ys
-type r1 ≅ r2 = r1 :~: r2
-
-(≅) = (~=)
diff --git a/Data/Vinyl/Universe.hs b/Data/Vinyl/Universe.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Universe.hs
@@ -0,0 +1,7 @@
+module Data.Vinyl.Universe
+  ( module Data.Vinyl.Universe.Id
+  , module Data.Vinyl.Universe.Field
+  ) where
+
+import Data.Vinyl.Universe.Id
+import Data.Vinyl.Universe.Field
diff --git a/Data/Vinyl/Universe/Const.hs b/Data/Vinyl/Universe/Const.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Universe/Const.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE DataKinds    #-}
+{-# LANGUAGE GADTs        #-}
+{-# LANGUAGE PolyKinds    #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Data.Vinyl.Universe.Const (Const(..)) where
+
+import Data.Vinyl.TyFun
+
+data Const :: * -> (TyFun k *) -> * where
+  Const :: Const t el
+
+type instance App (Const t) x = t
diff --git a/Data/Vinyl/Universe/Field.hs b/Data/Vinyl/Universe/Field.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Universe/Field.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE DataKinds     #-}
+{-# LANGUAGE GADTs         #-}
+{-# LANGUAGE PolyKinds     #-}
+{-# LANGUAGE TypeFamilies  #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Vinyl.Universe.Field where
+
+import Data.Vinyl.TyFun
+import GHC.TypeLits
+
+data (sy :: k) ::: (t :: *)
+
+data SField :: * -> * where
+  SField :: KnownSymbol sy => SField (sy ::: t)
+
+data ElField :: (TyFun * *) -> * where
+  ElField :: ElField el
+type instance App ElField (sy ::: t) = t
diff --git a/Data/Vinyl/Universe/Id.hs b/Data/Vinyl/Universe/Id.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Universe/Id.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE DataKinds    #-}
+{-# LANGUAGE GADTs        #-}
+{-# LANGUAGE PolyKinds    #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Data.Vinyl.Universe.Id (Id(..)) where
+
+import Data.Vinyl.TyFun
+
+data Id :: (TyFun k k) -> * where
+  Id :: Id el
+type instance App Id x = x
+
diff --git a/Data/Vinyl/Witnesses.hs b/Data/Vinyl/Witnesses.hs
--- a/Data/Vinyl/Witnesses.hs
+++ b/Data/Vinyl/Witnesses.hs
@@ -20,24 +20,10 @@
 
 -- | A constraint for implicit resolution of list membership proofs.
 type IElem x xs = Implicit (Elem x xs)
-
--- | An inductive list subset relation.
-data Subset :: [k] -> [k] -> * where
-  SubsetNil  :: Subset '[] xs
-  SubsetCons :: Elem x ys
-             -> Subset xs ys
-             -> Subset (x ': xs) ys
-
--- | A constraint for implicit resolution of list subset proofs.
-type ISubset xs ys = Implicit (Subset xs ys)
+type x ∈ xs = IElem x xs
 
 instance Implicit (Elem x (x ': xs)) where
   implicitly = Here
 instance Implicit (Elem x xs) => Implicit (Elem x (y ': xs)) where
   implicitly = There implicitly
-
-instance Implicit (Subset '[] xs) where
-  implicitly = SubsetNil
-instance (IElem x ys, ISubset xs ys) => Implicit (Subset (x ': xs) ys) where
-  implicitly = SubsetCons implicitly implicitly
 
diff --git a/tests/Intro.lhs b/tests/Intro.lhs
--- a/tests/Intro.lhs
+++ b/tests/Intro.lhs
@@ -17,45 +17,72 @@
 Let’s work through a quick example. We’ll need to enable some language
 extensions first:
 
-> {-# LANGUAGE DataKinds, TypeOperators #-}
-> {-# LANGUAGE FlexibleContexts, NoMonomorphismRestriction #-}
-> {-# LANGUAGE GADTs #-}
+> {-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-}
+> {-# LANGUAGE FlexibleContexts, FlexibleInstances, NoMonomorphismRestriction #-}
+> {-# LANGUAGE GADTs, TemplateHaskell, TypeSynonymInstances #-}
 > import Data.Vinyl
-> import Data.Vinyl.Unicode
+> import Data.Vinyl.TyFun
+> import Data.Vinyl.TH
+> import Data.Vinyl.Functor
 > import Data.Vinyl.Idiom.Identity
 > import Data.Vinyl.Idiom.Validation
+> import Data.Vinyl.Witnesses
+> import qualified Data.Vinyl.Universe.Const as U
 > import Control.Applicative
 > import Control.Lens hiding (Identity)
 > import Data.Char
 > import Test.DocTest
+> import Data.Singletons.TH
 
-Let’s define the fields we want to use:
+Let’s define a universe of fields which we want to use:
 
-> name     = Field :: "name"     ::: String
-> age      = Field :: "age"      ::: Int
-> sleeping = Field :: "sleeping" ::: Bool
+> data Fields = Name | Age | Sleeping | Master deriving Show
+> genSingletons [ ''Fields ]
+> makeUniverse' ''Fields "ElF"
+> semantics ''ElF [ 'Name     :~> ''String
+>                 , 'Age      :~> ''Int
+>                 , 'Sleeping :~> ''Bool
+>                 ]
 
 Now, let’s try to make an entity that represents a man:
 
-> jon = name =: "jon"
->    <+> age =: 20
->    <+> sleeping =: False
+> jon = SName =: "jon"
+>    <+> SAge =: 20
+>    <+> SSleeping =: False
 
+
 We could make an alias for the sort of entity that jon is:
 
-> type LifeForm = ["name" ::: String, "age" ::: Int, "sleeping" ::: Bool]
-> jon :: PlainRec LifeForm
+> type LifeForm = [Name, Age, Sleeping]
+> jon :: PlainRec ElF LifeForm
 
+We can print out the record by assigning names to each field:
+
+> instance Implicit (PlainRec (U.Const String) [ Name, Age, Sleeping ]) where
+>   implicitly = SName     =: "name"
+>            <+> SAge      =: "age"
+>            <+> SSleeping =: "sleeping"
+
+> -- | >>> rshow jon
+> -- "{ name =: \"jon\", age =: 20, sleeping =: False }"
+
 The types are inferred, though, so this is unnecessary unless you’d
 like to reuse the type later. Now, make a dog! Dogs are life-forms,
 but unlike men, they have masters. So, let’s build my dog:
 
-> master = Field :: "master" ::: PlainRec LifeForm
-> tucker = name =: "tucker"
->       <+> age =: 7
->       <+> sleeping =: True
->       <+> master =: jon
+> semantics ''ElF [ 'Master :~> [t| PlainRec ElF LifeForm |] ]
 
+> tucker = withUniverse ElF $
+>   SName =: "tucker"
+>   <+> SAge =: 7
+>   <+> SSleeping =: True
+>   <+> SMaster =: jon
+
+It was necessary to specify the interpreter for the universe in which `tucker`
+lives, since (lacking a type annotation), records constructed using `(<+>)` and
+`(=:)` are polymorphic with respect to `el`. We can help along the type
+inference by giving it explicitly using `withUniverse`.
+
 Using Lenses
 ------------
 
@@ -65,8 +92,8 @@
 on a particular field in the record for access and update, without
 losing additional information:
 
-> wakeUp :: (("sleeping" ::: Bool) ∈ fields) => PlainRec fields -> PlainRec fields
-> wakeUp = sleeping `rPut` False
+> wakeUp :: (Sleeping ∈ fields) => PlainRec ElF fields -> PlainRec ElF fields
+> wakeUp = SSleeping `rPut` False
 
 Now, the type annotation on wakeUp was not necessary; I just wanted to
 show how intuitive the type is. Basically, it takes as an input any
@@ -77,34 +104,30 @@
 > jon' = wakeUp jon
 
 > -- |
-> -- >>> tucker' ^. rLens sleeping
+> -- >>> tucker' ^. rLens SSleeping
 > -- False
 > --
-> -- >>> tucker ^. rLens sleeping
+> -- >>> tucker ^. rLens SSleeping
 > -- True
 > --
-> -- >>> jon' ^. rLens sleeping
+> -- >>> jon' ^. rLens SSleeping
 > -- False
 
 We can also access the entire lens for a field using the rLens
 function; since lenses are composable, it’s super easy to do deep
 update on a record:
 
-> masterSleeping :: (("master" ::: PlainRec LifeForm) ∈ fields) => Lens' (PlainRec fields) Bool
-> masterSleeping = rLens master . rLens sleeping
+> masterSleeping :: (Master ∈ fields) => Lens' (PlainRec ElF fields) Bool
+> masterSleeping = rLens SMaster . rLens SSleeping
 > tucker'' = masterSleeping .~ True $ tucker'
 
-> -- | >>> tucker'' ^. rLens master . rLens sleeping
+
+> -- | >>> tucker'' ^. masterSleeping
 > -- True
 
-Again, the type annotation is unnecessary. In fact, the seperate
-definition is also unnecessary, and we could just define:
+Again, the type annotation is unnecessary.
 
-> tucker''' = rLens master . rLens sleeping .~ True $ tucker'
 
-> -- | >>> tucker''' ^. rLens master . rLens sleeping
-> -- True
-
 Subtyping Relation and Coercion
 -------------------------------
 
@@ -117,15 +140,15 @@
 
 Therefore, the following works:
 
-> upcastedTucker :: PlainRec LifeForm
-> upcastedTucker = cast (fixRecord tucker)
+> upcastedTucker :: PlainRec ElF LifeForm
+> upcastedTucker = cast (toPlainRec tucker)
 
-The reason for using `fixRecord` will become clear a bit later.
+The reason for using `toPlainRec` will become clear a bit later.
 
 The subtyping relationship between record types is expressed with the
 `(<:)` constraint; so, cast is of the following type:
 
-< cast :: r1 <: r2 => r1 -> r2
+< cast :: r1 <: r2 => Rec r1 f -> Rec r2 f
 
 Also provided is a `(≅)` constraint which indicates record congruence
 (that is, two record types differ only in the order of their fields).
@@ -133,13 +156,13 @@
 Records are polymorphic over functors
 -------------------------------------
 
-So far, we’ve been working with the PlainRec type; but below that,
-there is something a bit more advanced called Rec, which looks like
+So far, we’ve been working with the `PlainRec` type; but below that,
+there is something a bit more advanced called `Rec`, which looks like
 this:
 
-< data Rec :: [*] -> (* -> *) -> * where
-<   RNil :: Rec '[] f
-<   (:&) :: (r ~ (sy ::: t)) => f t -> Rec rs f -> Rec (r ': rs) f
+< data Rec :: (TyFun u * -> *) -> (* -> *) -> [u] -> * where
+<   RNil :: Rec el f '[]
+<   (:&) :: f (el $ r) -> Rec el f rs -> Rec el f (r ': rs)
 
 The second parameter is a functor, in which every element of the
 record will be placed. In `PlainRec`, the functor is just set to
@@ -148,22 +171,23 @@
 Let’s imagine that we want to do validation on a record that
 represents a name and an age:
 
-> type Person = ["name" ::: String, "age" ::: Int]
+> type Person = [Name, Age]
 
 We’ve decided that names must be alphabetic, and ages must be
 positive. For validation, we’ll use a type that’s included here called
 `Result e a`, which is similar to `Either`, except that its
 `Applicative` instance accumulates monoidal errors on the left.
 
-> goodPerson :: PlainRec Person
-> goodPerson = name =: "Jon"
->          <+> age =: 20
-> badPerson = name =: "J#@#$on"
->          <+> age =: 20
-> validatePerson :: PlainRec Person -> Result [String] (PlainRec Person)
-> validatePerson p = (\n a -> name =: n <+> age =: a) <$> vName <*> vAge where
->   vName = validateName (rGet name p)
->   vAge  = validateAge  (rGet age p)
+> goodPerson :: PlainRec ElF Person
+> goodPerson = SName =: "Jon"
+>          <+> SAge  =: 20
+> badPerson = SName =: "J#@#$on"
+>         <+> SAge  =: 20
+
+> validatePerson :: PlainRec ElF Person -> Result [String] (PlainRec ElF Person)
+> validatePerson p = (\n a -> SName =: n <+> SAge =: a) <$> vName <*> vAge where
+>   vName = validateName (rGet SName p)
+>   vAge  = validateAge  (rGet SAge p)
 >
 >   validateName str | all isAlpha str = Success str
 >   validateName _ = Failure [ "name must be alphabetic" ]
@@ -191,22 +215,22 @@
 then that record could be applied to a plain one, to get a record of
 validated fields? That’s what we’re going to do.
 
-Vinyl provides a type of validators, which is basically a natural
-transformation from the `Identity` functor to the `Result` functor, which
-we just used above.
+Vinyl provides a type of validators, which is the class of functions from the
+`Identity` functor to the `Result` functor at some type.
 
-< type Validator e = Identity ~> Result e
+< type Validator e = Lift (->) Identity ~> Result e
 
 Let’s parameterize a record by it: when we do, then an element of type
 `a` should be a function `Identity a -> Result e a`:
 
-> vperson :: Rec Person (Validator [String])
-> vperson = NT validateName :& NT validateAge :& RNil where
+> vperson :: Rec ElF (Validator [String]) Person
+> vperson = Lift validateName :& Lift validateAge :& RNil where
 >    validateName (Identity str) | all isAlpha str = Success str
 >    validateName _ = Failure [ "name must be alphabetic" ]
 >    validateAge (Identity i) | i >= 0 = Success i
 >    validateAge _ = Failure [ "age must be positive" ]
 
+
 And we can use the special application operator `<<*>>` (which is
 analogous to `<*>`, but generalized a bit) to use this to validate a
 record:
@@ -214,29 +238,29 @@
 > goodPersonResult = vperson <<*>> goodPerson
 > badPersonResult  = vperson <<*>> badPerson
 
-goodPersonResult === name :=: Success "Jon", age :=: Success 20, {}
-badPersonResult  === name :=: Failure ["name must be alphabetic"], age :=: Success 20, {}
+< goodPersonResult === SName :=: Success "Jon", SAge :=: Success 20, {}
+< badPersonResult  === SName :=: Failure ["name must be alphabetic"], SAge :=: Success 20, {}
 
 > -- |
-> -- >>> isSuccess $ goodPersonResult ^. rLens' name
+> -- >>> isSuccess $ goodPersonResult ^. rLens' SName
 > -- True
-> -- >>> isSuccess $ goodPersonResult ^. rLens' age
+> -- >>> isSuccess $ goodPersonResult ^. rLens' SAge
 > -- True
-> -- >>> isSuccess $ badPersonResult ^. rLens' name
+> -- >>> isSuccess $ badPersonResult ^. rLens' SName
 > -- False
-> -- >>> isSuccess $ badPersonResult ^. rLens' age
+> -- >>> isSuccess $ badPersonResult ^. rLens' SAge
 > -- True
 
 So now we have a partial record, and we can still do stuff with its
 contents. Next, we can even recover the original behavior of the
 validator (that is, to give us a value of type `Result [String]
-(PlainRec Person)`) using `dist`:
+(PlainRec Person)`) using `rdist`:
 
-> distGoodPerson = dist goodPersonResult
-> distBadPerson  = dist badPersonResult
+> distGoodPerson = rdist goodPersonResult
+> distBadPerson  = rdist badPersonResult
 
-`distGoodPerson === Success name :=: "Jon", age :=: 20, {}`
-`distBadPerson  === Failure ["name must be alphabetic"]``
+< distGoodPerson === Success name :=: "Jon", age :=: 20, {}
+< distBadPerson  === Failure ["name must be alphabetic"]
 
 > -- |
 > -- >>> isSuccess distGoodPerson
@@ -250,15 +274,15 @@
 If you produced a record using `(=:)` and `(<+>)` without providing a
 type annotation, then its type is something like this:
 
-< record :: Applicative f => Record [ <bunch of stuff> ] f
+< record :: Applicative f => Rec el f [ <bunch of stuff> ]
 
 The problem is then we can’t do anything with the record that requires
 us to know what its functor is. For instance, `cast` will fail. So, we
 might try to provide a type annotation, but that can be a bit brittle
-and frustrating to have to do. To alleviate this problem, `fixRecord` is
+and frustrating to have to do. To alleviate this problem, `toPlainRec` is
 provided:
 
-< fixRecord :: (forall f. Applicative f => Rec rs f) -> PlainRec rs
+< toPlainRec :: (forall f. Applicative f => Rec el f rs) -> PlainRec el rs
 
 ---
 
@@ -266,3 +290,4 @@
 
 > main :: IO ()
 > main = doctest ["tests/Intro.lhs"]
+
diff --git a/vinyl.cabal b/vinyl.cabal
--- a/vinyl.cabal
+++ b/vinyl.cabal
@@ -1,5 +1,5 @@
 name:                vinyl
-version:             0.3
+version:             0.4
 synopsis:            Extensible Records
 -- description:
 license:             MIT
@@ -19,19 +19,31 @@
   location: https://github.com/VinylRecords/Vinyl/
 
 library
-  exposed-modules:     Data.Vinyl, Data.Vinyl.Field, Data.Vinyl.Lens,
-                       Data.Vinyl.Witnesses, Data.Vinyl.Rec,
-                       Data.Vinyl.Relation, Data.Vinyl.Unicode,
-                       Data.Vinyl.Classes, Data.Vinyl.Idiom.Validation,
-                       Data.Vinyl.Idiom.Identity, Data.Vinyl.Idiom.LazyIdentity
-  build-depends:       base >=4.6 && <= 5, ghc-prim
+  exposed-modules:     Data.Vinyl
+                     , Data.Vinyl.Core
+                     , Data.Vinyl.Operators
+                     , Data.Vinyl.Lens
+                     , Data.Vinyl.Witnesses
+                     , Data.Vinyl.Constraint
+                     , Data.Vinyl.Idiom.Validation
+                     , Data.Vinyl.Idiom.Identity
+                     , Data.Vinyl.Idiom.Thunk
+                     , Data.Vinyl.TyFun
+                     , Data.Vinyl.Functor
+                     , Data.Vinyl.Universe
+                     , Data.Vinyl.Universe.Id
+                     , Data.Vinyl.Universe.Const
+                     , Data.Vinyl.Universe.Field
+                     , Data.Vinyl.TH
+  build-depends:       base >=4.6 && <= 5, ghc-prim, template-haskell == 2.9.0.0
   default-language:    Haskell2010
+  ghc-options: -fwarn-dodgy-exports -fwarn-dodgy-imports -fwarn-unused-matches -fwarn-unused-imports -fwarn-unused-binds -fwarn-incomplete-record-updates -fwarn-missing-signatures -fwarn-name-shadowing -fwarn-orphans -fwarn-overlapping-patterns -fwarn-tabs -fwarn-type-defaults
 
 benchmark bench-builder-all
   type:             exitcode-stdio-1.0
   hs-source-dirs:   benchmarks
   main-is:          StorableBench.hs
-  build-depends:    base >= 4.6 && <= 5, vector, criterion, vinyl == 0.3, mwc-random, lens, linear
+  build-depends:    base >= 4.6 && <= 5, vector, criterion, vinyl == 0.4, mwc-random, lens, linear
   ghc-options:      -O2 -fllvm
   default-language: Haskell2010
 
@@ -39,5 +51,5 @@
   type:             exitcode-stdio-1.0
   hs-source-dirs:   tests
   main-is:          Intro.lhs
-  build-depends:    base >= 4.6 && <= 5, lens, vinyl == 0.3, doctest >= 0.8
+  build-depends:    base >= 4.6 && <= 5, lens, vinyl == 0.4, doctest >= 0.8, singletons == 1.0
   default-language: Haskell2010