diff --git a/bookkeeper.cabal b/bookkeeper.cabal
--- a/bookkeeper.cabal
+++ b/bookkeeper.cabal
@@ -3,7 +3,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           bookkeeper
-version:        0.1.2.0
+version:        0.2.0.0
 description:    Please see README.md
 homepage:       http://github.com/turingjump/bookkeeper#readme
 bug-reports:    https://github.com/turingjump/bookkeeper/issues
@@ -30,8 +30,8 @@
     , type-level-sets
   exposed-modules:
       Bookkeeper
-      Bookkeeper.Errors
       Bookkeeper.Internal
+      Bookkeeper.Internal.Errors
   default-language: Haskell2010
 
 executable readme
diff --git a/src/Bookkeeper.hs b/src/Bookkeeper.hs
--- a/src/Bookkeeper.hs
+++ b/src/Bookkeeper.hs
@@ -37,10 +37,6 @@
   -- * Re-exports
   , (&)
 
-  -- * For coercion
-  -- | These types should not be used, but need to be in scope for coercion,
-  -- which is used when setting or modifying a value.
-  , ChooseFirst(..)
   ) where
 
 import Bookkeeper.Internal
diff --git a/src/Bookkeeper/Errors.hs b/src/Bookkeeper/Errors.hs
deleted file mode 100644
--- a/src/Bookkeeper/Errors.hs
+++ /dev/null
@@ -1,20 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
-module Bookkeeper.Errors where
-
-import qualified Data.Type.Map as Map
-import GHC.TypeLits (TypeError, ErrorMessage(..))
-import GHC.Exts
-
-type Contains book field exp = Contains' book field book exp
-
-type family Contains' book field orig exp :: Constraint where
-   Contains' '[] field '[] exp = TypeError (Text "The provided Book is empty!")
-   Contains' '[] field orig exp
-      = TypeError (Text "The provided Book does not contain the field "
-              :<>: ShowType field
-              :$$: Text "Book type:"
-              :$$: ShowType orig
-              )
-   Contains' ((k Map.:-> v) ': m) k orig exp = (v ~ exp)
-   Contains' (any ': m) k     orig exp = Contains' m k orig exp
diff --git a/src/Bookkeeper/Internal.hs b/src/Bookkeeper/Internal.hs
--- a/src/Bookkeeper/Internal.hs
+++ b/src/Bookkeeper/Internal.hs
@@ -8,13 +8,15 @@
 import GHC.TypeLits (Symbol, KnownSymbol)
 import Data.Kind (Type)
 import Data.Type.Map (Map, Mapping((:->)))
-import Data.Coerce
-import Data.Proxy
 import Data.Monoid ((<>))
 import Data.List (intercalate)
 
-import Bookkeeper.Errors
+import Bookkeeper.Internal.Errors
 
+------------------------------------------------------------------------------
+-- Book
+------------------------------------------------------------------------------
+
 -- Using a type synonym allows the user to write the fields in any order, and
 -- yet have the underlying value always have sorted fields.
 type Book a = Book' (Map.AsMap a)
@@ -39,19 +41,29 @@
          ) => ShowHelper (Book' ((k :=> v) ': xs)) where
   showHelper (Book (Map.Ext k v rest)) = (show k, show v):showHelper (Book rest)
 
+instance Eq (Book' '[]) where
+  _ == _ = True
 
+instance (Eq val, Eq (Book' xs)) => Eq (Book' ((field :=> val) ': xs)  ) where
+  Book (Map.Ext _ a as) == Book (Map.Ext _ b bs) = a == b && Book as == Book bs
+
+instance Monoid (Book' '[]) where
+  mempty = emptyBook
+  _ `mappend` _ = emptyBook
+
 -- | A book with no records. You'll usually want to use this to construct
 -- books.
 emptyBook :: Book '[]
 emptyBook = Book Map.Empty
 
+------------------------------------------------------------------------------
+-- Other types
+------------------------------------------------------------------------------
+
 -- | An alias for ':->' because otherwise you'll have to tick your
 -- constructors.
 type a :=> b = a ':-> b
 
-instance Monoid (Book' '[]) where
-  mempty = emptyBook
-  _ `mappend` _ = emptyBook
 
 instance (s ~ s') => IsLabel s (Key s') where
   fromLabel _ = Key
@@ -61,6 +73,10 @@
 data Key (a :: Symbol) = Key
   deriving (Eq, Show, Read, Generic)
 
+------------------------------------------------------------------------------
+-- Setters and getters
+------------------------------------------------------------------------------
+
 -- | Get a value by key, if it exists.
 --
 -- >>> get #age julian
@@ -92,34 +108,30 @@
 --
 -- >>> set #likesDoctest True julian
 -- Book {age = 28, likesDoctest = True, name = "Julian K. Arni"}
-set :: forall field val old mid1 mid2 new .
-  ( Map.Unionable '[field :=> ChooseFirst val] mid1
-  , Mappable ChooseFirst old mid1
-  , Mappable ChooseFirst new mid2
-  , mid1 ~ (MapThere ChooseFirst old)
-  , mid2 ~ (Map.Union '[field :=> ChooseFirst val] mid1)
-  , new ~ MapBack ChooseFirst mid2
+set :: forall field val old deleted added new .
+  ( Map.Submap deleted old
+  , deleted ~ (Map.AsMap (old Map.:\ field))
+  , added ~ (( field :=> val) ': deleted)
+  , Map.Unionable '[ field :=> val] deleted
+  , new ~ Map.AsMap added
   )
   => Key field -> val -> Book' old -> Book' new
-set _ v (Book bk)
-    = Book $ mapBack p
-           $ Map.union new
-           $ mapThere p bk
+set p v old = Book new
   where
-    new = Map.Ext (Map.Var :: Map.Var field) (ChooseFirst v) Map.Empty
-    p = Proxy :: Proxy ChooseFirst
+    Book deleted = delete p old
+    added = Map.Ext (Map.Var :: Map.Var field) v deleted
+    new = Map.asMap added
 
 -- | Infix version of 'set'
 --
 -- >>> julian & #age =: 29
 -- Book {age = 29, name = "Julian K. Arni"}
-(=:) :: forall field val old mid1 mid2 new .
-  ( Map.Unionable '[field :=> ChooseFirst val] mid1
-  , Mappable ChooseFirst old mid1
-  , Mappable ChooseFirst new mid2
-  , mid1 ~ (MapThere ChooseFirst old)
-  , mid2 ~ (Map.Union '[field :=> ChooseFirst val] mid1)
-  , new ~ MapBack ChooseFirst mid2
+(=:) :: forall field val old deleted added new .
+  ( Map.Submap deleted old
+  , deleted ~ (Map.AsMap (old Map.:\ field))
+  , added ~ (( field :=> val) ': deleted)
+  , Map.Unionable '[ field :=> val] deleted
+  , new ~ Map.AsMap added
   )
   => Key field -> val -> Book' old -> Book' new
 (=:) = set
@@ -139,16 +151,17 @@
 -- ...    '["age" ':-> Int, "name" ':-> String]
 -- ...  • In the expression: modify #height (\ _ -> 132) julian
 -- ...
-modify :: forall field val val' old mid1 mid2 new .
-  ( Map.Unionable '[field :=> ChooseFirst val'] mid1
-  , Mappable ChooseFirst old mid1
-  , Mappable ChooseFirst new mid2
-  , (Map.Submap '[field :=> val] old
-  , Contains old field val )
-  , mid1 ~ (MapThere ChooseFirst old)
-  , mid2 ~ (Map.Union '[field :=> ChooseFirst val'] mid1)
-  , new ~ MapBack ChooseFirst mid2
+modify :: forall field val val' old deleted added new .
+  -- For setting
+  ( Map.Submap deleted old
+  , deleted ~ (Map.AsMap (old Map.:\ field))
+  , added ~ (( field :=> val') ': deleted)
+  , Map.Unionable '[ field :=> val'] deleted
+  , new ~ Map.AsMap added
   , Map.AsMap new ~ new
+  -- For getting
+  , Contains old field val
+  , Map.Submap '[ field :=> val] old
   ) =>  Key field -> (val -> val') -> Book' old -> Book new
 modify p f b = set p v b
   where v = f $ get p b
@@ -157,16 +170,17 @@
 --
 -- >>> julian & #name %: fmap toUpper
 -- Book {age = 28, name = "JULIAN K. ARNI"}
-(%:) :: forall field val val' old mid1 mid2 new .
-  ( Map.Unionable '[field :=> ChooseFirst val'] mid1
-  , Mappable ChooseFirst old mid1
-  , Mappable ChooseFirst new mid2
-  , (Map.Submap '[field :=> val] old
-  , Contains old field val )
-  , mid1 ~ (MapThere ChooseFirst old)
-  , mid2 ~ (Map.Union '[field :=> ChooseFirst val'] mid1)
-  , new ~ MapBack ChooseFirst mid2
+(%:) :: forall field val val' old deleted added new .
+  -- For setting
+  ( Map.Submap deleted old
+  , deleted ~ (Map.AsMap (old Map.:\ field))
+  , added ~ (( field :=> val') ': deleted)
+  , Map.Unionable '[ field :=> val'] deleted
+  , new ~ Map.AsMap added
   , Map.AsMap new ~ new
+  -- For getting
+  , Contains old field val
+  , Map.Submap '[ field :=> val] old
   ) =>  Key field -> (val -> val') -> Book' old -> Book new
 (%:) = modify
 infixr 3 %:
@@ -186,53 +200,6 @@
         ( Map.Submap (Map.AsMap (old Map.:\ field)) old
         ) => Key field -> Book' old -> Book (old Map.:\ field)
 delete _ (Book bk) = Book $ Map.submap bk
-
-
-
--- * Mapping
---
--- | In order to be able to establish how maps are to combined, we need to a
--- little song and dance.
-
-type family MapThere (f :: Type -> Type) (map :: [Mapping Symbol Type])  where
-  MapThere f '[] = '[]
-  MapThere f ((k :=> a) ': as) = (k :=> f a) ': MapThere f as
-
-type family MapBack f (map :: [Mapping Symbol Type]) where
-  MapBack f '[] = '[]
-  MapBack f ((k :=> f a) ': as) =  k :=> a ': MapBack f as
-
-class (MapThere f a ~ b, MapBack f b ~ a ) => Mappable f a b | f a -> b, f b -> a where
-  mapThere :: proxy f -> Map a -> Map b
-  mapBack :: proxy f -> Map b -> Map a
-
-instance Mappable f '[] '[] where
-  mapThere _ x = x
-  mapBack _  x = x
-
-instance (Coercible a (f a), Coercible (f a) a, Mappable f as fas )
-  => Mappable f ((k :=> a) ': as) ((k :=> f a) ': fas) where
-  mapThere p (Map.Ext v k r) = Map.Ext v (coerce k) $ mapThere p r
-  mapBack p (Map.Ext v k r) = Map.Ext v (coerce k) $ mapBack p r
-
-
-class MapMap f map where
-  type MapMapT f map :: [Mapping Symbol Type]
-  mapMap :: f -> Map map -> Map (MapMapT f map)
-
-
-instance MapMap f '[] where
-  type MapMapT f '[] = '[]
-  mapMap _ m = m
-
-{-#  WARNING ChooseFirst "This should not be used" #-}
-newtype ChooseFirst a = ChooseFirst { getChooseFirst :: a }
- deriving (Eq, Show, Read, Generic)
-
-instance Map.Combinable (ChooseFirst a) (ChooseFirst b) where
-  combine a _ = a
-
-type instance Map.Combine (ChooseFirst a) (ChooseFirst b) = ChooseFirst a
 
 
 -- $setup
diff --git a/src/Bookkeeper/Internal/Errors.hs b/src/Bookkeeper/Internal/Errors.hs
new file mode 100644
--- /dev/null
+++ b/src/Bookkeeper/Internal/Errors.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+module Bookkeeper.Internal.Errors where
+
+import qualified Data.Type.Map as Map
+import GHC.TypeLits (TypeError, ErrorMessage(..))
+import GHC.Exts
+
+type Contains book field exp = Contains' book field book exp
+
+type family Contains' book field orig exp :: Constraint where
+   Contains' '[] field '[] exp = TypeError (Text "The provided Book is empty!")
+   Contains' '[] field orig exp
+      = TypeError (Text "The provided Book does not contain the field "
+              :<>: ShowType field
+              :$$: Text "Book type:"
+              :$$: ShowType orig
+              )
+   Contains' ((k Map.:-> v) ': m) k orig exp = (v ~ exp)
+   Contains' (any ': m) k     orig exp = Contains' m k orig exp
diff --git a/test/BookkeeperSpec.hs b/test/BookkeeperSpec.hs
--- a/test/BookkeeperSpec.hs
+++ b/test/BookkeeperSpec.hs
@@ -2,6 +2,7 @@
 
 import Data.Char (toUpper)
 import Test.Hspec
+import Test.QuickCheck
 
 import Bookkeeper
 
@@ -46,6 +47,12 @@
 
     it "has a decent show instance" $ do
       show p `shouldBe` "Book {age = 28, name = \"Julian K. Arni\"}"
+
+    it "obeys the 'get . put' law" $ property $ \(x :: Int) -> do
+      get #label (set #label x emptyBook) `shouldBe` x
+
+    it "obeys the 'put . put' law" $ property $ \(x :: Int) (y :: Int) -> do
+      set #label y (set #label x emptyBook) `shouldBe` set #label y emptyBook
 
 type Person = Book '[ "name" :=> String , "age" :=> Int]