diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,2 +1,132 @@
 # justified-containers
 Standard containers, with keys that carry evidence of their own presence.
+
+# Description
+
+Have you ever *known* that a key could be found in a certain map? Were you tempted to
+reach for `fromJust` or `error` to handle the "impossible" case, when you knew that
+`lookup` should give `Just v`? (and did shifting requirements ever make the impossible
+become possible after all?)
+
+`Data.Map.Justified` provides a wrapper around `Data.Map`s `Data.Map.Map` that enables you
+to separate the *proof that a key is present* from the *operations using the key*. Once
+you prove that a key is present, you can use it `Maybe`-free in any number of other
+operations -- sometimes even operations on other maps!
+
+None of the functions in this module can cause a run-time error, and very few
+of the operations return a `Maybe` value.
+
+See the `Data.Map.Justified.Tutorial` module for usage examples.
+
+```haskell
+    withMap test_table $ \\table -> do
+    
+      case member 1 table of
+    
+        Nothing  -> putStrLn "Sorry, I couldnt prove that the key is present."
+    
+        Just key -> do
+          -- In this do-block, \key\ represents the key 1, but carries type-level
+          -- evidence that the key is present. Lookups and updates can now proceed
+          -- without the possibility of error.
+          putStrLn ("Found key: " ++ show key)
+    
+          -- lookup returns a value directly, not a \Maybe\!
+          putStrLn ("Value for key: " ++ lookup key table)
+    
+          -- If you update an already-mapped value, the set of valid keys does
+          -- not change. So the evidence that 'key' could be found in 'table'
+          -- is still sufficient to ensure that 'key' can be found in the updated
+          -- table as well.
+          let table = reinsert key "howdy" table
+          putStrLn ("Value for key in updated map: " ++ lookup key table)
+```
+
+Output:
+
+    Found key: Key 1
+    Value for key: hello
+    Value for key in updated map: howdy
+
+## Motivation: `Data.Map` and `Maybe` values
+
+Suppose you have a key-value mapping using `Data.Map`s type `Data.Map.Map k v`. Anybody making
+use of `Data.Map.Map k v` to look up or modify a value must take into account the possibility
+that the given key is not present.
+
+In `Data.Map`, there are two strategies for dealing with absent keys:
+
+  1. Cause a runtime error (e.g. `Data.Map`s `Data.Map.!` when the key is absent)
+
+  2. Return a `Maybe` value (e.g. `Data.Map`s `Data.Map.lookup`)
+
+The first option introduces partial functions, so is not very palatable. But what is
+wrong with the second option?
+
+To understand the problem with returning a `Maybe` value, lets ask what the  `Maybe v` in
+
+```haskell
+    lookup :: k -> Map k v -> Maybe v
+```
+
+really does for us. By returning
+a `Maybe v` value, `lookup key table` is saying "Your program must account
+for the possibility that `key` cannot be found in `table`. I will ensure that you
+account for this possibility by forcing you to handle the `Nothing` case."
+In effect, `Data.Map` is requiring the user to prove they have handled the
+possibility that a key is absent whenever they use the `Data.Map.lookup` function.
+
+## Laziness (the bad kind)
+
+Every programmer has probably had the experience of knowing, somehow, that a certain
+key is going to be present in a map. In this case, the `Maybe v` feels like a burden:
+I already *know* that this key is in the map, why should I have to handle the `Nothing` case?
+
+In this situation, it is tempting to reach for the partial function `Data.Maybe.fromJust`,
+or a pattern match like `Nothing -> error "The impossible happened!"`. But as parts of
+the program are changed over time, you may find the impossible has become possible after
+all (or perhaps youll see the dreaded and unhelpful `*** Exception: Maybe.fromJust: Nothing`)
+
+It is tempting to reach for partial functions or "impossible" runtime errors here, because
+the programmer has proven that the key is a member of the map in some other way. They
+know that `Data.Map.lookup` should return a `Just v` --- but the *compiler* doesnt know this!
+
+The idea behind `Data.Map.Justified` is to encode the programmers knowledge that a key
+is present *within the type system*, where it can be checked at compile-time. Once a key
+is known to be present, `Data.Map.Justified.lookup` will never fail. Your justification
+removes the `Just`!
+
+# How it works
+
+Evidence that a key can indeed be found in a map is carried by a phantom type parameter `ph`
+shared by both the `Data.Map.Justified.Map` and `Data.Map.Justified.Key` types. If you are
+able to get your hands on a value of type `Key ph k`, then you must have already proven that
+the key is present in *any* value of type `Map ph k v`.
+
+The `Key ph k` type is simply a `newtype` wrapper around `k`, but the phantom type `ph` allows
+`Key ph k` to represent both *a key of type `k`* __and__ *a proof that the key is present in*
+*all maps of type `Map ph k v`*.
+
+There are several ways to prove that a key belongs to a map, but the simplest is to just use
+`Data.Map.Justified`s `Data.Map.Justified.member` function. In `Data.Map`, `Data.Map.member`
+has the type
+
+```haskell
+    member :: Ord k => k -> Map k v -> Bool
+```
+
+and reports whether or not the key can be found in the map. In `Data.Map.Justified`,
+`Data.Map.Member` has the type
+
+```haskell
+    member :: Ord k => k -> Map ph k v -> Maybe (Key ph k)
+```
+
+Instead of a boolean, `Data.Map.Justified.member` either says `the key is not present`
+(`Nothing`), or gives back the same key, *augmented with evidence that they key*
+*is present*. This key-plus-evidence can then be used to do any number of `Maybe`-free
+operations on the map.
+
+`Data.Map.Justified` uses the same rank-2 polymorphism trick used in the `Control.Monad.ST` monad to
+ensure that the `ph` phantom type can not be extracted; in effect, the proof that a key is
+present can't leak to contexts where the proof would no longer be valid.
diff --git a/justified-containers.cabal b/justified-containers.cabal
--- a/justified-containers.cabal
+++ b/justified-containers.cabal
@@ -1,5 +1,5 @@
 name:                justified-containers
-version:             0.1.0.0
+version:             0.1.1.0
 synopsis:            Keyed container types with verified keys.
 description:         This package contains wrappers around standard container types,
                      that provide guarantees about the presence of keys within the
diff --git a/src/Data/Map/Justified.hs b/src/Data/Map/Justified.hs
--- a/src/Data/Map/Justified.hs
+++ b/src/Data/Map/Justified.hs
@@ -8,86 +8,126 @@
 --
 -- = Description
 --
--- A wrapper around "Data.Map"'s 'Data.Map.Map' for shifting the burden of proof that a key
--- exists in a map from "lookup time" to "key creation time".
+-- Have you ever /known/ that a key could be found in a certain map? Were you tempted to
+-- reach for @'fromJust'@ or @'error'@ to handle the "impossible" case, when you knew that
+-- @'lookup'@ should give @'Just' v@? (and did shifting requirements ever make the impossible
+-- become possible after all?)
 --
--- == Motivation: "Data.Map" and 'Maybe' values
+-- "Data.Map.Justified" provides a wrapper around "Data.Map"'s @'Data.Map.Map'@ that enables you
+-- to separate the /proof that a key is present/ from the /operations using the key/. Once
+-- you prove that a key is present, you can use it @Maybe@-free in any number of other
+-- operations -- sometimes even operations on other maps!
 --
--- Suppose you have a key-value mapping using "Data.Map"'s type @Map k v@. Anybody making
--- use of @Map k v@ to look up or modify a value must take into account the possibility
+-- None of the functions in this module can cause a run-time error, and very few
+-- of the operations return a @'Maybe'@ value.
+--
+-- See the 'Data.Map.Justified.Tutorial' module for usage examples.
+--
+-- @
+--  withMap test_table $ \\table -> do
+--  
+--    case member 1 table of
+--
+--      Nothing  -> putStrLn "Sorry, I couldn't prove that the key is present."
+--
+--      Just key -> do
+--        -- In this do-block, \'key\' represents the key 1, but carries type-level
+--        -- evidence that the key is present. Lookups and updates can now proceed
+--        -- without the possibility of error.
+--        putStrLn ("Found key: " ++ show key)
+--  
+--        -- lookup returns a value directly, not a \'Maybe\'!
+--        putStrLn ("Value for key: " ++ lookup key table)
+--  
+--        -- If you update an already-mapped value, the set of valid keys does
+--        -- not change. So the evidence that \'key\' could be found in \'table\'
+--        -- is still sufficient to ensure that \'key\' can be found in the updated
+--        -- table as well.
+--        let table' = reinsert key "howdy" table
+--        putStrLn ("Value for key in updated map: " ++ lookup key table')
+-- @
+-- Output:
+--
+-- @
+--  Found key: Key 1
+--  Value for key: hello
+--  Value for key in updated map: howdy
+-- @
+--
+-- == Motivation: "Data.Map" and @'Maybe'@ values
+--
+-- Suppose you have a key-value mapping using "Data.Map"'s type @'Data.Map.Map' k v@. Anybody making
+-- use of @'Data.Map.Map' k v@ to look up or modify a value must take into account the possibility
 -- that the given key is not present.
 --
 -- In "Data.Map", there are two strategies for dealing with absent keys:
 --
---   1. Cause a runtime error (e.g. "Data.Map"'s 'Data.Map.!' when the key is absent)
+--   1. Cause a runtime error (e.g. "Data.Map"'s @'Data.Map.!'@ when the key is absent)
 --
---   2. Return a 'Maybe' value (e.g. "Data.Map"'s 'Data.Map.lookup')
+--   2. Return a @'Maybe'@ value (e.g. "Data.Map"'s @'Data.Map.lookup'@)
 --
 -- The first option introduces partial functions, so is not very palatable. But what is
 -- wrong with the second option?
 --
--- To understand the problem with returning a 'Maybe' value, let's ask what returning
--- @Maybe v@ from @lookup :: k -> Map k v -> Maybe v@ really does for us. By returning
+-- To understand the problem with returning a @'Maybe'@ value, let's ask what returning
+-- @Maybe v@ from @'Data.Map.lookup' :: k -> Map k v -> Maybe v@ really does for us. By returning
 -- a @Maybe v@ value, @lookup key table@ is saying "Your program must account
 -- for the possibility that @key@ cannot be found in @table@. I will ensure that you
--- account for this possibility by forcing you to handle the 'Nothing' case."
+-- account for this possibility by forcing you to handle the @'Nothing'@ case."
 -- In effect, "Data.Map" is requiring the user to prove they have handled the
--- possibility that a key is absent whenever they use the 'Data.Map.lookup' function.
+-- possibility that a key is absent whenever they use the @'Data.Map.lookup'@ function.
 --
 -- == Laziness (the bad kind)
 --
 -- Every programmer has probably had the experience of knowing, somehow, that a certain
--- key is going to be present in a map. In this case, the @Maybe v@ feels like a burden:
--- I already /know/ that this key is in the map, why should I handle the 'Nothing' case?
+-- key is going to be present in a map. In this case, the @'Maybe' v@ feels like a burden:
+-- I already /know/ that this key is in the map, why should I have to handle the @'Nothing'@ case?
 --
--- In this situation, it is tempting to reach for the partial function 'Data.Maybe.fromJust',
--- or a pattern match like @Nothing -> error "The impossible happened!"@. But as parts of
+-- In this situation, it is tempting to reach for the partial function @'Data.Maybe.fromJust'@,
+-- or a pattern match like @'Nothing' -> 'error' "The impossible happened!"@. But as parts of
 -- the program are changed over time, you may find the impossible has become possible after
 -- all (or perhaps you'll see the dreaded and unhelpful @*** Exception: Maybe.fromJust: Nothing@)
 --
 -- It is tempting to reach for partial functions or "impossible" runtime errors here, because
 -- the programmer has proven that the key is a member of the map in some other way. They
--- know that 'Data.Map.lookup' should return a 'Just v' --- but the /compiler/ doesn't know this!
+-- know that @'Data.Map.lookup'@ should return a @'Just' v@ --- but the /compiler/ doesn't know this!
 --
 -- The idea behind "Data.Map.Justified" is to encode the programmer's knowledge that a key
--- is present, within the type system where it can be checked at compile-time. Once a key
--- is known to be present, 'Data.Map.Justified.lookup' will never fail. Your justification
--- removes the 'Just'!
+-- is present /within the type system/, where it can be checked at compile-time. Once a key
+-- is known to be present, @'Data.Map.Justified.lookup'@ will never fail. Your justification
+-- removes the @'Just'@!
 --
 -- == How it works
 --
 -- Evidence that a key can indeed be found in a map is carried by a phantom type parameter @ph@
--- shared by both the 'Data.Map.Justified.Map' and 'Data.Map.Justified.Key' types. If you are
--- able to get your hands on a value of type @Key ph k@, then you must have already proven that
--- the key is present in /any/ value of type @Map ph k v@.
+-- shared by both the @'Data.Map.Justified.Map'@ and @'Data.Map.Justified.Key'@ types. If you are
+-- able to get your hands on a value of type @'Key' ph k@, then you must have already proven that
+-- the key is present in /any/ value of type @'Map' ph k v@.
 --
--- The @Key ph k@ type is simply a @newtype@ wrapper around @k@, but the phantom type @ph@ allows
--- @Key ph k@ to represent both /a key of type @k@/ __and__ /a proof that the key is present in
--- maps of type @Map ph k v@/.
+-- The @'Key' ph k@ type is simply a @newtype@ wrapper around @k@, but the phantom type @ph@ allows
+-- @'Key' ph k@ to represent both /a key of type @k@/ __and__ /a proof that the key is present in/
+-- /all maps of type @'Map' ph k v@/.
 --
 -- There are several ways to prove that a key belongs to a map, but the simplest is to just use
--- "Data.Map.Justified"'s 'Data.Map.Justified.member' function. In "Data.Map", 'Data.Map.member'
+-- "Data.Map.Justified"'s @'Data.Map.Justified.member'@ function. In "Data.Map", @'Data.Map.member'@
 -- has the type
 --
--- @member :: Ord k => k -> Map k v -> Bool@
+-- @'Data.Map.member' :: 'Ord' k => k -> 'Data.Map.Map' k v -> 'Bool'@
 --
 -- and reports whether or not the key can be found in the map. In "Data.Map.Justified",
--- 'Data.Map.Member' has the type
+-- @'Data.Map.Member'@ has the type
 --
--- @member :: Ord k => k -> Map ph k v -> Maybe (Key ph k)@
+-- @'member' :: 'Ord' k => k -> 'Map' ph k v -> 'Maybe' ('Key' ph k)@
 --
--- Instead of a boolean, 'Data.Map.Justified.member' either says "the key is not present"
--- ('Nothing'), or gives back the same key, /augmented with evidence that they key/
--- /is present/. This key-plus-evidence can then be used to do any number of 'Maybe'-free
+-- Instead of a boolean, @'Data.Map.Justified.member'@ either says "the key is not present"
+-- (@'Nothing'@), or gives back the same key, /augmented with evidence that they key/
+-- /is present/. This key-plus-evidence can then be used to do any number of @'Maybe'@-free
 -- operations on the map.
 --
--- "Data.Map.Justified" uses the same rank-2 polymorphism trick used in the 'ST' monad to
+-- "Data.Map.Justified" uses the same rank-2 polymorphism trick used in the @'Control.Monad.ST'@ monad to
 -- ensure that the @ph@ phantom type can not be extracted; in effect, the proof that a key is
 -- present can't leak to contexts where the proof would no longer be valid.
 --
--- == Tutorial
---
--- See "Data.Map.Justified.Tutorial" for usage examples and FAQs.
 
 module Data.Map.Justified (
     -- * Map and Key types
@@ -98,6 +138,7 @@
 
     -- * Evaluation
     , withMap
+    , withSingleton
     , KeyInfo(..)
     , MissingReference
     , withRecMap
@@ -105,14 +146,42 @@
     -- * Gathering evidence
     , member
     , keys
-
+    , lookupLT
+    , lookupLE
+    , lookupGT
+    , lookupGE
+      
     -- * Lookup and update
     , lookup
     , (!)
     , adjust
     , adjustWithKey
     , reinsert
+    -- ** Inserting new keys
+    , inserting
+    , insertingWith
+      
+    -- * Mapping
+    , mapWithKey
+    , traverseWithKey
+    , mapAccum
+    , mapAccumWithKey
+    -- ** Mapping keys
+    , mappingKeys
+    , mappingKnownKeys
+    , mappingKeysWith
+    , mappingKnownKeysWith
+      
+    -- * Unions
+    , unioning
+    , unioningWith
+    , unioningWithKey
 
+    -- * Zipping
+    , zip
+    , zipWith
+    , zipWithKey
+      
     -- * Indexing
     , findIndex
     , elemAt
@@ -122,7 +191,7 @@
 
     ) where
 
-import Prelude hiding (lookup)
+import Prelude hiding (lookup, zip, zipWith)
 import qualified Data.Map as M
 import Data.List (partition)
 import Control.Arrow ((&&&))
@@ -130,23 +199,23 @@
 {--------------------------------------------------------------------
   Map and Key types
 --------------------------------------------------------------------}
--- | A "Data.Map" 'Data.Map.Map' wrapper that allows direct lookup of keys that
+-- | A "Data.Map" @'Data.Map.Map'@ wrapper that allows direct lookup of keys that
 -- are known to exist in the map.
 --
 -- Here, "direct lookup" means that once a key has been proven
 -- to exist in the map, it can be used to extract a value directly
--- from the map, rather than requiring a 'Maybe' layer.
+-- from the map, rather than requiring a @'Maybe'@ layer.
 --
--- 'Map' allows you to shift the burden of proof that a key exists
+-- @'Map'@ allows you to shift the burden of proof that a key exists
 -- in a map from "prove at every lookup" to "prove once per key".
 newtype Map ph k v = Map (M.Map k v) deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
 
--- | A key that knows it can be found in certain 'Map's.
+-- | A key that knows it can be found in certain @'Map'@s.
 -- 
 -- The evidence that the key can be found in a map is carried by
 -- the type system via the phantom type parameter @ph@. Certain
--- operations such as lookup will only type-check if the 'Key'
--- and the 'Map' have the same phantom type parameter.
+-- operations such as lookup will only type-check if the @'Key'@
+-- and the @'Map'@ have the same phantom type parameter.
 newtype Key ph k = Key k deriving (Eq, Ord, Show)
 
 -- | Get a bare key out of a key-plus-evidence by forgetting
@@ -154,7 +223,7 @@
 theKey :: Key ph k -> k
 theKey (Key k) = k
 
--- | Get the underlying "Data.Map" 'Data.Map' out of a 'Map'.
+-- | Get the underlying "Data.Map" @'Data.Map'@ out of a @'Map'@.
 theMap :: Map ph k v -> M.Map k v
 theMap (Map m) = m
 
@@ -178,16 +247,27 @@
 -- >     Just k  -> putStrLn ("Found " ++ show k ++ " with value " ++ lookup k m)
 
 withMap :: M.Map k v -> (forall ph. Map ph k v -> t) -> t
-withMap m f = f (Map m)
+withMap m cont = cont (Map m)
 
+-- | Like @'withMap'@, but begin with a singleton map taking @k@ to @v@.
+--
+-- The continuation is passed a pair consisting of:
+--
+--  1. Evidence that @k@ is in the map, and
+--
+--  2. The singleton map itself, of type @'Map' ph k v@.
+--
+-- > withSingleton 1 'a' (uncurry lookup) == 'a'
+
+withSingleton :: k -> v -> (forall ph. (Key ph k, Map ph k v) -> t) -> t
+withSingleton k v cont = cont (Key k, Map (M.singleton k v))
+
 -- | Information about whether a key is present or missing.
--- See 'Data.Map.Justified.withRecMap' and "Data.Map.Justified.Tutorial"'s
--- 'Data.Map.Justified.Tutorial.example4'.
+-- See @'Data.Map.Justified.withRecMap'@ and "Data.Map.Justified.Tutorial"'s @'Data.Map.Justified.Tutorial.example5'@.
 data KeyInfo = Present | Missing deriving (Show, Eq, Ord)
 
 -- | A description of what key/value-containing-keys pairs failed to be found.
--- See 'Data.Map.Justified.withRecMap' and "Data.Map.Justified.Tutorial"'s
--- 'Data.Map.Justified.Tutorial.example4'.
+-- See @'Data.Map.Justified.withRecMap'@ and "Data.Map.Justified.Tutorial"'s @'Data.Map.Justified.Tutorial.example5'@.
 type MissingReference k f = (k, f (k, KeyInfo))
 
 -- | Evaluate an expression using justified key lookups into the given map,
@@ -208,14 +288,15 @@
 -- >
 -- > memory2 = M.fromList [(1, Cons 2 3), (2, Nil)]
 -- > withRecMap memory2 (const ()) -- Left [(1, Cons (2,Present) (3,Missing))]
-
+--
+-- See @'Data.Map.Justified.Tutorial.example5'@ for more usage examples.
 withRecMap :: (Ord k, Traversable f)
            => M.Map k (f k)
            -> (forall ph. Map ph k (f (Key ph k)) -> t)
            -> Either [MissingReference k f] t
-withRecMap m f =
+withRecMap m cont =
   case bad of
-    [] -> Right $ f (Map $ M.map (fmap Key) $ M.fromList ok)
+    [] -> Right $ cont (Map $ M.map (fmap Key) $ M.fromList ok)
     _  -> Left (map (\(k,v) -> (k, fmap (id &&& locate) v)) bad)
   where
     (ok, bad) = partition (all ((== Present) . locate) . snd) (M.toList m)
@@ -227,9 +308,9 @@
 -- | /O(log n)/. Obtain evidence that the key is a member of the map.
 --
 -- Where "Data.Map" generally requires evidence that a key exists in a map
--- at every use of some functions (e.g. "Data.Map"'s 'Data.Map.lookup'),
--- 'Map' requires the evidence up-front. After it is known that a key can be
--- found, there is no need for 'Maybe' types or run-time errors.
+-- at every use of some functions (e.g. "Data.Map"'s @'Data.Map.lookup'@),
+-- @'Map'@ requires the evidence up-front. After it is known that a key can be
+-- found, there is no need for @'Maybe'@ types or run-time errors.
 --
 -- The @Maybe value@ that has to be checked at every lookup in "Data.Map"
 -- is then shifted to a @Maybe (Key ph k)@ that has to be checked in order
@@ -253,7 +334,7 @@
   Lookup and update
 --------------------------------------------------------------------}
 -- | /O(log n)/. Find the value at a key. Unlike
--- "Data.Map"'s 'Data.Map.!', this function is total and can not fail at runtime.
+-- "Data.Map"'s @'Data.Map.!'@, this function is total and can not fail at runtime.
 (!) :: Ord k => Map ph k v -> Key ph k -> v
 (!) = flip lookup
 
@@ -268,6 +349,40 @@
   Just value -> value
   Nothing    -> error "Data.Map.Justified has been subverted!"
 
+-- | /O(log n)/. Find the largest key smaller than the given one
+-- and return the corresponding (key,value) pair, with evidence for the key.
+--
+-- > withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupLT 3 table == Nothing
+-- > withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupLT 4 table == Just (Key 3, 'a')
+lookupLT :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)
+lookupLT k (Map m) = fmap (\(key, v) -> (Key key, v)) (M.lookupLT k m)
+
+-- | /O(log n)/. Find the smallest key greater than the given one
+-- and return the corresponding (key,value) pair, with evidence for the key.
+--
+-- > withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupGT 4 table == Just (Key 5, 'b')
+-- > withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupGT 5 table == Nothing
+lookupGT :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)
+lookupGT k (Map m) = fmap (\(key, v) -> (Key key, v)) (M.lookupGT k m)
+
+-- | /O(log n)/. Find the largest key smaller than or equal to the given one
+-- and return the corresponding (key,value) pair, with evidence for the key.
+--
+-- > withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupLE 2 table == Nothing
+-- > withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupLE 4 table == Just (Key 3, 'a')
+-- > withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupLE 5 table == Just (Key 5, 'b')
+lookupLE :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)
+lookupLE k (Map m) = fmap (\(key, v) -> (Key key, v)) (M.lookupLE k m)
+
+-- | /O(log n)/. Find the smallest key greater than or equal to the given one
+-- and return the corresponding (key,value) pair, with evidence for the key.
+--
+-- > withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupGE 3 table == Just (Key 3, 'a')
+-- > withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupGE 4 table == Just (Key 5, 'b')
+-- > withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupGE 6 table == Nothing
+lookupGE :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)
+lookupGE k (Map m) = fmap (\(key, v) -> (Key key, v)) (M.lookupGE k m)
+
 -- | Adjust the valid at a key, known to be in the map,
 -- using the given function.
 --
@@ -285,8 +400,9 @@
 -- are the same, keys that were valid for the input map remain
 -- valid for the output map.
 
-adjustWithKey :: Ord k => (k -> v -> v) -> Key ph k -> Map ph k v -> Map ph k v
-adjustWithKey f (Key k) (Map m) = Map (M.adjustWithKey f k m)
+adjustWithKey :: Ord k => (Key ph k -> v -> v) -> Key ph k -> Map ph k v -> Map ph k v
+adjustWithKey f (Key k) (Map m) = Map (M.adjustWithKey f' k m)
+  where f' key = f (Key key)
 
 -- | Replace the value at a key, known to be in the map.
 --
@@ -297,16 +413,250 @@
 reinsert :: Ord k => Key ph k -> v -> Map ph k v -> Map ph k v
 reinsert (Key k) v (Map m) = Map (M.insert k v m)
 
+-- | Insert a value for a key that is /not/ known to be in the map,
+-- evaluating the updated map with the given continuation.
+--
+-- The continuation is given three things:
+--
+--   1. A proof that the inserted key exists in the new map,
+--
+--   2. A function that can be used to convert evidence that a key
+--      exists in the original map, to evidence that the key exists in
+--      the updated map, and
+--
+--   3. The updated @'Data.Map.Justified.Map'@, with a /different phantom type/.
+--
+-- > withMap (M.fromList [(5,'a'), (3,'b')]) (\table -> inserting 5 'x' table $ \(_,_,table') -> theMap table') == M.fromList [(3, 'b'), (5, 'x')]
+-- > withMap (M.fromList [(5,'a'), (3,'b')]) (\table -> inserting 7 'x' table $ \(_,_,table') -> theMap table') == M.fromList [(3, 'b'), (5, 'b'), (7, 'x')]
+--
+-- See @'Data.Map.Justified.Tutorial.example4'@ for more usage examples.
+inserting :: Ord k
+          => k
+          -> v
+          -> Map ph k v
+          -> (forall ph'. (Key ph' k, Key ph k -> Key ph' k, Map ph' k v) -> t)
+          -> t
+inserting k v (Map m) cont = cont (Key k, \(Key key) -> Key key, Map (M.insert k v m))
 
+-- | /O(log n)/. Insert with a function, combining new value and old value.
+-- @'insertingWith' f key value mp cont@
+-- will insert the pair (key, value) into @mp@ if key does
+-- not exist in the map. If the key /does/ exist, the function will
+-- insert the pair @(key, f new_value old_value)@.
+--
+-- The continuation is given three things (as in @'inserting'@):
+--
+--   1. A proof that the inserted key exists in the new map,
+--
+--   2. A function that can be used to convert evidence that a key
+--      exists in the original map, to evidence that the key exists in
+--      the updated map, and
+--
+--   3. The updated @'Data.Map.Justified.Map'@, with a /different phantom type/.
+--
+-- > withMap (M.fromList [(5,"a"), (3,"b")]) (theMap . insertingWith (++) 5) == M.fromList [(3,"b"), (5,"xxxa")]
+-- > withMap (M.fromList [(5,"a"), (3,"b")]) (theMap . insertingWith (++) 7) == M.fromList [(3,"b"), (5,"a"), (7,"xxx")]
+insertingWith :: Ord k
+              => (v -> v -> v)
+              -> k
+              -> v
+              -> Map ph k v
+              -> (forall ph'. (Key ph' k, Key ph k -> Key ph' k, Map ph' k v) -> t)
+              -> t
+insertingWith f k v (Map m) cont = cont (Key k, \(Key key) -> Key key, Map (M.insertWith f k v m))
+                                         
 {--------------------------------------------------------------------
+  Unions
+--------------------------------------------------------------------}
+
+-- | Take the left-biased union of two @'Data.Map.Justified.Map'@s, as in "Data.Map"'s
+-- @'Data.Map.union'@, evaluating the unioned map with the given continuation.
+--
+-- The continuation is given three things:
+--
+--   1. A function that can be used to convert evidence that a key exists in the left
+--      map to evidence that the key exists in the union,
+--
+--   2. A function that can be used to convert evidence that a key exists in the right
+--      map to evidence that the key exists in the union, and
+--
+--   3. The updated @'Data.Map.Justified.Map'@, with a /different phantom type/.
+--
+unioning :: Ord k
+         => Map phL k v
+         -> Map phR k v
+         -> (forall ph'. (Key phL k -> Key ph' k, Key phR k -> Key ph' k, Map ph' k v) -> t)
+         -> t
+unioning (Map mapL) (Map mapR) cont = cont (\(Key key) -> Key key,
+                                            \(Key key) -> Key key,
+                                            Map (M.union mapL mapR))
+
+-- | @'unioningWith' f@ is the same as @'unioning'@, except that @f@ is used to
+-- combine values that correspond to keys found in both maps.
+unioningWith :: Ord k
+             => (v -> v -> v)
+             -> Map phL k v
+             -> Map phR k v
+             -> (forall ph'. (Key phL k -> Key ph' k, Key phR k -> Key ph' k, Map ph' k v) -> t)
+             -> t
+unioningWith f (Map mapL) (Map mapR) cont = cont (\(Key key) -> Key key,
+                                                  \(Key key) -> Key key,
+                                                  Map (M.unionWith f mapL mapR))
+
+-- | @'unioningWithKey' f@ is the same as @'unioningWith' f@, except that @f@ also
+-- has access to the key and evidence that it is present in both maps.
+unioningWithKey :: Ord k
+                => (Key phL k -> Key phR k -> v -> v -> v)
+                -> Map phL k v
+                -> Map phR k v
+                -> (forall ph'. (Key phL k -> Key ph' k, Key phR k -> Key ph' k, Map ph' k v) -> t)
+                -> t
+unioningWithKey f (Map mapL) (Map mapR) cont = cont (\(Key key) -> Key key,
+                                                     \(Key key) -> Key key,
+                                                     Map (M.unionWithKey f' mapL mapR))
+  where f' k = f (Key k) (Key k)
+
+{--------------------------------------------------------------------
+  Mapping and traversing
+--------------------------------------------------------------------}
+
+-- | /O(n)/. Map a function over all keys and values in the map.
+--
+mapWithKey :: (Key ph k -> a -> b)
+           -> Map ph k a
+           -> Map ph k b
+mapWithKey f (Map m) = Map (M.mapWithKey f' m)
+  where f' k = f (Key k)
+
+-- | /O(n)/. As in @'Data.Map.traverse'@: traverse the map, but give the
+-- traversing function access to the key associated with each value.
+traverseWithKey :: Applicative t
+                => (Key ph k -> a -> t b)
+                -> Map ph k a
+                -> t (Map ph k b)
+traverseWithKey f (Map m) = fmap Map (M.traverseWithKey f' m)
+  where f' k = f (Key k)
+        
+-- | /O(n)/. The function @'mapAccum'@ threads an accumulating
+-- argument through the map in ascending order of keys.
+--
+mapAccum :: (a -> b -> (a,c))
+         -> a
+         -> Map ph k b
+         -> (a, Map ph k c)
+mapAccum f a (Map m) = fmap Map (M.mapAccum f a m)
+
+-- | /O(n)/. The function @'mapAccumWithKey'@ threads an accumulating
+-- argument through the map in ascending order of keys.
+--
+mapAccumWithKey :: (a -> Key ph k -> b -> (a,c))
+                -> a
+                -> Map ph k b
+                -> (a, Map ph k c)
+mapAccumWithKey f a (Map m) = fmap Map (M.mapAccumWithKey f' a m)
+  where f' x k = f x (Key k)
+        
+-- | /O(n*log n)/.
+-- @'mappingKeys'@ evaluates a continuation with the map obtained by applying
+-- @f@ to each key of @s@.
+--
+-- The size of the resulting map may be smaller if @f@ maps two or more distinct
+-- keys to the same new key.  In this case the value at the greatest of the
+-- original keys is retained.
+--
+-- The continuation is passed two things:
+--
+--   1. A function that converts evidence that a key belongs to the original map
+--      into evidence that a key belongs to the new map.
+--
+--   2. The new, possibly-smaller map.
+--
+--
+mappingKeys :: Ord k2
+            => (k1 -> k2)
+            -> Map ph k1 v
+            -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t)
+            -> t
+mappingKeys f (Map m) cont = cont (\(Key k) -> Key (f k), Map (M.mapKeys f m))
+
+-- | /O(n*log n)/.
+-- Same as @'mappingKeys'@, but the key-mapping function can make use of
+-- evidence that the input key belongs to the original map.
+--
+mappingKnownKeys :: Ord k2
+            => (Key ph k1 -> k2)
+            -> Map ph k1 v
+            -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t)
+            -> t
+mappingKnownKeys f (Map m) cont = cont (Key . f, Map (M.mapKeys f' m))
+  where f' k = f (Key k)
+        
+-- | /O(n*log n)/.
+-- Same as @'mappingKeys'@, except a function is used to combine values when
+-- two or more keys from the original map correspond to the same key in the
+-- final map.
+mappingKeysWith :: Ord k2
+                => (v -> v -> v)
+                -> (k1 -> k2)
+                -> Map ph k1 v
+                -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t)
+                -> t
+mappingKeysWith op f (Map m) cont = cont (\(Key k) -> Key (f k), Map (M.mapKeysWith op f m))
+
+-- | /O(n*log n)/.
+-- Same as @'mappingKnownKeys'@, except a function is used to combine values when
+-- two or more keys from the original map correspond to the same key in the
+-- final map.
+mappingKnownKeysWith :: Ord k2
+                => (v -> v -> v)
+                -> (Key ph k1 -> k2)
+                -> Map ph k1 v
+                -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t)
+                -> t
+mappingKnownKeysWith op f (Map m) cont = cont (Key . f, Map (M.mapKeysWith op f' m))
+  where f' k = f (Key k)
+        
+{--------------------------------------------------------------------
+  Zipping
+--------------------------------------------------------------------}
+
+-- | Zip the values in two maps together. The phantom type @ph@ ensures
+-- that the two maps have the same set of keys, so no elements are left out.
+--
+zip :: Ord k
+    => Map ph k a
+    -> Map ph k b
+    -> Map ph k (a,b)
+zip = zipWith (,)
+
+-- | Combine the values in two maps together. The phantom type @ph@ ensures
+-- that the two maps have the same set of keys, so no elements are left out.
+zipWith :: Ord k
+        => (a -> b -> c)
+        -> Map ph k a
+        -> Map ph k b
+        -> Map ph k c
+zipWith f m1 m2 = mapWithKey (\k x -> f x (m2 ! k)) m1
+
+-- | Combine the values in two maps together, using the key and values.
+-- The phantom type @ph@ ensures that the two maps have the same set of
+-- keys.
+zipWithKey :: Ord k
+           => (Key ph k -> a -> b -> c)
+           -> Map ph k a
+           -> Map ph k b
+           -> Map ph k c
+zipWithKey f m1 m2 = mapWithKey (\k x -> f k x (m2 ! k)) m1
+        
+{--------------------------------------------------------------------
   Indexing
 --------------------------------------------------------------------}
 -- | /O(log n)/. Return the /index/ of a key, which is its zero-based index in
 -- the sequence sorted by keys. The index is a number from /0/ up to, but not
--- including, the 'size' of the map. The index also carries a proof that it is
+-- including, the size of the map. The index also carries a proof that it is
 -- valid for the map.
 --
--- Unlike "Data.Map"'s 'Data.Map.findIndex', this function can not fail at runtime.
+-- Unlike "Data.Map"'s @'Data.Map.findIndex'@, this function can not fail at runtime.
 
 findIndex :: Ord k => Key ph k -> Map ph k a -> Key ph Int
 findIndex (Key k) (Map m) = Key (M.findIndex k m)
@@ -314,7 +664,7 @@
 -- | /O(log n)/. Retrieve an element by its /index/, i.e. by its zero-based
 -- index in the sequence sorted by keys.
 --
--- Unlike "Data.Map"'s 'Data.Map.elemAt', this function can not fail at runtime.
+-- Unlike "Data.Map"'s @'Data.Map.elemAt'@, this function can not fail at runtime.
 
 elemAt :: Key ph Int -> Map ph k v -> (Key ph k, v)
 elemAt (Key n) (Map m) = let (k,v) = M.elemAt n m in (Key k, v)
diff --git a/src/Data/Map/Justified/Tutorial.hs b/src/Data/Map/Justified/Tutorial.hs
--- a/src/Data/Map/Justified/Tutorial.hs
+++ b/src/Data/Map/Justified/Tutorial.hs
@@ -44,26 +44,26 @@
 test_table :: M.Map Int String
 test_table = M.fromList [ (1, "hello"), (2, "world") ]
 
--- | This example shows how the 'Data.Map.Justified.member'
+-- | This example shows how the @'Data.Map.Justified.member'@
 -- function can be used to obtain a key whose type has been
 -- augmented by a proof that the key is present in maps of a
 -- certain type.
 --
--- Where "Data.Map" may use a 'Maybe' type to ensure that
+-- Where "Data.Map" may use a @'Maybe'@ type to ensure that
 -- the user handles missing keys when performing a lookup,
--- here we use the 'Maybe' type to either tell the user
--- that a key is missing (by returning 'Nothing'), or
+-- here we use the @'Maybe'@ type to either tell the user
+-- that a key is missing (by returning @'Nothing'@), or
 -- actually give back evidence of the key's presence
 -- (by returning @Just known_key@)
 --
--- The 'Data.Map.Justified.withMap' function is used to
--- plumb a "Data.Map" 'Data.Map.Map' into a function that
--- expects a "Data.Map.Justified" 'Data.Map.Justified.Map'.
+-- The @'Data.Map.Justified.withMap'@ function is used to
+-- plumb a "Data.Map" @'Data.Map.Map'@ into a function that
+-- expects a "Data.Map.Justified" @'Data.Map.Justified.Map'@.
 -- In the code below, you can think of @table@ as @test_table@,
 -- enhanced with the ability to use verified keys.
 --
 -- You can get from @table@ back to @test_table@ using the
--- function 'Data.Map.Justified.theMap'.
+-- function @'Data.Map.Justified.theMap'@.
 --
 -- @
 --  example1 = withMap test_table $ \\table -> do
@@ -104,10 +104,10 @@
 -- "Data.Map.Justified" has several functions that are similar
 -- to ones found in "Data.Map" that operate over verified keys.
 -- In this example, notice that we can extract values directly
--- from the map using 'Data.Map.Justified.lookup'; since we already
+-- from the map using @'Data.Map.Justified.lookup'@; since we already
 -- proved that the key is present when we obtained a @Key ph k@
--- value, 'Data.Map.Justified.lookup' does not need to return a
--- 'Maybe' value.
+-- value, @'Data.Map.Justified.lookup'@ does not need to return a
+-- @'Maybe'@ value.
 --
 -- @
 --  example2 = withMap test_table $ \\table -> do
@@ -204,6 +204,47 @@
 
   return ()
 
+-- | What if your set of keys can change over time?
+--
+-- If you were to insert a new key into a map, evidence that a key
+-- exists is in the old map is no longer equivalent to evidence that
+-- a key exists in the new map.
+--
+-- On the other hand, we know that if some @key@ exists in the old map,
+-- then @key@ must still exist in the new map. So there should be a
+-- way of "upgrading" evidence from the old map to the new. Furthermore,
+-- we know that the key we just added must be in the new map.
+--
+-- The @'Data.Map.Justified.inserting'@ function inserts a value into a map
+-- and feeds the new map into a continuation, along with the "upgrade" and
+-- "new key" data.
+--
+-- @
+--  example4 = withMap test_table $ \table -> do
+--    inserting 3 "NEW" table $ \(newKey, upgrade, table') -> do
+--      forM_ (keys table) $ \key -> do
+--        putStrLn (show key ++ " maps to " ++ table  ! key ++ " in the old table.")
+--        putStrLn (show key ++ " maps to " ++ table' ! (upgrade key) ++ " in the new table.")
+--      putStrLn ("Also, the new table maps " ++ show newKey ++ " to " ++ table' ! newKey)
+-- @
+-- Output:
+--
+-- @
+--  Key 1 maps to hello in the old table.
+--  Key 1 maps to hello in the new table.
+--  Key 2 maps to world in the old table.
+--  Key 2 maps to world in the new table.
+--  Also, the new table maps Key 3 to NEW
+-- @
+
+example4 :: IO ()
+example4 = withMap test_table $ \table -> do
+  inserting 3 "NEW" table $ \(newKey, upgrade, table') -> do
+    forM_ (keys table) $ \key -> do
+      putStrLn (show key ++ " maps to " ++ table  ! key ++ " in the old table.")
+      putStrLn (show key ++ " maps to " ++ table' ! (upgrade key) ++ " in the new table.")
+    putStrLn ("Also, the new table maps " ++ show newKey ++ " to " ++ table' ! newKey)
+    
 -- | The next example uses a directed graph, defined by this adjacency list.
 --
 -- @
@@ -233,16 +274,16 @@
 --                                   |
 --   (each neighbor should carry a proof that they are also in the map)
 -- @
--- You can do this via 'Data.Map.Justified.withRecMap', which converts each
--- key reference of type @k@ in your map to a verified key of type @Key ph k@.
+-- You can do this via @'Data.Map.Justified.withRecMap'@, which converts each
+-- key reference of type @k@ in your map to a verified key of type @'Key' ph k@.
 --
--- But what if a referenced key really is missing from the map? 'Data.Map.Justified.withRecMap'
--- returns an 'Either' value to represent failure; if a key is missing, then the
--- result will be a value of the form @Left problem@, where @problem@ is an explanation
+-- But what if a referenced key really is missing from the map? @'Data.Map.Justified.withRecMap'@
+-- returns an @'Either'@ value to represent failure; if a key is missing, then the
+-- result will be a value of the form @'Left' problems@, where @problems@ is an explanation
 -- of where the missing keys are.
 --
 -- @
---  example4 = do
+--  example5 = do
 --     -- Print out the nodes in a graph 
 --     putStrLn ("Finding nodes in the directed graph " ++ show adjacencies)
 --     trial adjacencies
@@ -271,8 +312,8 @@
 --    The following edges are missing targets:
 --      4 -> 6
 -- @
-example4 :: IO ()
-example4 = do
+example5 :: IO ()
+example5 = do
    -- Print out the nodes in a graph 
    putStrLn ("Finding nodes in the directed graph " ++ show adjacencies)
    trial adjacencies