diff --git a/Data/Vinyl.hs b/Data/Vinyl.hs
--- a/Data/Vinyl.hs
+++ b/Data/Vinyl.hs
@@ -1,16 +1,10 @@
 module Data.Vinyl
   ( module Data.Vinyl.Core
   , module Data.Vinyl.Derived
-  , module Data.Vinyl.Operators
   , module Data.Vinyl.Lens
-  , module Data.Vinyl.Witnesses
-  , module Data.Vinyl.Constraint
   ) where
 
 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/Constraint.hs b/Data/Vinyl/Constraint.hs
deleted file mode 100644
--- a/Data/Vinyl/Constraint.hs
+++ /dev/null
@@ -1,50 +0,0 @@
-{-# 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
--- a/Data/Vinyl/Core.hs
+++ b/Data/Vinyl/Core.hs
@@ -1,80 +1,191 @@
-{-# LANGUAGE BangPatterns        #-}
-{-# LANGUAGE DataKinds           #-}
-{-# LANGUAGE FlexibleContexts    #-}
-{-# LANGUAGE FlexibleInstances   #-}
-{-# LANGUAGE GADTs               #-}
-{-# LANGUAGE PolyKinds           #-}
-{-# LANGUAGE RankNTypes          #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies        #-}
-{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE BangPatterns          #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
 
 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(..))
+import Data.Vinyl.Functor
+import Control.Applicative hiding (Const(..))
+import Data.Typeable (Proxy(..))
+import Data.List (intercalate)
+import Data.Vinyl.TypeLevel
 
--- | 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 (el :: TyFun u * -> *) (f :: * -> *) (rrs :: [u]) where
-  RNil :: Rec el f '[]
-  (:&) :: !(f (el $ r)) -> !(Rec el f rs) -> Rec el f (r ': rs)
+-- | A record is parameterized by a universe @u@, an interpretation @f@ and a
+-- list of rows @rs@.  The labels or indices of the record are given by
+-- inhabitants of the kind @u@; the type of values at any label @r :: u@ is
+-- given by its interpretation @f r :: *@.
+data Rec :: (u -> *) -> [u] -> * where
+  RNil :: Rec f '[]
+  (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs)
+
 infixr :&
+infixr 5  <+>
+infixl 8 <<$>>
+infixl 8 <<*>>
 
--- | 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
+-- | Two records may be pasted together.
+rappend
+  :: Rec f as
+  -> Rec f bs
+  -> Rec f (as ++ bs)
+rappend RNil ys = ys
+rappend (x :& xs) ys = x :& (xs `rappend` ys)
 
--- | 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 <-:
+-- | A shorthand for 'rappend'.
+(<+>)
+  :: Rec f as
+  -> Rec f bs
+  -> Rec f (as ++ bs)
+(<+>) = rappend
 
--- | 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 #-}
+-- | 'Rec' @_ rs@ with labels in kind @u@ gives rise to a functor @Hask^u ->
+-- Hask@; that is, a natural transformation between two interpretation functors
+-- @f,g@ may be used to transport a value from 'Rec' @f rs@ to 'Rec' @g rs@.
+rmap
+  :: (forall x. f x -> g x)
+  -> Rec f rs
+  -> Rec g rs
+rmap _ RNil = RNil
+rmap η (x :& xs) = η x :& (η `rmap` xs)
+{-# INLINE rmap #-}
 
-instance Monoid (Rec el f '[]) where
+-- | A shorthand for 'rmap'.
+(<<$>>)
+  :: (forall x. f x -> g x)
+  -> Rec f rs
+  -> Rec g rs
+(<<$>>) = rmap
+{-# INLINE (<<$>>) #-}
+
+-- | An inverted shorthand for 'rmap'.
+(<<&>>)
+  :: Rec f rs
+  -> (forall x. f x -> g x)
+  -> Rec g rs
+xs <<&>> f = rmap f xs
+{-# INLINE (<<&>>) #-}
+
+-- | A record of components @f r -> g r@ may be applied to a record of @f@ to
+-- get a record of @g@.
+rapply
+  :: Rec (Lift (->) f g) rs
+  -> Rec f rs
+  -> Rec g rs
+rapply RNil RNil = RNil
+rapply (f :& fs) (x :& xs) = getLift f x :& (fs `rapply` xs)
+{-# INLINE rapply #-}
+
+-- | A shorthand for 'rapply'.
+(<<*>>)
+  :: Rec (Lift (->) f g) rs
+  -> Rec f rs
+  -> Rec g rs
+(<<*>>) = rapply
+{-# INLINE (<<*>>) #-}
+
+-- | Given a section of some functor, records in that functor of any size are
+-- inhabited.
+class RecApplicative rs where
+  rpure
+    :: (forall x. f x)
+    -> Rec f rs
+instance RecApplicative '[] where
+  rpure _ = RNil
+  {-# INLINE rpure #-}
+instance RecApplicative rs => RecApplicative (r ': rs) where
+  rpure s = s :& rpure s
+  {-# INLINE rpure #-}
+
+-- | A record may be traversed with respect to its interpretation functor. This
+-- can be used to yank (some or all) effects from the fields of the record to
+-- the outside of the record.
+rtraverse
+  :: Applicative h
+  => (forall x. f x -> h (g x))
+  -> Rec f rs
+  -> h (Rec g rs)
+rtraverse _ RNil      = pure RNil
+rtraverse f (x :& xs) = (:&) <$> f x <*> rtraverse f xs
+
+-- | A record with uniform fields may be turned into a list.
+recordToList
+  :: Rec (Const a) rs
+  -> [a]
+recordToList RNil = []
+recordToList (x :& xs) = getConst x : recordToList xs
+
+-- | Wrap up a value with a capability given by its type
+data Dict c a where
+  Dict
+    :: c a
+    => a
+    -> Dict c a
+
+-- | Sometimes we may know something for /all/ fields of a record, but when
+-- you expect to be able to /each/ of the fields, you are then out of luck.
+-- Surely given @∀x:u.φ(x)@ we should be able to recover @x:u ⊢ φ(x)@! Sadly,
+-- the constraint solver is not quite smart enough to realize this and we must
+-- make it patently obvious by reifying the constraint pointwise with proof.
+reifyConstraint
+  :: RecAll f rs c
+  => proxy c
+  -> Rec f rs
+  -> Rec (Dict c :. f) rs
+reifyConstraint prx rec =
+  case rec of
+    RNil -> RNil
+    (x :& xs) -> Compose (Dict x) :& reifyConstraint prx xs
+
+-- | Records may be shown insofar as their points may be shown.
+-- 'reifyConstraint' is used to great effect here.
+instance RecAll f rs Show => Show (Rec f rs) where
+  show xs =
+    (\str -> "{" <> str <> "}")
+      . intercalate "; "
+      . recordToList
+      . rmap (\(Compose (Dict x)) -> Const $ show x)
+      $ reifyConstraint (Proxy :: Proxy Show) xs
+
+instance Monoid (Rec 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 (Monoid (f r), Monoid (Rec f rs)) => Monoid (Rec f (r ': rs)) where
+  mempty = mempty :& mempty
+  (x :& xs) `mappend` (y :& ys) = (x <> y) :& (xs <> ys)
 
-instance Eq (Rec el f '[]) where
+instance Eq (Rec f '[]) where
   _ == _ = True
-instance (Eq (f (el $ r)), Eq (Rec el f rs)) => Eq (Rec el f (r ': rs)) where
+instance (Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs)) where
   (x :& xs) == (y :& ys) = (x == y) && (xs == ys)
 
-instance Storable (Rec el Identity '[]) where
+instance Storable (Rec f '[]) 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)
+instance (Storable (f r), Storable (Rec f rs)) => Storable (Rec f (r ': rs)) where
+  sizeOf _ = sizeOf (undefined :: f r) + sizeOf (undefined :: Rec f rs)
   {-# INLINABLE sizeOf #-}
-  alignment _ =  alignment (undefined :: el $ r)
+  alignment _ =  alignment (undefined :: f r)
   {-# INLINABLE alignment #-}
   peek ptr = do !x <- peek (castPtr ptr)
-                !xs <- peek (ptr `plusPtr` sizeOf (undefined :: el $ r))
-                return $ Identity x :& xs
+                !xs <- peek (ptr `plusPtr` sizeOf (undefined :: f r))
+                return $ x :& xs
   {-# INLINABLE peek #-}
-  poke ptr (Identity !x :& xs) = poke (castPtr ptr) x >>
-                                 poke (ptr `plusPtr` sizeOf (undefined :: el $ r)) xs
+  poke ptr (!x :& xs) = poke (castPtr ptr) x >> poke (ptr `plusPtr` sizeOf (undefined :: f r)) xs
   {-# INLINEABLE poke #-}
-
diff --git a/Data/Vinyl/Derived.hs b/Data/Vinyl/Derived.hs
--- a/Data/Vinyl/Derived.hs
+++ b/Data/Vinyl/Derived.hs
@@ -1,26 +1,18 @@
+{-# LANGUAGE DataKinds  #-}
+{-# LANGUAGE GADTs      #-}
 {-# LANGUAGE PolyKinds  #-}
 {-# LANGUAGE RankNTypes #-}
 
 module Data.Vinyl.Derived where
 
 import Data.Vinyl.Core
-import qualified Data.Vinyl.Idiom.Identity as I
-import qualified Data.Vinyl.Idiom.Thunk as I
-import qualified Data.Vinyl.Universe as U
-
-import Control.Applicative
-
-type PlainRec el = Rec el I.Identity
-type LazyPlainRec el = Rec el I.Thunk
-type FieldRec = Rec U.ElField
-type PlainFieldRec = Rec U.ElField I.Identity
-type HList = Rec U.Id I.Identity
-type LazyHList = Rec U.Id I.Thunk
+import Data.Vinyl.Functor
 
--- | Fixes a polymorphic record into the 'Identity' functor.
-toPlainRec :: (forall f. Applicative f => Rec el f rs) -> PlainRec el rs
-toPlainRec xs = xs
+import GHC.TypeLits
 
-toLazyPlainRec :: (forall f. Applicative f => Rec el f rs) -> LazyPlainRec el rs
-toLazyPlainRec xs = xs
+data ElField (field :: (Symbol, *)) where
+  Field :: KnownSymbol s => t -> ElField '(s,t)
 
+type FieldRec = Rec ElField
+type HList = Rec Identity
+type LazyHList = Rec Thunk
diff --git a/Data/Vinyl/Functor.hs b/Data/Vinyl/Functor.hs
--- a/Data/Vinyl/Functor.hs
+++ b/Data/Vinyl/Functor.hs
@@ -1,14 +1,85 @@
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DeriveFoldable             #-}
+{-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE DeriveTraversable          #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE PolyKinds                  #-}
+{-# LANGUAGE TypeOperators              #-}
 
 module Data.Vinyl.Functor where
 
 import Control.Applicative
+import Data.Foldable
+import Data.Traversable
+import Foreign.Storable
 
-class Presheaf f where
-  contramap :: (a -> b) -> (f b -> f a)
+newtype Identity a
+  = Identity { getIdentity :: a }
+    deriving ( Functor
+             , Foldable
+             , Traversable
+             , Storable
+             )
 
-newtype Lift op f g x = Lift { runLift :: op (f x) (g x) }
+data Thunk a
+  = Thunk { getThunk :: a }
+    deriving ( Functor
+             , Foldable
+             , Traversable
+             )
 
+newtype Lift (op :: l -> l' -> *) (f :: k -> l) (g :: k -> l') (x :: k)
+  = Lift { getLift :: op (f x) (g x) }
+
+newtype Compose (f :: l -> *) (g :: k -> l) (x :: k)
+  = Compose { getCompose :: f (g x) }
+    deriving (Storable)
+
+type f :. g = Compose f g
+
+newtype Const (a :: *) (b :: k)
+  = Const { getConst :: a }
+    deriving ( Functor
+             , Foldable
+             , Traversable
+             , Storable
+             )
+
+instance (Functor f, Functor g) => Functor (Compose f g) where
+  fmap f (Compose x) = Compose (fmap (fmap f) x)
+
+instance (Foldable f, Foldable g) => Foldable (Compose f g) where
+  foldMap f (Compose t) = foldMap (foldMap f) t
+
+instance (Traversable f, Traversable g) => Traversable (Compose f g) where
+  traverse f (Compose t) = Compose <$> traverse (traverse f) t
+
+instance (Applicative f, Applicative g) => Applicative (Compose f g) where
+  pure x = Compose (pure (pure x))
+  Compose f <*> Compose x = Compose ((<*>) <$> f <*> x)
+
+instance Applicative Identity where
+  pure = Identity
+  Identity f <*> Identity x = Identity (f x)
+
+instance Monad Identity where
+  return = Identity
+  Identity x >>= f = f x
+
+instance Show a => Show (Identity a) where
+  show (Identity x) = show x
+
+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
+
 instance (Functor f, Functor g) => Functor (Lift (,) f g) where
   fmap f (Lift (x, y)) = Lift (fmap f x, fmap f y)
 
@@ -16,20 +87,7 @@
   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/Identity.hs b/Data/Vinyl/Idiom/Identity.hs
deleted file mode 100644
--- a/Data/Vinyl/Idiom/Identity.hs
+++ /dev/null
@@ -1,25 +0,0 @@
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveTraversable #-}
-
-module Data.Vinyl.Idiom.Identity where
-
-import Control.Applicative
-import Data.Foldable
-import Data.Traversable
-
-newtype Identity a
-  = Identity
-  { runIdentity :: a
-  } deriving (Functor, Foldable, Traversable)
-
-instance Applicative Identity where
-  pure = Identity
-  (Identity f) <*> (Identity x) = Identity (f x)
-
-instance Monad Identity where
-  return = Identity
-  (Identity x) >>= f = f x
-
-instance Show a => Show (Identity a) where
-  show (Identity x) = show x
diff --git a/Data/Vinyl/Idiom/Thunk.hs b/Data/Vinyl/Idiom/Thunk.hs
deleted file mode 100644
--- a/Data/Vinyl/Idiom/Thunk.hs
+++ /dev/null
@@ -1,25 +0,0 @@
-{-# 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
deleted file mode 100644
--- a/Data/Vinyl/Idiom/Validation.hs
+++ /dev/null
@@ -1,32 +0,0 @@
-{-# LANGUAGE TypeOperators #-}
-
-module Data.Vinyl.Idiom.Validation where
-
-import Data.Vinyl.Idiom.Identity
-import Data.Vinyl.Functor
-
-import Control.Applicative
-import Data.Monoid
-
--- | A type which is similar to 'Either', except that it has a
--- slightly different Applicative instance.
-data Result e a
-  = Failure e
-  | Success a
-  deriving (Show, Eq)
-
--- | Validators transform identities into results.
-type Validator e = Lift (->) Identity (Result e)
-
-instance Functor (Result e) where
-  fmap f (Success x) = Success $ f x
-  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 _)  = 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,82 +1,138 @@
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
 {-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
 {-# 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
+module Data.Vinyl.Lens
+  ( RElem(..)
+  , RSubset(..)
+  , REquivalent
+  , type (∈)
+  , type (⊆)
+  , type (≅)
+  , type (<:)
+  , type (:~:)
+  ) where
 
 import Data.Vinyl.Core
-import Data.Vinyl.Derived
-import Data.Vinyl.TyFun
-import Data.Vinyl.Witnesses
-import Data.Vinyl.Idiom.Identity
+import Data.Vinyl.Functor
+import Data.Vinyl.TypeLevel
+import Data.Typeable (Proxy(..))
 
-import Control.Applicative
+-- | The presence of a field in a record is witnessed by a lens into its value.
+-- The third parameter to 'RElem', @i@, is there to help the constraint solver
+-- realize that this is a decidable predicate with respect to the judgemental
+-- equality in @k@.
+class i ~ RIndex r rs => RElem (r :: k) (rs :: [k]) (i :: Nat) where
 
--- | Project a field from a 'Rec'.
-rGet' :: (r ∈ rs) => sing r -> Rec el f rs -> f (el $ r)
-rGet' r = getConst . rLens' r Const
-{-# INLINE rGet' #-}
+  -- | We can get a lens for getting and setting the value of a field which is
+  -- in a record. As a convenience, we take a proxy argument to fix the
+  -- particular field being viewed. These lenses are compatible with the @lens@
+  -- library. Morally:
+  --
+  -- > rlens :: sing r => Lens' (Rec f rs) (f r)
+  rlens
+    :: Functor g
+    => sing r
+    -> (f r -> g (f r))
+    -> Rec f rs
+    -> g (Rec f rs)
 
--- | Project a field from a 'PlainRec'.
-rGet :: (r ∈ rs) => sing r -> PlainRec el rs -> el $ r
-rGet = (runIdentity .) . rGet'
-{-# INLINE rGet #-}
+  -- | For Vinyl users who are not using the @lens@ package, we provide a getter.
+  rget
+    :: sing r
+    -> Rec f rs
+    -> f r
+  rget k = getConst . rlens k Const
 
--- | Set a field in a 'Rec' over an arbitrary functor.
-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' #-}
+  -- | For Vinyl users who are not using the @lens@ package, we also provide a
+  -- setter. In general, it will be unambiguous what field is being written to,
+  -- and so we do not take a proxy argument here.
+  rput
+    :: f r
+    -> Rec f rs
+    -> Rec f rs
+  rput y = getIdentity . rlens Proxy (\_ -> Identity y)
 
--- | Set a field in a 'PlainRec'.
-rPut :: (r ∈ rs) => sing r -> el $ r -> PlainRec el rs -> PlainRec el rs
-rPut r x = rPut' r (Identity x)
-{-# INLINE rPut #-}
+-- This is an internal convenience stolen from the @lens@ library.
+lens
+  :: Functor f
+  => (t -> s)
+  -> (t -> a -> b)
+  -> (s -> f a)
+  -> t
+  -> f b
+lens sa sbt afb s = fmap (sbt s) $ afb (sa s)
+{-# INLINE lens #-}
 
--- | Modify a field.
-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 #-}
+instance RElem r (r ': rs) Z where
+  rlens _ f (x :& xs) = fmap (:& xs) (f x)
+  {-# INLINE rlens #-}
 
--- We manually unroll several levels of 'Elem' value traversal to help
--- GHC statically index into small records.
+instance (RIndex r (s ': rs) ~ S i, RElem r rs i) => RElem r (s ': rs) (S i) where
+  rlens p f (x :& xs) = fmap (x :&) (rlens p f xs)
+  {-# INLINE rlens #-}
 
--- | Provide a lens to a record field. Note that this implementation
--- does not support polymorphic update. In the parlance of the @lens@
--- package,
---
--- > 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 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) =
-          fmap (\x' -> a :& b :& x' :& xs) (f x)
-        go (There (There (There Here))) (a :& b :& c :& x :& xs) =
-          fmap (\x' -> a :& b :& c :& x' :& xs) (f x)
-        go (There (There (There (There Here)))) (a :& b :& c :& d :& x :& xs) =
-          fmap (\x' -> a :& b :& c :& d :& x' :& xs) (f x)
-        go (There (There (There (There p)))) (a :& b :& c :& d :& xs) =
-          fmap (\xs' -> a :& b :& c :& d :& xs') (go' p xs)
-        {-# INLINE go #-}
+-- | If one field set is a subset another, then a lens of from the latter's
+-- record to the former's is evident. That is, we can either cast a larger
+-- record to a smaller one, or we may replace the values in a slice of a
+-- record.
+class is ~ RImage rs ss => RSubset (rs :: [k]) (ss :: [k]) is where
 
-        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' #-}
-{-# INLINE rLens' #-}
+  -- | This is a lens into a slice of the larger record. Morally, we have:
+  --
+  -- > rsubset :: Lens' (Rec f ss) (Rec f rs)
+  rsubset
+    :: Functor g
+    => (Rec f rs -> g (Rec f rs))
+    -> Rec f ss
+    -> g (Rec f ss)
 
--- | A lens into a 'PlainRec' that smoothly interoperates with lenses
--- from the @lens@ package. Note that polymorphic update is not
--- supported. In the parlance of the @lens@ package,
---
--- > 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 #-}
+  -- | The getter of the 'rsubset' lens is 'rcast', which takes a larger record
+  -- to a smaller one by forgetting fields.
+  rcast
+    :: Rec f ss
+    -> Rec f rs
+  rcast = getConst . rsubset Const
+  {-# INLINE rcast #-}
+
+  -- | The setter of the 'rsubset' lens is 'rreplace', which allows a slice of
+  -- a record to be replaced with different values.
+  rreplace
+    :: Rec f rs
+    -> Rec f ss
+    -> Rec f ss
+  rreplace rs = getIdentity . rsubset (\_ -> Identity rs)
+  {-# INLINE rreplace #-}
+
+instance RSubset '[] ss '[] where
+  rsubset = lens (const RNil) const
+
+instance (RElem r ss i , RSubset rs ss is) => RSubset (r ': rs) ss (i ': is) where
+  rsubset = lens (\ss -> rget Proxy ss :& rcast ss) set
+    where
+      set :: Rec f ss -> Rec f (r ': rs) -> Rec f ss
+      set ss (r :& rs) = rput r $ rreplace rs ss
+
+-- | Two record types are equivalent when they are subtypes of each other.
+type REquivalent rs ss is js = (RSubset rs ss is, RSubset ss rs js)
+
+-- | A shorthand for 'RElem' which supplies its index.
+type r ∈ rs = RElem r rs (RIndex r rs)
+
+-- | A shorthand for 'RSubset' which supplies its image.
+type rs ⊆ ss = RSubset rs ss (RImage rs ss)
+
+-- | A shorthand for 'REquivalent' which supplies its images.
+type rs ≅ ss = REquivalent rs ss (RImage rs ss) (RImage ss rs)
+
+-- | A non-unicode equivalent of @(⊆)@.
+type rs <: ss = rs ⊆ ss
+
+-- | A non-unicode equivalent of @(≅)@.
+type rs :~: ss = rs ≅ ss
diff --git a/Data/Vinyl/Notation.hs b/Data/Vinyl/Notation.hs
--- a/Data/Vinyl/Notation.hs
+++ b/Data/Vinyl/Notation.hs
@@ -1,17 +1,17 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+
 module Data.Vinyl.Notation
-  ( (:~:)
-  , (<-:)
-  , (<:)()
-  , (<+>)
+  ( (<+>)
   , (<<*>>)
   , (<<$>>)
-  , (=:)
-  , (~=)
+  , (<<&>>)
   , Rec((:&))
-  , Semantics((:~>))
+  , type (∈)
+  , type (⊆)
+  , type (≅)
+  , type (<:)
+  , type (:~:)
   ) where
 
-import Data.Vinyl.Constraint
 import Data.Vinyl.Core
-import Data.Vinyl.Operators
-import Data.Vinyl.TH
+import Data.Vinyl.Lens
diff --git a/Data/Vinyl/Operators.hs b/Data/Vinyl/Operators.hs
deleted file mode 100644
--- a/Data/Vinyl/Operators.hs
+++ /dev/null
@@ -1,100 +0,0 @@
-{-# LANGUAGE ConstraintKinds       #-}
-{-# LANGUAGE DataKinds             #-}
-{-# LANGUAGE GADTs                 #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PolyKinds             #-}
-{-# LANGUAGE RankNTypes            #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeOperators         #-}
-
-module Data.Vinyl.Operators
-  ( (<<$>>)
-  , (<<*>>)
-  , (<+>)
-  , type (++)
-  , RecApplicative(rpure)
-  , rtraverse
-  , rdist
-  , rdistLazy
-  , FoldRec(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/TH.hs b/Data/Vinyl/TH.hs
deleted file mode 100644
--- a/Data/Vinyl/TH.hs
+++ /dev/null
@@ -1,59 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# 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
-#if __GLASGOW_HASKELL__ > 707
-          (TySynEqn [elu',u'] t')
-#else
-                    [elu',u'] t'
-#endif
diff --git a/Data/Vinyl/TyFun.hs b/Data/Vinyl/TyFun.hs
deleted file mode 100644
--- a/Data/Vinyl/TyFun.hs
+++ /dev/null
@@ -1,14 +0,0 @@
-{-# 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/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/TypeLevel.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+
+module Data.Vinyl.TypeLevel where
+
+import GHC.Exts
+
+-- | A mere approximation of the natural numbers. And their image as lifted by
+-- @-XDataKinds@ corresponds to the actual natural numbers.
+data Nat = Z | S !Nat
+
+-- | A partial relation that gives the index of a value in a list.
+type family RIndex (r :: k) (rs :: [k]) :: Nat where
+  RIndex r (r ': rs) = Z
+  RIndex r (s ': rs) = S (RIndex r rs)
+
+-- | A partial relation that gives the indices of a sublist in a larger list.
+type family RImage (rs :: [k]) (ss :: [k]) :: [Nat] where
+  RImage '[] ss = '[]
+  RImage (r ': rs) ss = RIndex r ss ': RImage rs ss
+
+-- | A constraint-former which applies to every field in a record.
+type family RecAll (f :: u -> *) (rs :: [u]) (c :: * -> Constraint) :: Constraint where
+  RecAll f '[] c = ()
+  RecAll f (r ': rs) c = (c (f r), RecAll f rs c)
+
+-- | Append for type-level lists.
+type family (as :: [k]) ++ (bs :: [k]) :: [k] where
+  '[] ++ bs = bs
+  (a ': as) ++ bs = a ': (as ++ bs)
+
diff --git a/Data/Vinyl/Universe.hs b/Data/Vinyl/Universe.hs
deleted file mode 100644
--- a/Data/Vinyl/Universe.hs
+++ /dev/null
@@ -1,7 +0,0 @@
-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
deleted file mode 100644
--- a/Data/Vinyl/Universe/Const.hs
+++ /dev/null
@@ -1,13 +0,0 @@
-{-# 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
deleted file mode 100644
--- a/Data/Vinyl/Universe/Field.hs
+++ /dev/null
@@ -1,26 +0,0 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE CPP #-}
-{-# 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 :: *)
-
-#if __GLASGOW_HASKELL__ > 707
-data SField :: * -> * where
-  SField :: KnownSymbol sy => SField (sy ::: t)
-#else
-data SField :: * -> * where
-  SField :: SingE (Kind :: Symbol) str => SField (sy ::: t)
-#endif
-
-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
deleted file mode 100644
--- a/Data/Vinyl/Universe/Id.hs
+++ /dev/null
@@ -1,13 +0,0 @@
-{-# 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
deleted file mode 100644
--- a/Data/Vinyl/Witnesses.hs
+++ /dev/null
@@ -1,29 +0,0 @@
-{-# LANGUAGE ConstraintKinds       #-}
-{-# LANGUAGE DataKinds             #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE GADTs                 #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE OverlappingInstances  #-}
-{-# LANGUAGE PolyKinds             #-}
-{-# LANGUAGE TypeOperators         #-}
-
-module Data.Vinyl.Witnesses where
-
-class Implicit p where
-  implicitly :: p
-
--- | An inductive list membership proposition.
-data Elem :: k -> [k] -> * where
-  Here  :: Elem x (x ': xs)
-  There :: Elem x xs -> Elem x (y ': xs)
-
--- | A constraint for implicit resolution of list membership proofs.
-type IElem x xs = Implicit (Elem x xs)
-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
-
diff --git a/tests/Intro.lhs b/tests/Intro.lhs
--- a/tests/Intro.lhs
+++ b/tests/Intro.lhs
@@ -19,17 +19,12 @@
 
 > {-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-}
 > {-# LANGUAGE FlexibleContexts, FlexibleInstances, NoMonomorphismRestriction #-}
-> {-# LANGUAGE GADTs, TemplateHaskell, TypeSynonymInstances #-}
+> {-# LANGUAGE GADTs, TypeSynonymInstances, TemplateHaskell, StandaloneDeriving #-}
 > import Data.Vinyl
-> 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 Control.Lens.TH
 > import Data.Char
 > import Test.DocTest
 > import Data.Singletons.TH
@@ -37,51 +32,47 @@
 Let’s define a universe of fields which we want to use:
 
 > 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 = SName =: "jon"
->    <+> SAge =: 20
->    <+> SSleeping =: False
+> type LifeForm = [Name, Age, Sleeping]
 
+> type family ElF (f :: Fields) :: * where
+>   ElF Name = String
+>   ElF Age = Int
+>   ElF Sleeping = Bool
+>   ElF Master = Rec Attr LifeForm
 
-We could make an alias for the sort of entity that jon is:
+> newtype Attr f = Attr { _unAttr :: ElF f }
+> makeLenses ''Attr
+> instance Show (Attr Name) where show (Attr x) = "name: " ++ show x
+> instance Show (Attr Age) where show (Attr x) = "age: " ++ show x
+> instance Show (Attr Sleeping) where show (Attr x) = "sleeping: " ++ show x
+> instance Show (Attr Master) where show (Attr x) = "master: " ++ show x
 
-> type LifeForm = [Name, Age, Sleeping]
-> jon :: PlainRec ElF LifeForm
+> (=:) :: sing f -> ElF f -> Attr f
+> _ =: x = Attr x
 
-We can print out the record by assigning names to each field:
+> genSingletons [ ''Fields ]
 
-> instance Implicit (PlainRec (U.Const String) [ Name, Age, Sleeping ]) where
->   implicitly = SName     =: "name"
->            <+> SAge      =: "age"
->            <+> SSleeping =: "sleeping"
+Now, let’s try to make an entity that represents a man:
 
-> -- | >>> rshow jon
-> -- "{ name =: \"jon\", age =: 20, sleeping =: False }"
+> jon = (SName =: "jon")
+>    :& (SAge =: 23)
+>    :& (SSleeping =: False)
+>    :& RNil
 
-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:
+Automatically, we can show the record:
 
-> semantics ''ElF [ 'Master :~> [t| PlainRec ElF LifeForm |] ]
+> -- |
+> -- >>> show jon
+> -- "{name: \"jon\"; age: 23; sleeping: False}"
 
-> tucker = withUniverse ElF $
->   SName =: "tucker"
->   <+> SAge =: 7
->   <+> SSleeping =: True
->   <+> SMaster =: jon
+And its types are all inferred with no problem. Now, make a dog! Dogs are
+life-forms, but unlike men, they have masters. So, let’s build my dog:
 
-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`.
+> tucker = (SName =: "tucker")
+>       :& (SAge =: 9)
+>       :& (SSleeping =: True)
+>       :& (SMaster =: jon)
+>       :& RNil
 
 Using Lenses
 ------------
@@ -92,9 +83,10 @@
 on a particular field in the record for access and update, without
 losing additional information:
 
-> wakeUp :: (Sleeping ∈ fields) => PlainRec ElF fields -> PlainRec ElF fields
-> wakeUp = SSleeping `rPut` False
 
+> wakeUp :: (Sleeping ∈ fields) => Rec Attr fields -> Rec Attr fields
+> wakeUp = rput $ SSleeping =: 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
 record that has a `Bool` field labelled `sleeping`, and modifies that
@@ -104,34 +96,29 @@
 > jon' = wakeUp jon
 
 > -- |
-> -- >>> tucker' ^. rLens SSleeping
-> -- False
+> -- >>> tucker' ^. rlens SSleeping
+> -- sleeping: False
 > --
-> -- >>> tucker ^. rLens SSleeping
-> -- True
+> -- >>> tucker ^. rlens SSleeping
+> -- sleeping: True
 > --
-> -- >>> jon' ^. rLens SSleeping
-> -- False
+> -- >>> jon' ^. rlens SSleeping
+> -- sleeping: 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 ∈ fields) => Lens' (PlainRec ElF fields) Bool
-> masterSleeping = rLens SMaster . rLens SSleeping
-> tucker'' = masterSleeping .~ True $ tucker'
-
+> masterSleeping = rlens SMaster . unAttr . rlens SSleeping
+> tucker'' = masterSleeping .~ (SSleeping =: True) $ tucker'
 
 > -- | >>> tucker'' ^. masterSleeping
-> -- True
-
-Again, the type annotation is unnecessary.
-
+> -- sleeping: True
 
 Subtyping Relation and Coercion
 -------------------------------
 
-A record `PlainRec xs` is a subtype of a record `PlainRec ys` if `ys ⊆ xs`;
+A record `Rec f xs` is a subtype of a record `Rec f ys` if `ys ⊆ xs`;
 that is to say, if one record can do everything that another record
 can, the former is a subtype of the latter. As such, we should be able
 to provide an upcast operator which “forgets” whatever makes one
@@ -140,73 +127,80 @@
 
 Therefore, the following works:
 
-> upcastedTucker :: PlainRec ElF LifeForm
-> upcastedTucker = cast (toPlainRec tucker)
-
-The reason for using `toPlainRec` will become clear a bit later.
+> upcastedTucker :: Rec Attr LifeForm
+> upcastedTucker = rcast tucker
 
 The subtyping relationship between record types is expressed with the
 `(<:)` constraint; so, cast is of the following type:
 
-< cast :: r1 <: r2 => Rec r1 f -> Rec r2 f
+< rcast :: r1 <: r2 => Rec f r1 -> Rec f r2
 
 Also provided is a `(≅)` constraint which indicates record congruence
 (that is, two record types differ only in the order of their fields).
 
+In fact, `rcast` is actually given as a special case of the lens `rsubset`,
+which lets you modify entire (possibly non-contiguous) slices of a record!
+
 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
-this:
+Consider the following declaration:
 
-< data Rec :: (TyFun u * -> *) -> (* -> *) -> [u] -> * where
-<   RNil :: Rec el f '[]
-<   (:&) :: f (el $ r) -> Rec el f rs -> Rec el f (r ': rs)
+< data Rec :: (u -> *) -> [u] -> * where
+<   RNil :: Rec f '[]
+<   (:&) :: f r -> Rec f rs -> Rec 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
-`Identity`. Let’s try and motivate this stuff with an example.
+Records are implicitly parameterized over a kind `u`, which stands for the
+"universe" or key space. Keys (inhabitants of `u`) are then interpreted into
+the types of their values by the first parameter to `Rec`, `f`. An extremely
+powerful aspect of Vinyl records is that you can construct natural
+transformations between different interpretation functors `f,g`, or postcompose
+some other functor onto the stack. This can be used to immerse each field of a
+record in some particular effect modality, and then the library functions can
+be used to traverse and accumulate these effects.
 
 Let’s imagine that we want to do validation on a record that
 represents a name and an age:
 
 > 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.
+We’ve decided that names must be alphabetic, and ages must be positive. For
+validation, we’ll use `Maybe` for now, though you should use a
+left-accumulating `Validation` type.
 
-> goodPerson :: PlainRec ElF Person
-> goodPerson = SName =: "Jon"
->          <+> SAge  =: 20
-> badPerson = SName =: "J#@#$on"
->         <+> SAge  =: 20
+> goodPerson :: Rec Attr Person
+> goodPerson = (SName =: "Jon")
+>           :& (SAge =: 20)
+>           :& RNil
 
-> 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)
+> badPerson = (SName =: "J#@#$on")
+>           :& (SAge =: 20)
+>           :& RNil
+
+We'll give validation a (rather poor) shot.
+
+> validatePerson :: Rec Attr Person -> Maybe (Rec Attr Person)
+> validatePerson p = (\n a -> (SName =: n) :& (SAge =: a) :& RNil) <$> vName <*> vAge where
+>   vName = validateName $ p ^. rlens SName . unAttr
+>   vAge  = validateAge $ p ^. rlens SAge . unAttr
 >
->   validateName str | all isAlpha str = Success str
->   validateName _ = Failure [ "name must be alphabetic" ]
->   validateAge i | i >= 0 = Success i
->   validateAge _ = Failure [ "age must be positive" ]
+>   validateName str | all isAlpha str = Just str
+>   validateName _ = Nothing
+>   validateAge i | i >= 0 = Just i
+>   validateAge _ = Nothing
 
 > -- $setup
-> -- >>> let isSuccess (Success _) = True; isSuccess _ = False
+> -- >>> let isJust (Just _) = True; isJust _ = False
 
 > -- |
-> -- >>> isSuccess $ validatePerson goodPerson
+> -- >>> isJust $ validatePerson goodPerson
 > -- True
 > --
-> -- >>> isSuccess $ validatePerson badPerson
+> -- >>> isJust $ validatePerson badPerson
 > -- False
 
-The results are as expected (`Success` for `goodPerson`, and a
-`Failure` with one error for `badPerson`); but this was not very fun
-to build.
+The results are as expected (`Just` for `goodPerson`, and a `Nothing` for
+`badPerson`); but this was not very fun to build.
 
 Further, it would be nice to have some notion of a partial record;
 that is, if part of it can’t be validated, it would still be nice to
@@ -215,21 +209,19 @@
 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 the class of functions from the
-`Identity` functor to the `Result` functor at some type.
-
-< type Validator e = Lift (->) Identity ~> Result e
+> type Validator f = Lift (->) f (Maybe :. f)
 
 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 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" ]
-
+> vperson :: Rec (Validator Attr) Person
+> vperson = lift validateName :& lift validateAge :& RNil
+>   where
+>     lift f = Lift $ Compose . f
+>     validateName (Attr str) | all isAlpha str = Just (Attr str)
+>     validateName _ = Nothing
+>     validateAge (Attr i) | i >= 0 = Just (Attr i)
+>     validateAge _ = Nothing
 
 And we can use the special application operator `<<*>>` (which is
 analogous to `<*>`, but generalized a bit) to use this to validate a
@@ -238,56 +230,31 @@
 > goodPersonResult = vperson <<*>> goodPerson
 > badPersonResult  = vperson <<*>> badPerson
 
-< goodPersonResult === SName :=: Success "Jon", SAge :=: Success 20, {}
-< badPersonResult  === SName :=: Failure ["name must be alphabetic"], SAge :=: Success 20, {}
-
 > -- |
-> -- >>> isSuccess $ goodPersonResult ^. rLens' SName
+> -- >>> isJust . getCompose $ goodPersonResult ^. rlens SName
 > -- True
-> -- >>> isSuccess $ goodPersonResult ^. rLens' SAge
+> -- >>> isJust . getCompose $ goodPersonResult ^. rlens SAge
 > -- True
-> -- >>> isSuccess $ badPersonResult ^. rLens' SName
+> -- >>> isJust . getCompose $ badPersonResult ^. rlens SName
 > -- False
-> -- >>> isSuccess $ badPersonResult ^. rLens' SAge
+> -- >>> isJust . getCompose $ 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 `rdist`:
 
-> distGoodPerson = rdist goodPersonResult
-> distBadPerson  = rdist badPersonResult
+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 `Maybe (Rec Attr Person)`) using `rtraverse`:
 
-< distGoodPerson === Success name :=: "Jon", age :=: 20, {}
-< distBadPerson  === Failure ["name must be alphabetic"]
+> mgoodPerson :: Maybe (Rec Attr Person)
+> mgoodPerson = rtraverse getCompose goodPersonResult
 
+> mbadPerson  = rtraverse getCompose badPersonResult
+
 > -- |
-> -- >>> isSuccess distGoodPerson
+> -- >>> isJust mgoodPerson
 > -- True
-> -- >>> isSuccess distBadPerson
+> -- >>> isJust mbadPerson
 > -- False
 
-Fixing a polymorphic record into the Identity Functor
------------------------------------------------------
-
-If you produced a record using `(=:)` and `(<+>)` without providing a
-type annotation, then its type is something like this:
-
-< 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, `toPlainRec` is
-provided:
-
-< toPlainRec :: (forall f. Applicative f => Rec el f rs) -> PlainRec el rs
-
----
-
-(We must define a main value for doctest to run.)
-
 > 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.4.3
+version:             0.5
 synopsis:            Extensible Records
 -- description:
 license:             MIT
@@ -21,23 +21,12 @@
 library
   exposed-modules:     Data.Vinyl
                      , Data.Vinyl.Core
-                     , Data.Vinyl.Operators
                      , Data.Vinyl.Lens
                      , Data.Vinyl.Derived
-                     , Data.Vinyl.Witnesses
-                     , Data.Vinyl.Constraint
-                     , Data.Vinyl.Idiom.Validation
-                     , Data.Vinyl.Idiom.Identity
-                     , Data.Vinyl.Idiom.Thunk
-                     , Data.Vinyl.TyFun
+                     , Data.Vinyl.TypeLevel
                      , Data.Vinyl.Functor
                      , Data.Vinyl.Notation
-                     , 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.7.0.0
+  build-depends:       base >=4.7 && <= 5, ghc-prim
   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
 
@@ -45,7 +34,7 @@
   type:             exitcode-stdio-1.0
   hs-source-dirs:   benchmarks
   main-is:          StorableBench.hs
-  build-depends:    base >= 4.6 && <= 5, vector, criterion, vinyl == 0.4.3, mwc-random, lens, linear
+  build-depends:    base >= 4.7 && <= 5, vector, criterion, vinyl == 0.5, mwc-random, lens, linear
   ghc-options:      -O2 -fllvm
   default-language: Haskell2010
 
@@ -53,5 +42,5 @@
   type:             exitcode-stdio-1.0
   hs-source-dirs:   tests
   main-is:          Intro.lhs
-  build-depends:    base >= 4.6 && <= 5, lens, vinyl == 0.4.3, doctest >= 0.8, singletons >= 0.10
+  build-depends:    base >= 4.7 && <= 5, lens, vinyl == 0.5, doctest >= 0.8, singletons >= 0.10
   default-language: Haskell2010