diff --git a/refined-containers.cabal b/refined-containers.cabal
--- a/refined-containers.cabal
+++ b/refined-containers.cabal
@@ -23,10 +23,11 @@
 license-file: LICENSE
 author: mniip@typeable.io
 maintainer: mniip@typeable.io
-version: 0.1.0.2
+version: 0.1.1.0
 build-type: Simple
 
 tested-with:
+    , GHC == 9.12.1
     , GHC == 9.10.1
     , GHC == 9.8.2
     , GHC == 9.6.6
@@ -42,7 +43,7 @@
 
 library
     build-depends:
-        , base >= 4.12 && < 4.21
+        , base >= 4.12 && < 4.22
         , adjunctions >= 4.4 && < 4.5
         , constraints >= 0.11 && < 0.15
         , containers >= 0.5.7 && < 0.8
diff --git a/src/Data/HashMap/Common/Refined.hs b/src/Data/HashMap/Common/Refined.hs
--- a/src/Data/HashMap/Common/Refined.hs
+++ b/src/Data/HashMap/Common/Refined.hs
@@ -4,6 +4,7 @@
 
 import           Control.Monad.Reader
 import           Control.DeepSeq
+import           Data.Bifoldable
 import           Data.Coerce
 import           Data.Constraint (Dict(..))
 import           Data.Container.Refined.Hashable
@@ -11,6 +12,7 @@
 import           Data.Container.Refined.Unsafe
 import           Data.Distributive
 import           Data.Foldable.WithIndex
+import           Data.Functor.Classes
 import           Data.Functor.Rep
 import           Data.Functor.WithIndex
 import qualified Data.Hashable as Hashable
@@ -22,6 +24,7 @@
 import           Data.Traversable.WithIndex
 import           Data.Type.Coercion
 import           Data.Type.Equality ((:~:)(..))
+import           Prelude hiding (zipWith)
 import           Refined
 import           Refined.Unsafe
 import           Unsafe.Coerce
@@ -44,7 +47,10 @@
 -- always derive @'KnownHashSet' s k@ by pattern matching on the 'Dict' returned
 -- by 'keysSet'.
 newtype HashMap s k a = HashMap (HashMap.HashMap k a)
-  deriving newtype (Eq, Ord, Show, Functor, Foldable, Hashable.Hashable, NFData)
+  deriving newtype
+    ( Eq, Eq1, Eq2, Ord, Ord1, Ord2, Show, Show1, Show2
+    , Functor, Foldable, Bifoldable, Hashable.Hashable, NFData
+    )
   deriving stock (Traversable)
 type role HashMap nominal nominal representational
 
@@ -90,7 +96,7 @@
 --
 -- @
 -- 'withHashMap' ('fromHashMap' ...
---   $ \(m :: 'HashMap' s k a) -> doSomethingWith \@s
+--   $ \\(m :: 'HashMap' s k a) -> doSomethingWith \@s
 -- @
 withHashMap
   :: forall k a r. SomeHashMap k a -> (forall s. HashMap s k a -> r) -> r
@@ -100,6 +106,26 @@
 fromHashMap :: forall k a. HashMap.HashMap k a -> SomeHashMap k a
 fromHashMap m = SomeHashMap (HashMap m)
 
+-- | Given a set of keys @s@ known ahead of time, verify whether a regular
+-- 'Data.HashMap.Lazy.HashMap' has exactly that set of keys.
+verifyHashMap
+  :: forall s k a. (Hashable k, KnownHashSet s k)
+  => HashMap.HashMap k a -> Maybe (HashMap s k a)
+verifyHashMap m
+#if MIN_VERSION_unordered_containers(0, 2, 12)
+  | HashMap.isSubmapOfBy (\_ _ -> True) m (HashSet.toMap keys)
+  , HashMap.isSubmapOfBy (\_ _ -> True) (HashSet.toMap keys) m
+#else
+  | All True <- flip HashMap.foldMapWithKey m \k _
+    -> All $ k `HashSet.member` keys
+  , All True <- flip foldMap keys \k
+    -> All $ k `HashMap.member` m
+#endif
+  = Just (HashMap m)
+  | otherwise = Nothing
+  where
+    keys = reflect $ Proxy @s
+
 -- | An existential wrapper for a 'HashMap' with an as-yet-unknown set of keys,
 -- together with a proof of some fact @p@ about the set. Pattern matching on it
 -- gives you a way to refer to the set (the parameter @s@). Functions that
@@ -214,12 +240,26 @@
 
 -- | Given two maps proven to have the same keys, for each key apply the
 -- function to the associated values, to obtain a new map with the same keys.
-zipWithKey
+zipWith
   :: forall s k a b c. Hashable k
-  => (Key s k -> a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c
-zipWithKey f (HashMap m1) (HashMap m2) = HashMap
-  $ HashMap.intersectionWithKey (f . unsafeKey) m1 m2
+  => (a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c
+zipWith f (HashMap m1) (HashMap m2) = HashMap $ HashMap.intersectionWith f m1 m2
 
+-- | Return the union of two maps. For keys that exist in both maps, the value
+-- is taken from the first map.
+--
+-- @
+-- 'union' = unionWith 'const'
+-- @
+union
+  :: forall s t k a. Hashable k
+  => HashMap s k a
+  -> HashMap t k a
+  -> SomeHashMapWith (UnionProof 'Hashed s t) k a
+union (HashMap m1) (HashMap m2) = SomeHashMapWith
+  (HashMap $ HashMap.union m1 m2)
+  $ UnionProof unsafeSubset unsafeSubsetWith2
+
 -- | Remove the keys that appear in the second map from the first map.
 difference
   :: forall s t k a b. Hashable k
@@ -230,6 +270,20 @@
   = SomeHashMapWith (HashMap $ HashMap.difference m1 m2)
     $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset
 
+-- | Return the intersection of two maps, taking values from the first map.
+--
+-- @
+-- 'intersection' = intersectionWith 'const'
+-- @
+intersection
+  :: forall s t k a b. Hashable k
+  => HashMap s k a
+  -> HashMap t k b
+  -> SomeHashMapWith (IntersectionProof 'Hashed s t) k a
+intersection (HashMap m1) (HashMap m2) = SomeHashMapWith
+  (HashMap $ HashMap.intersection m1 m2)
+  $ IntersectionProof unsafeSubset unsafeSubsetWith2
+
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, that are proven to be in the map. The set of keys remains the same.
 mapWithKey
@@ -288,6 +342,25 @@
 toList :: forall s k a. HashMap s k a -> [(Key s k, a)]
 toList = gcoerceWith (unsafeCastKey @s @k) $ coerce $ HashMap.toList @k @a
 
+-- | Retain only the values that satisfy the predicate, returning a potentially
+-- smaller map.
+filter
+  :: forall s k a. (a -> Bool)
+  -> HashMap s k a
+  -> SomeHashMapWith (SupersetProof 'Hashed s) k a
+filter p (HashMap m) = SomeHashMapWith (HashMap $ HashMap.filter p m)
+  $ SupersetProof unsafeSubset
+
+-- | Retain only the keys that satisfy the predicate, returning a potentially
+-- smaller map.
+filterKeys
+  :: forall s k a. (Key s k -> Bool)
+  -> HashMap s k a
+  -> SomeHashMapWith (SupersetProof 'Hashed s) k a
+filterKeys p (HashMap m) = SomeHashMapWith
+  (HashMap $ HashMap.filterWithKey (\k _ -> p (unsafeKey k)) m)
+  $ SupersetProof unsafeSubset
+
 -- | Retain only the key-value pairs that satisfy the predicate, returning a
 -- potentially smaller map.
 filterWithKey
@@ -317,6 +390,25 @@
 
 -- | Partition a map into two disjoint submaps: those whose key-value pairs
 -- satisfy the predicate, and those whose don't.
+partition
+  :: forall s k a. Hashable k -- TODO: this is only used in the proof
+  => (a -> Bool)
+  -> HashMap s k a
+  -> Some2HashMapWith (PartitionProof 'Hashed s k) k a a
+partition p (HashMap m) = Some2HashMapWith
+  (HashMap $ HashMap.filter p m)
+  (HashMap $ HashMap.filter (not . p) m)
+  $ PartitionProof
+    do \k -> case HashMap.lookup (unrefine k) m of
+        Nothing -> error
+          "partition: bug: Data.HashMap.Refined has been subverted"
+        Just x -> if p x
+          then Left $ unsafeKey $ unrefine k
+          else Right $ unsafeKey $ unrefine k
+    unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g
+
+-- | Partition a map into two disjoint submaps: those whose key-value pairs
+-- satisfy the predicate, and those whose don't.
 partitionWithKey
   :: forall s k a. Hashable k -- TODO: this is only used in the proof
   => (Key s k -> a -> Bool)
@@ -349,15 +441,15 @@
 castKey = castRefined
 
 -- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps
--- can be interconverted too. For example, 'zipWithKey' can be implemented via
--- 'Data.HashMap.Refined.intersectionWithKey' by proving that the set of keys
--- remains unchanged:
+-- can be interconverted too. For example, 'Data.HashMap.Refined.zipWithKey' can
+-- be implemented via 'Data.HashMap.Refined.intersectionWithKey' by proving that
+-- the set of keys remains unchanged:
 --
 -- @
--- 'zipWithKey'
+-- 'Data.HashMap.Refined.zipWithKey'
 --   :: forall s k a b c. 'Hashable' k
 --   => ('Key' s k -> a -> b -> c) -> 'HashMap' s k a -> 'HashMap' s k b -> 'HashMap' s k c
--- 'zipWithKey' f m1 m2
+-- 'Data.HashMap.Refined.zipWithKey' f m1 m2
 --   | v'SomeHashMapWith' @r m proof <- 'Data.HashMap.Refined.intersectionWithKey' (f . 'andLeft') m1 m2
 --   , v'IntersectionProof' p1 p2 <- proof
 --   , ( v'Coercion' :: t'Coercion' ('HashMap' r k c) ('HashMap' s k c))
@@ -382,10 +474,10 @@
   itraverse = traverseWithKey
 
 -- | Similar to the instance for functions -- zip corresponding keys. To use
--- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWithKey'.
+-- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWith'.
 instance (Hashable k, KnownHashSet s k) => Applicative (HashMap s k) where
   pure x = fromSet \_ -> x
-  (<*>) = zipWithKey (const id)
+  (<*>) = zipWith id
 
 -- | @'bind' m f@ is a map that for each key @k :: 'Key' s k@, contains the
 -- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.
@@ -408,7 +500,7 @@
 
 -- | Append the values at the corresponding keys
 instance (Hashable k, Semigroup a) => Semigroup (HashMap s k a) where
-  (<>) = zipWithKey (const (<>))
+  (<>) = zipWith (<>)
 
 instance (Hashable k, KnownHashSet s k, Monoid a)
   => Monoid (HashMap s k a) where
diff --git a/src/Data/HashMap/Refined.hs b/src/Data/HashMap/Refined.hs
--- a/src/Data/HashMap/Refined.hs
+++ b/src/Data/HashMap/Refined.hs
@@ -43,18 +43,26 @@
   , SingletonProof(..)
   , fromSet
   , Common.fromHashMap
+  , Common.verifyHashMap
+  , fromTraversable
+  , fromTraversableWith
   , fromTraversableWithKey
   , FromTraversableProof(..)
   -- * Insertion
   , insert
+  , insertWith
+  , insertWithKey
   , InsertProof(..)
   , reinsert
   , insertLookupWithKey
   -- * Deletion/Update
   , Common.delete
+  , adjust'
   , adjust
   , adjustWithKey
+  , update'
   , update
+  , updateWithKey
   , updateLookupWithKey
   -- * Query
   , Common.lookup
@@ -66,21 +74,29 @@
   , Common.disjoint
   , DisjointProof(..)
   -- * Combine
+  , zipWith
   , zipWithKey
   , bind
+  , Common.union
+  , unionWith
   , unionWithKey
   , UnionProof(..)
   , Common.difference
   , DifferenceProof(..)
+  , differenceWith
   , differenceWithKey
   , PartialDifferenceProof(..)
+  , Common.intersection
+  , intersectionWith
   , intersectionWithKey
   , IntersectionProof(..)
   -- * Traversal
+  , map
   , mapWithKey
   , traverseWithKey
   , mapAccumLWithKey
   , mapAccumRWithKey
+  , mapKeys
   , mapKeysWith
   , MapProof(..)
   , backpermuteKeys
@@ -97,10 +113,15 @@
   -- * Filter
   , Common.restrictKeys
   , Common.withoutKeys
+  , Common.filter
+  , Common.filterKeys
   , Common.filterWithKey
+  , Common.partition
   , Common.partitionWithKey
   , PartitionProof(..)
+  , mapMaybe
   , mapMaybeWithKey
+  , mapEither
   , mapEitherWithKey
   -- * Casts
   , Common.castKey
@@ -115,7 +136,7 @@
 import           Data.Functor
 import           Data.HashMap.Common.Refined
   ( HashMap(..), Key, unsafeCastKey, unsafeKey, SomeHashMapWith(..)
-  , Some2HashMapWith(..), fromSet, (!), zipWithKey, mapWithKey, traverseWithKey
+  , Some2HashMapWith(..), fromSet, (!), zipWith, mapWithKey, traverseWithKey
   , bind
   )
 import qualified Data.HashMap.Common.Refined as Common
@@ -123,7 +144,7 @@
 import           Data.Traversable
 import           Data.Traversable.WithIndex
 import           Data.Type.Coercion
-import           Prelude hiding (lookup, null)
+import           Prelude hiding (lookup, map, null, zipWith)
 import           Refined
 import           Refined.Unsafe
 
@@ -136,7 +157,42 @@
 singleton k v = SomeHashMapWith (HashMap $ HashMap.singleton k v)
   $ SingletonProof (unsafeKey k)
 
--- | Create a map from an arbitrary traversable of key-value pairs.
+-- | Create a map from an arbitrary traversable of key-value pairs. If a key is
+-- repeated, the retained value is the last one in traversal order. If you're
+-- looking for @fromList@, this is the function you want.
+fromTraversable
+  :: forall t k a. (Traversable t, Hashable k)
+  => t (k, a) -> SomeHashMapWith (FromTraversableProof 'Hashed t k) k a
+fromTraversable xs = SomeHashMapWith (HashMap m) $ FromTraversableProof proof
+  where
+    (m, proof) = mapAccumL
+      (\s (k, v) -> let !s' = HashMap.insert k v s in (s', unsafeKey k))
+      HashMap.empty
+      xs
+
+-- | Create a map from an arbitrary traversable of key-value pairs, with a
+-- function for combining values for repeated keys. The function is called as if
+-- by 'foldl1', but flipped:
+--
+-- @
+-- 'fromTraversableWith' f [(k, x1), (k, x2), (k, x3)]
+--   = 'singleton' k (f x3 (f x2 x1))
+-- @
+fromTraversableWith
+  :: forall t k a. (Traversable t, Hashable k)
+  => (a -> a -> a)
+  -> t (k, a)
+  -> SomeHashMapWith (FromTraversableProof 'Hashed t k) k a
+fromTraversableWith f xs
+  = SomeHashMapWith (HashMap m) $ FromTraversableProof proof
+  where
+    (m, proof) = mapAccumL
+      (\s (k, v) -> let !s' = HashMap.insertWith f k v s in (s', unsafeKey k))
+      HashMap.empty
+      xs
+
+-- | Create a map from an arbitrary traversable of key-value pairs. Like
+-- 'fromTraversableWith', but the combining function has access to the key.
 fromTraversableWithKey
   :: forall t k a. (Traversable t, Hashable k)
   => (k -> a -> a -> a)
@@ -160,6 +216,35 @@
 insert k v (HashMap m) = SomeHashMapWith (HashMap $ HashMap.insert k v m)
   $ InsertProof (unsafeKey k) unsafeSubset
 
+-- | Insert a key-value pair into the map to obtain a potentially larger map,
+-- guaranteed to contain the given key. If the key was already present, the
+-- supplied function is used to combine the new value with the old (in that
+-- order).
+insertWith
+  :: forall s k a. Hashable k
+  => (a -> a -> a)
+  -> k
+  -> a
+  -> HashMap s k a
+  -> SomeHashMapWith (InsertProof 'Hashed k s) k a
+insertWith f k v (HashMap m) = SomeHashMapWith
+  (HashMap $ HashMap.insertWith f k v m)
+  $ InsertProof (unsafeKey k) unsafeSubset
+
+-- | Insert a key-value pair into the map to obtain a potentially larger map,
+-- guaranteed to contain the given key. Like 'insertWith', but the combining
+-- function has access to the key, which is guaranteed to be in the old map.
+insertWithKey
+  :: forall s k a. Hashable k
+  => (Key s k -> a -> a -> a)
+  -> k
+  -> a
+  -> HashMap s k a
+  -> SomeHashMapWith (InsertProof 'Hashed k s) k a
+insertWithKey f k v (HashMap m) = SomeHashMapWith
+  (HashMap $ HashMap.insertWith (f $ unsafeKey k) k v m)
+  $ InsertProof (unsafeKey k) unsafeSubset
+
 -- | Overwrite a key-value pair that is known to already be in the map. The set
 -- of keys remains the same.
 reinsert
@@ -183,12 +268,22 @@
     $ InsertProof (unsafeKey k) unsafeSubset
   )
 
+-- | If the given key is in the map, update the value at that key using the
+-- given function. In any case, the set of keys remains the same.
+adjust'
+  :: forall s k a. Hashable k => (a -> a) -> k -> HashMap s k a -> HashMap s k a
+adjust' = coerce $ HashMap.adjust @k @a
+
 -- | Update the value at a specific key known the be in the map using the given
 -- function. The set of keys remains the same.
+--
+-- @
+-- 'reinsert' k v = 'adjust (const v) k'
+-- @
 adjust
   :: forall s k a. Hashable k
   => (a -> a) -> Key s k -> HashMap s k a -> HashMap s k a
-adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ HashMap.adjust @k @a
+adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ adjust' @s @k @a
 
 -- | If the given key is in the map, update the associated value using the given
 -- function with a proof that the key was in the map; otherwise return the map
@@ -198,6 +293,17 @@
   => (Key s k -> a -> a) -> k -> HashMap s k a -> HashMap s k a
 adjustWithKey f k (HashMap m) = HashMap $ HashMap.adjust (f $ unsafeKey k) k m
 
+-- | If a key is present in the map, update its value or delete it using the
+-- given function, returning a potentially smaller map.
+update'
+  :: forall s k a. Hashable k
+  => (a -> Maybe a)
+  -> k
+  -> HashMap s k a
+  -> SomeHashMapWith (SupersetProof 'Hashed s) k a
+update' f k (HashMap m) = SomeHashMapWith (HashMap $ HashMap.update f k m)
+  $ SupersetProof unsafeSubset
+
 -- | Update or delete a key known to be in the map using the given function,
 -- returning a potentially smaller map.
 update
@@ -206,10 +312,21 @@
   -> Key s k
   -> HashMap s k a
   -> SomeHashMapWith (SupersetProof 'Hashed s) k a
-update f k (HashMap m)
-  = SomeHashMapWith (HashMap $ HashMap.update f (unrefine k) m)
-    $ SupersetProof unsafeSubset
+update = gcoerceWith (unsafeCastKey @s @k) $ coerce $ update' @s @k @a
 
+-- | If a key is present in the map, update its value or delete it using the
+-- given function with a proof that the key was in the map, returning a
+-- potentially smaller map.
+updateWithKey
+  :: forall s k a. Hashable k
+  => (Key s k -> a -> Maybe a)
+  -> k
+  -> HashMap s k a
+  -> SomeHashMapWith (SupersetProof 'Hashed s) k a
+updateWithKey f k (HashMap m) = SomeHashMapWith
+  (HashMap $ HashMap.update (f $ unsafeKey k) k m)
+  $ SupersetProof unsafeSubset
+
 -- | If the given key is in the map, update or delete it using the given
 -- function with a proof that the key was in the map; otherwise the map is
 -- unchanged. Alongside return the new value if it was updated, or the old value
@@ -226,8 +343,28 @@
     $ SupersetProof unsafeSubset
   )
 
+-- | Given two maps proven to have the same keys, for each key apply the
+-- function to the associated values, to obtain a new map with the same keys.
+zipWithKey
+  :: forall s k a b c. Hashable k
+  => (Key s k -> a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c
+zipWithKey f (HashMap m1) (HashMap m2) = HashMap
+  $ HashMap.intersectionWithKey (f . unsafeKey) m1 m2
+
 -- | Return the union of two maps, with a given combining function for keys that
 -- exist in both maps simultaneously.
+unionWith
+  :: forall s t k a. Hashable k
+  => (a -> a -> a)
+  -> HashMap s k a
+  -> HashMap t k a
+  -> SomeHashMapWith (UnionProof 'Hashed s t) k a
+unionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith
+  (HashMap $ HashMap.unionWith f m1 m2)
+  $ UnionProof unsafeSubset unsafeSubsetWith2
+
+-- | Return the union of two maps, with a given combining function for keys that
+-- exist in both maps simultaneously.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@
 -- respectively.
@@ -241,8 +378,20 @@
   (HashMap $ HashMap.unionWithKey (f . reallyUnsafeRefine) m1 m2)
   $ UnionProof unsafeSubset unsafeSubsetWith2
 
--- | For keys that appear in both maps, the given function decides whether the
--- key is removed from the first map.
+-- | Return the first map, but for keys that appear in both maps, the given
+-- function decides whether the key is removed.
+differenceWith
+  :: forall s t k a b. Hashable k
+  => (a -> b -> Maybe a)
+  -> HashMap s k a
+  -> HashMap t k b
+  -> SomeHashMapWith (PartialDifferenceProof 'Hashed s t) k a
+differenceWith f (HashMap m1) (HashMap m2) = SomeHashMapWith
+  (HashMap $ HashMap.differenceWith f m1 m2)
+  $ PartialDifferenceProof unsafeSubset unsafeSubset
+
+-- | Return the first map, but for keys that appear in both maps, the given
+-- function decides whether the key is removed.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@
 -- respectively.
@@ -260,6 +409,17 @@
   $ PartialDifferenceProof unsafeSubset unsafeSubset
 
 -- | Return the intersection of two maps with the given combining function.
+intersectionWith
+  :: forall s t k a b c. Hashable k
+  => (a -> b -> c)
+  -> HashMap s k a
+  -> HashMap t k b
+  -> SomeHashMapWith (IntersectionProof 'Hashed s t) k c
+intersectionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith
+  (HashMap $ HashMap.intersectionWith f m1 m2)
+  $ IntersectionProof unsafeSubset unsafeSubsetWith2
+
+-- | Return the intersection of two maps with the given combining function.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@
 -- respectively.
@@ -273,6 +433,10 @@
   (HashMap $ HashMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)
   $ IntersectionProof unsafeSubset unsafeSubsetWith2
 
+-- | Apply a function to all values in a map. The set of keys remains the same.
+map :: forall s k a b. (a -> b) -> HashMap s k a -> HashMap s k b
+map = coerce $ HashMap.map @a @b @k
+
 -- | Thread an accumularing argument through the map in ascending order of
 -- hashes.
 mapAccumLWithKey
@@ -291,6 +455,28 @@
   -> (a, HashMap s k c)
 mapAccumRWithKey f = imapAccumR (flip f)
 
+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results
+-- into a new map. For keys that were mapped to the same new key, the value is
+-- picked in an unspecified way.
+mapKeys
+  :: forall s k1 k2 a. Hashable k2
+  => (Key s k1 -> k2)
+  -> HashMap s k1 a
+  -> SomeHashMapWith (MapProof 'Hashed s k1 k2) k2 a
+mapKeys g (HashMap m) = SomeHashMapWith
+  (HashMap $ HashMap.fromList
+    $ HashMap.foldrWithKey (\k x xs -> (g $ unsafeKey k, x) : xs) [] m)
+  $ MapProof (unsafeKey . g) \k2 ->
+    case HashMap.lookup (unrefine k2) backMap of
+      Nothing -> error "mapKeys: bug: Data.HashMap.Refined has been subverted"
+      Just k1 -> k1
+  where
+    ~backMap = HashMap.fromList
+      [ (k2, unsafeKey k1)
+      | k1 <- HashMap.keys m
+      , let !k2 = g $ unsafeKey k1
+      ]
+
 -- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the
 -- results into a new map. For keys that were mapped to the same new key, @c@
 -- acts as the combining function for corresponding values.
@@ -315,6 +501,15 @@
       , let !k2 = g $ unsafeKey k1
       ]
 
+-- | Apply a function to all values in a map and collect only the 'Just'
+-- results, returning a potentially smaller map.
+mapMaybe
+  :: forall s k a b. (a -> Maybe b)
+  -> HashMap s k a
+  -> SomeHashMapWith (SupersetProof 'Hashed s) k b
+mapMaybe f (HashMap m) = SomeHashMapWith (HashMap $ HashMap.mapMaybe f m)
+  $ SupersetProof unsafeSubset
+
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, and collect only the 'Just' results, returning a potentially smaller
 -- map.
@@ -325,6 +520,27 @@
 mapMaybeWithKey f (HashMap m)
   = SomeHashMapWith (HashMap $ HashMap.mapMaybeWithKey (f . unsafeKey) m)
     $ SupersetProof unsafeSubset
+
+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'
+-- results into separate (disjoint) maps.
+mapEither
+  :: forall s k a b c. Hashable k -- TODO: this is only used in the proof
+  => (a -> Either b c)
+  -> HashMap s k a
+  -> Some2HashMapWith (PartitionProof 'Hashed s k) k b c
+mapEither p (HashMap m)
+  | m' <- HashMap.map p m
+  = Some2HashMapWith
+    (HashMap $ HashMap.mapMaybe (either Just (const Nothing)) m')
+    (HashMap $ HashMap.mapMaybe (either (const Nothing) Just) m')
+    $ PartitionProof
+      do \k -> case HashMap.lookup (unrefine k) m of
+          Nothing -> error
+            "mapEither: bug: Data.HashMap.Refined has been subverted"
+          Just x -> case p x of
+            Left _ -> Left $ unsafeKey $ unrefine k
+            Right _ -> Right $ unsafeKey $ unrefine k
+      unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g
 
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, and collect the 'Left' and 'Right' results into separate (disjoint)
diff --git a/src/Data/HashMap/Strict/Refined.hs b/src/Data/HashMap/Strict/Refined.hs
--- a/src/Data/HashMap/Strict/Refined.hs
+++ b/src/Data/HashMap/Strict/Refined.hs
@@ -43,18 +43,26 @@
   , SingletonProof(..)
   , fromSet
   , Common.fromHashMap
+  , Common.verifyHashMap
+  , fromTraversable
+  , fromTraversableWith
   , fromTraversableWithKey
   , FromTraversableProof(..)
   -- * Insertion
   , insert
+  , insertWith
+  , insertWithKey
   , InsertProof(..)
   , reinsert
   , insertLookupWithKey
   -- * Deletion/Update
   , Common.delete
+  , adjust'
   , adjust
   , adjustWithKey
+  , update'
   , update
+  , updateWithKey
   , updateLookupWithKey
   -- * Query
   , Common.lookup
@@ -66,21 +74,29 @@
   , Common.disjoint
   , DisjointProof(..)
   -- * Combine
+  , zipWith
   , zipWithKey
   , bind
+  , Common.union
+  , unionWith
   , unionWithKey
   , UnionProof(..)
   , Common.difference
   , DifferenceProof(..)
+  , differenceWith
   , differenceWithKey
   , PartialDifferenceProof(..)
+  , Common.intersection
+  , intersectionWith
   , intersectionWithKey
   , IntersectionProof(..)
   -- * Traversal
+  , map
   , mapWithKey
   , traverseWithKey
   , mapAccumLWithKey
   , mapAccumRWithKey
+  , mapKeys
   , mapKeysWith
   , MapProof(..)
   , backpermuteKeys
@@ -97,10 +113,15 @@
   -- * Filter
   , Common.restrictKeys
   , Common.withoutKeys
+  , Common.filter
+  , Common.filterKeys
   , Common.filterWithKey
+  , Common.partition
   , Common.partitionWithKey
   , PartitionProof(..)
+  , mapMaybe
   , mapMaybeWithKey
+  , mapEither
   , mapEitherWithKey
   -- * Casts
   , Common.castKey
@@ -116,7 +137,7 @@
 import qualified Data.HashMap.Strict as HashMap
 import           Data.HashMap.Common.Refined
   ( HashMap(..), Key, unsafeCastKey, unsafeKey, SomeHashMapWith(..)
-  , Some2HashMapWith(..), (!)
+  , Some2HashMapWith(..), (!), zipWith
   )
 import qualified Data.HashMap.Common.Refined as Common
 import qualified Data.HashSet as HashSet
@@ -125,7 +146,7 @@
 import           Data.Traversable
 import           Data.Traversable.WithIndex
 import           Data.Type.Coercion
-import           Prelude hiding (lookup, null)
+import           Prelude hiding (lookup, map, null, zipWith)
 import           Refined
 import           Refined.Unsafe
 
@@ -144,14 +165,49 @@
 fromSet f = HashMap $ HashMap.mapWithKey (\k _ -> f $ unsafeKey k)
   $ HashSet.toMap (reflect $ Proxy @s)
 
--- | Create a map from an arbitrary traversable of key-value pairs.
+-- | Create a map from an arbitrary traversable of key-value pairs. If a key is
+-- repeated, the retained value is the last one in traversal order. If you're
+-- looking for @fromList@, this is the function you want.
+fromTraversable
+  :: forall t k a. (Traversable t, Hashable k)
+  => t (k, a) -> SomeHashMapWith (FromTraversableProof 'Hashed t k) k a
+fromTraversable xs = SomeHashMapWith (HashMap m) $ FromTraversableProof proof
+  where
+    (m, proof) = mapAccumL
+      (\s (k, v) -> let !s' = HashMap.insert k v s in (s', unsafeKey k))
+      HashMap.empty
+      xs
+
+-- | Create a map from an arbitrary traversable of key-value pairs, with a
+-- function for combining values for repeated keys. The function is called as if
+-- by 'foldl1', but flipped:
+--
+-- @
+-- 'fromTraversableWith' f [(k, x1), (k, x2), (k, x3)]
+--   = 'singleton' k (f x3 (f x2 x1))
+-- @
+fromTraversableWith
+  :: forall t k a. (Traversable t, Hashable k)
+  => (a -> a -> a)
+  -> t (k, a)
+  -> SomeHashMapWith (FromTraversableProof 'Hashed t k) k a
+fromTraversableWith f xs
+  = SomeHashMapWith (HashMap m) $ FromTraversableProof proof
+  where
+    (m, proof) = mapAccumL
+      (\s (k, v) -> let !s' = HashMap.insertWith f k v s in (s', unsafeKey k))
+      HashMap.empty
+      xs
+
+-- | Create a map from an arbitrary traversable of key-value pairs. Like
+-- 'fromTraversableWith', but the combining function has access to the key.
 fromTraversableWithKey
   :: forall t k a. (Traversable t, Hashable k)
   => (k -> a -> a -> a)
   -> t (k, a)
   -> SomeHashMapWith (FromTraversableProof 'Hashed t k) k a
-fromTraversableWithKey f xs = SomeHashMapWith (HashMap m)
-  $ FromTraversableProof proof
+fromTraversableWithKey f xs
+  = SomeHashMapWith (HashMap m) $ FromTraversableProof proof
   where
     (m, proof) = mapAccumL
       (\s (k, v)
@@ -168,8 +224,41 @@
 insert k v (HashMap m) = SomeHashMapWith (HashMap $ HashMap.insert k v m)
   $ InsertProof (unsafeKey k) unsafeSubset
 
+-- | Insert a key-value pair into the map to obtain a potentially larger map,
+-- guaranteed to contain the given key. If the key was already present, the
+-- supplied function is used to combine the new value with the old (in that
+-- order).
+insertWith
+  :: forall s k a. Hashable k
+  => (a -> a -> a)
+  -> k
+  -> a
+  -> HashMap s k a
+  -> SomeHashMapWith (InsertProof 'Hashed k s) k a
+insertWith f k v (HashMap m) = SomeHashMapWith
+  (HashMap $ HashMap.insertWith f k v m)
+  $ InsertProof (unsafeKey k) unsafeSubset
+
+-- | Insert a key-value pair into the map to obtain a potentially larger map,
+-- guaranteed to contain the given key. Like 'insertWith', but the combining
+-- function has access to the key, which is guaranteed to be in the old map.
+insertWithKey
+  :: forall s k a. Hashable k
+  => (Key s k -> a -> a -> a)
+  -> k
+  -> a
+  -> HashMap s k a
+  -> SomeHashMapWith (InsertProof 'Hashed k s) k a
+insertWithKey f k v (HashMap m) = SomeHashMapWith
+  (HashMap $ HashMap.insertWith (f $ unsafeKey k) k v m)
+  $ InsertProof (unsafeKey k) unsafeSubset
+
 -- | Overwrite a key-value pair that is known to already be in the map. The set
 -- of keys remains the same.
+--
+-- @
+-- 'reinsert' k v = 'adjust (const v) k'
+-- @
 reinsert
   :: forall s k a. Hashable k
   => Key s k -> a -> HashMap s k a -> HashMap s k a
@@ -191,12 +280,18 @@
     $ InsertProof (unsafeKey k) unsafeSubset
   )
 
+-- | If the given key is in the map, update the value at that key using the
+-- given function. In any case, the set of keys remains the same.
+adjust'
+  :: forall s k a. Hashable k => (a -> a) -> k -> HashMap s k a -> HashMap s k a
+adjust' = coerce $ HashMap.adjust @k @a
+
 -- | Update the value at a specific key known the be in the map using the given
 -- function. The set of keys remains the same.
 adjust
   :: forall s k a. Hashable k
   => (a -> a) -> Key s k -> HashMap s k a -> HashMap s k a
-adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ HashMap.adjust @k @a
+adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ adjust' @s @k @a
 
 -- | If the given key is in the map, update the associated value using the given
 -- function with a proof that the key was in the map; otherwise return the map
@@ -206,6 +301,17 @@
   => (Key s k -> a -> a) -> k -> HashMap s k a -> HashMap s k a
 adjustWithKey f k (HashMap m) = HashMap $ HashMap.adjust (f $ unsafeKey k) k m
 
+-- | If a key is present in the map, update its value or delete it using the
+-- given function, returning a potentially smaller map.
+update'
+  :: forall s k a. Hashable k
+  => (a -> Maybe a)
+  -> k
+  -> HashMap s k a
+  -> SomeHashMapWith (SupersetProof 'Hashed s) k a
+update' f k (HashMap m) = SomeHashMapWith (HashMap $ HashMap.update f k m)
+  $ SupersetProof unsafeSubset
+
 -- | Update or delete a key known to be in the map using the given function,
 -- returning a potentially smaller map.
 update
@@ -214,10 +320,21 @@
   -> Key s k
   -> HashMap s k a
   -> SomeHashMapWith (SupersetProof 'Hashed s) k a
-update f k (HashMap m)
-  = SomeHashMapWith (HashMap $ HashMap.update f (unrefine k) m)
-    $ SupersetProof unsafeSubset
+update = gcoerceWith (unsafeCastKey @s @k) $ coerce $ update' @s @k @a
 
+-- | If a key is present in the map, update its value or delete it using the
+-- given function with a proof that the key was in the map, returning a
+-- potentially smaller map.
+updateWithKey
+  :: forall s k a. Hashable k
+  => (Key s k -> a -> Maybe a)
+  -> k
+  -> HashMap s k a
+  -> SomeHashMapWith (SupersetProof 'Hashed s) k a
+updateWithKey f k (HashMap m) = SomeHashMapWith
+  (HashMap $ HashMap.update (f $ unsafeKey k) k m)
+  $ SupersetProof unsafeSubset
+
 -- | If the given key is in the map, update or delete it using the given
 -- function with a proof that the key was in the map; otherwise the map is
 -- unchanged. Alongside return the new value if it was updated, or the old value
@@ -244,6 +361,18 @@
 
 -- | Return the union of two maps, with a given combining function for keys that
 -- exist in both maps simultaneously.
+unionWith
+  :: forall s t k a. Hashable k
+  => (a -> a -> a)
+  -> HashMap s k a
+  -> HashMap t k a
+  -> SomeHashMapWith (UnionProof 'Hashed s t) k a
+unionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith
+  (HashMap $ HashMap.unionWith f m1 m2)
+  $ UnionProof unsafeSubset unsafeSubsetWith2
+
+-- | Return the union of two maps, with a given combining function for keys that
+-- exist in both maps simultaneously.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@
 -- respectively.
@@ -257,8 +386,20 @@
   (HashMap $ HashMap.unionWithKey (f . reallyUnsafeRefine) m1 m2)
   $ UnionProof unsafeSubset unsafeSubsetWith2
 
--- | For keys that appear in both maps, the given function decides whether the
--- key is removed from the first map.
+-- | Return the first map, but for keys that appear in both maps, the given
+-- function decides whether the key is removed.
+differenceWith
+  :: forall s t k a b. Hashable k
+  => (a -> b -> Maybe a)
+  -> HashMap s k a
+  -> HashMap t k b
+  -> SomeHashMapWith (PartialDifferenceProof 'Hashed s t) k a
+differenceWith f (HashMap m1) (HashMap m2) = SomeHashMapWith
+  (HashMap $ HashMap.differenceWith f m1 m2)
+  $ PartialDifferenceProof unsafeSubset unsafeSubset
+
+-- | Return the first map, but for keys that appear in both maps, the given
+-- function decides whether the key is removed.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@
 -- respectively.
@@ -276,6 +417,17 @@
   $ PartialDifferenceProof unsafeSubset unsafeSubset
 
 -- | Return the intersection of two maps with the given combining function.
+intersectionWith
+  :: forall s t k a b c. Hashable k
+  => (a -> b -> c)
+  -> HashMap s k a
+  -> HashMap t k b
+  -> SomeHashMapWith (IntersectionProof 'Hashed s t) k c
+intersectionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith
+  (HashMap $ HashMap.intersectionWith f m1 m2)
+  $ IntersectionProof unsafeSubset unsafeSubsetWith2
+
+-- | Return the intersection of two maps with the given combining function.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@
 -- respectively.
@@ -289,6 +441,10 @@
   (HashMap $ HashMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)
   $ IntersectionProof unsafeSubset unsafeSubsetWith2
 
+-- | Apply a function to all values in a map. The set of keys remains the same.
+map :: forall s k a b. (a -> b) -> HashMap s k a -> HashMap s k b
+map = coerce $ HashMap.map @a @b @k
+
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, that are proven to be in the map. The set of keys remains the same.
 mapWithKey
@@ -323,6 +479,29 @@
   -> (a, HashMap s k c)
 mapAccumRWithKey f = imapAccumR (flip f)
 
+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results
+-- into a new map. For keys that were mapped to the same new key, the value is
+-- picked in an unspecified way.
+mapKeys
+  :: forall s k1 k2 a. Hashable k2
+  => (Key s k1 -> k2)
+  -> HashMap s k1 a
+  -> SomeHashMapWith (MapProof 'Hashed s k1 k2) k2 a
+mapKeys g (HashMap m) = SomeHashMapWith
+  (HashMap $ HashMap.fromList
+    $ HashMap.foldrWithKey (\k x xs -> (g $ unsafeKey k, x) : xs) [] m)
+  $ MapProof (unsafeKey . g) \k2 ->
+    case HashMap.lookup (unrefine k2) backMap of
+      Nothing -> error
+        "mapKeys: bug: Data.HashMap.Strict.Refined has been subverted"
+      Just k1 -> k1
+  where
+    ~backMap = HashMap.fromList
+      [ (k2, unsafeKey k1)
+      | k1 <- HashMap.keys m
+      , let !k2 = g $ unsafeKey k1
+      ]
+
 -- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the
 -- results into a new map. For keys that were mapped to the same new key, @c@
 -- acts as the combining function for corresponding values.
@@ -347,6 +526,15 @@
       , let !k2 = g $ unsafeKey k1
       ]
 
+-- | Apply a function to all values in a map and collect only the 'Just'
+-- results, returning a potentially smaller map.
+mapMaybe
+  :: forall s k a b. (a -> Maybe b)
+  -> HashMap s k a
+  -> SomeHashMapWith (SupersetProof 'Hashed s) k b
+mapMaybe f (HashMap m) = SomeHashMapWith (HashMap $ HashMap.mapMaybe f m)
+  $ SupersetProof unsafeSubset
+
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, and collect only the 'Just' results, returning a potentially smaller
 -- map.
@@ -357,6 +545,27 @@
 mapMaybeWithKey f (HashMap m)
   = SomeHashMapWith (HashMap $ HashMap.mapMaybeWithKey (f . unsafeKey) m)
     $ SupersetProof unsafeSubset
+
+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'
+-- results into separate (disjoint) maps.
+mapEither
+  :: forall s k a b c. Hashable k -- TODO: this is only used in the proof
+  => (a -> Either b c)
+  -> HashMap s k a
+  -> Some2HashMapWith (PartitionProof 'Hashed s k) k b c
+mapEither p (HashMap m)
+  | m' <- HashMap.map p m
+  = Some2HashMapWith
+    (HashMap $ HashMap.mapMaybe (either Just (const Nothing)) m')
+    (HashMap $ HashMap.mapMaybe (either (const Nothing) Just) m')
+    $ PartitionProof
+      do \k -> case HashMap.lookup (unrefine k) m of
+          Nothing -> error
+            "mapEither: bug: Data.HashMap.Refined has been subverted"
+          Just x -> case p x of
+            Left _ -> Left $ unsafeKey $ unrefine k
+            Right _ -> Right $ unsafeKey $ unrefine k
+      unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g
 
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, and collect the 'Left' and 'Right' results into separate (disjoint)
diff --git a/src/Data/HashSet/Refined.hs b/src/Data/HashSet/Refined.hs
--- a/src/Data/HashSet/Refined.hs
+++ b/src/Data/HashSet/Refined.hs
@@ -165,7 +165,7 @@
 -- you a way to refer to the set (the parameter @s@), e.g.:
 --
 -- @
--- 'withHashSet' ('fromHashSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s
+-- 'withHashSet' ('fromHashSet' ...) $ \\(_ :: 'Proxy' s) -> doSomethingWith \@s
 -- @
 withHashSet
   :: forall a r. SomeHashSet a
diff --git a/src/Data/IntMap/Common/Refined.hs b/src/Data/IntMap/Common/Refined.hs
--- a/src/Data/IntMap/Common/Refined.hs
+++ b/src/Data/IntMap/Common/Refined.hs
@@ -14,11 +14,13 @@
 import           Data.Functor.WithIndex
 import qualified Data.Hashable as Hashable
 import qualified Data.IntMap as IntMap
+import qualified Data.IntSet as IntSet
 import           Data.Proxy
 import           Data.Reflection
 import           Data.Traversable.WithIndex
 import           Data.Type.Coercion
 import           Data.Type.Equality ((:~:)(..))
+import           Prelude hiding (zipWith)
 import           Refined
 import           Refined.Unsafe
 import           Unsafe.Coerce
@@ -36,6 +38,9 @@
 import qualified Data.List as List
 #endif
 
+#if MIN_VERSION_containers(0, 5, 9) || MIN_VERSION_hashable(1, 4, 0)
+import           Data.Functor.Classes
+#endif
 
 -- | A wrapper around a regular 'Data.IntMap.IntMap' with a type parameter @s@
 -- identifying the set of keys present in the map.
@@ -52,6 +57,9 @@
 #if MIN_VERSION_hashable(1, 3, 4)
   deriving newtype (Hashable.Hashable)
 #endif
+#if MIN_VERSION_containers(0, 5, 9) || MIN_VERSION_hashable(1, 4, 0)
+  deriving newtype (Eq1, Ord1, Show1)
+#endif
   deriving stock (Traversable)
 type role IntMap nominal representational
 
@@ -96,7 +104,8 @@
 -- parameter @s@), e.g.:
 --
 -- @
--- 'withIntMap' ('fromIntMap' ...) $ \(m :: 'IntMap' s a) -> doSomethingWith \@s
+-- 'withIntMap' ('fromIntMap' ...)
+--   $ \\(m :: 'IntMap' s a) -> doSomethingWith \@s
 -- @
 withIntMap :: forall a r. SomeIntMap a -> (forall s. IntMap s a -> r) -> r
 withIntMap (SomeIntMap m) k = k m
@@ -105,6 +114,14 @@
 fromIntMap :: forall a. IntMap.IntMap a -> SomeIntMap a
 fromIntMap m = SomeIntMap (IntMap m)
 
+-- | Given a set of keys @s@ known ahead of time, verify whether a regular
+-- 'Data.IntMap.IntMap' has exactly that set of keys.
+verifyIntMap
+  :: forall s a. KnownIntSet s => IntMap.IntMap a -> Maybe (IntMap s a)
+verifyIntMap m
+  | IntMap.keys m == IntSet.toList (reflect $ Proxy @s) = Just (IntMap m)
+  | otherwise = Nothing
+
 -- | An existential wrapper for an 'IntMap' with an as-yet-unknown set of keys,
 -- together with a proof of some fact @p@ about the set. Pattern matching on it
 -- gives you a way to refer to the set (the parameter @s@). Functions that
@@ -234,23 +251,36 @@
 
 -- | Given two maps proven to have the same keys, for each key apply the
 -- function to the associated values, to obtain a new map with the same keys.
-zipWithKey
-  :: forall s a b c. (Key s -> a -> b -> c)
+zipWith
+  :: forall s a b c. (a -> b -> c)
   -> IntMap s a
   -> IntMap s b
   -> IntMap s c
-zipWithKey f (IntMap m1) (IntMap m2) = IntMap
-  $ IntMap.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)
+zipWith f (IntMap m1) (IntMap m2) = IntMap
+  $ IntMap.mergeWithKey (\_ x y -> Just $ f x y)
     (\m -> if IntMap.null m
       then IntMap.empty
-      else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")
+      else error "zipWith: bug: Data.IntMap.Refined has been subverted")
     (\m -> if IntMap.null m
       then IntMap.empty
-      else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")
+      else error "zipWith: bug: Data.IntMap.Refined has been subverted")
     --  ^ Work around https://github.com/haskell/containers/issues/979
     m1
     m2
 
+-- | Return the union of two maps. For keys that exist in both maps, the value
+-- is taken from the first map.
+--
+-- @
+-- 'union' = unionWith 'const'
+-- @
+union
+  :: forall s t a. IntMap s a
+  -> IntMap t a
+  -> SomeIntMapWith (UnionProof 'Int s t) a
+union (IntMap m1) (IntMap m2) = SomeIntMapWith (IntMap $ IntMap.union m1 m2)
+  $ UnionProof unsafeSubset unsafeSubsetWith2
+
 -- | Remove the keys that appear in the second map from the first map.
 difference
   :: forall s t a b. IntMap s a
@@ -260,6 +290,19 @@
   (IntMap $ IntMap.difference m1 m2)
   $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset
 
+-- | Return the intersection of two maps, taking values from the first map.
+--
+-- @
+-- 'intersection' = intersectionWith 'const'
+-- @
+intersection
+  :: forall s t a b. IntMap s a
+  -> IntMap t b
+  -> SomeIntMapWith (IntersectionProof 'Int s t) a
+intersection (IntMap m1) (IntMap m2) = SomeIntMapWith
+  (IntMap $ IntMap.intersection m1 m2)
+  $ IntersectionProof unsafeSubset unsafeSubsetWith2
+
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, that are proven to be in the map. The set of keys remains the same.
 mapWithKey :: forall s a b. (Key s -> a -> b) -> IntMap s a -> IntMap s b
@@ -318,6 +361,29 @@
 
 -- | Retain only the key-value pairs that satisfy the predicate, returning a
 -- potentially smaller map.
+filter
+  :: forall s a. (a -> Bool)
+  -> IntMap s a
+  -> SomeIntMapWith (SupersetProof 'Int s) a
+filter p (IntMap m) = SomeIntMapWith (IntMap $ IntMap.filter p m)
+  $ SupersetProof unsafeSubset
+
+-- | Retain only the key-value pairs that satisfy the predicate, returning a
+-- potentially smaller map.
+filterKeys
+  :: forall s a. (Key s -> Bool)
+  -> IntMap s a
+  -> SomeIntMapWith (SupersetProof 'Int s) a
+filterKeys p (IntMap m) = SomeIntMapWith
+#if MIN_VERSION_containers(0, 8, 0)
+  (IntMap $ IntMap.filterKeys (p . unsafeKey) m)
+#else
+  (IntMap $ IntMap.filterWithKey (\k _ -> p (unsafeKey k)) m)
+#endif
+  $ SupersetProof unsafeSubset
+
+-- | Retain only the key-value pairs that satisfy the predicate, returning a
+-- potentially smaller map.
 filterWithKey
   :: forall s a. (Key s -> a -> Bool)
   -> IntMap s a
@@ -351,6 +417,22 @@
 #endif
   $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset
 
+-- | Partition a map into two disjoint submaps: those whose values satisfy the
+-- predicate, and those whose don't.
+partition
+  :: forall s a. (a -> Bool)
+  -> IntMap s a
+  -> Some2IntMapWith (PartitionProof 'Int s Int) a a
+partition p (IntMap m) = case IntMap.partition p m of
+  (m1, m2) -> Some2IntMapWith (IntMap m1) (IntMap m2) $ PartitionProof
+    do \k -> case IntMap.lookup (unrefine k) m of
+        Nothing -> error
+          "partition: bug: Data.IntMap.Refined has been subverted"
+        Just x -> if p x
+          then Left $ unsafeKey $ unrefine k
+          else Right $ unsafeKey $ unrefine k
+    unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g
+
 -- | Partition a map into two disjoint submaps: those whose key-value pairs
 -- satisfy the predicate, and those whose don't.
 partitionWithKey
@@ -368,6 +450,43 @@
             else Right $ unsafeKey $ unrefine k
       unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g
 
+-- | Take the a submap of keys up to a point where the predicate stops holding.
+--
+-- If @p@ is antitone ( \(\forall x y, x < y \implies p(x) \ge p(y)\) ), then
+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is
+-- chosen in an unspecified way.
+takeWhileAntitone
+  :: forall s a. (Key s -> Bool)
+  -> IntMap s a
+  -> SomeIntMapWith (SupersetProof 'Int s) a
+takeWhileAntitone p (IntMap m) = SomeIntMapWith
+#if MIN_VERSION_containers(0, 6, 7)
+  (IntMap $ IntMap.takeWhileAntitone (p . unsafeKey) m)
+#else
+  (IntMap $ IntMap.fromDistinctAscList
+    $ List.takeWhile (p . unsafeKey . fst) $ IntMap.toAscList m)
+#endif
+  $ SupersetProof unsafeSubset
+
+-- | Take the a submap of keys starting from a point where the predicate stops
+-- holding.
+--
+-- If @p@ is antitone ( \(\forall x y, x < y \implies p(x) \ge p(y)\) ), then
+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is
+-- chosen in an unspecified way.
+dropWhileAntitone
+  :: forall s a. (Key s -> Bool)
+  -> IntMap s a
+  -> SomeIntMapWith (SupersetProof 'Int s) a
+dropWhileAntitone p (IntMap m) = SomeIntMapWith
+#if MIN_VERSION_containers(0, 6, 7)
+  (IntMap $ IntMap.dropWhileAntitone (p . unsafeKey) m)
+#else
+  (IntMap $ IntMap.fromDistinctAscList
+    $ List.dropWhile (p . unsafeKey . fst) $ IntMap.toAscList m)
+#endif
+  $ SupersetProof unsafeSubset
+
 -- | Divide a map into two disjoint submaps at a point where the predicate on
 -- the keys stops holding.
 --
@@ -442,17 +561,17 @@
 castKey = castRefined
 
 -- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps
--- can be interconverted too. For example, 'zipWithKey' can be implemented via
--- 'Data.IntMap.Refined.intersectionWithKey' by proving that the set of keys
--- remains unchanged:
+-- can be interconverted too. For example, 'Data.IntMap.Refined.zipWithKey' can
+-- be implemented via 'Data.IntMap.Refined.intersectionWithKey' by proving that
+-- the set of keys remains unchanged:
 --
 -- @
--- 'zipWithKey'
+-- 'Data.IntMap.Refined.zipWithKey'
 --   :: forall s a b c. ('Key' s -> a -> b -> c)
 --   -> 'IntMap' s a
 --   -> 'IntMap' s b
 --   -> 'IntMap' s c
--- 'zipWithKey' f m1 m2
+-- 'Data.IntMap.Refined.zipWithKey' f m1 m2
 --   | v'SomeIntMapWith' @r m proof <- 'Data.IntMap.Refined.intersectionWithKey' (f . 'andLeft') m1 m2
 --   , v'IntersectionProof' p1 p2 <- proof
 --   , ( v'Coercion' :: t'Coercion' ('IntMap' r c) ('IntMap' s c))
@@ -479,10 +598,10 @@
   itraverse = traverseWithKey
 
 -- | Similar to the instance for functions -- zip corresponding keys. To use
--- '<*>'/'Control.Applicative.liftA2' without 'KnownIntSet' see 'zipWithKey'.
+-- '<*>'/'Control.Applicative.liftA2' without 'KnownIntSet' see 'zipWith'.
 instance  KnownIntSet s => Applicative (IntMap s) where
   pure x = fromSet \_ -> x
-  (<*>) = zipWithKey (const id)
+  (<*>) = zipWith id
 
 -- | @'bind' m f@ is a map that for each key @k :: 'Key' s@, contains the
 -- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.
@@ -502,7 +621,7 @@
 
 -- | Append the values at the corresponding keys
 instance Semigroup a => Semigroup (IntMap s a) where
-  (<>) = zipWithKey (const (<>))
+  (<>) = zipWith (<>)
 
 instance (KnownIntSet s, Monoid a) => Monoid (IntMap s a) where
   mempty = fromSet \_ -> mempty
diff --git a/src/Data/IntMap/Refined.hs b/src/Data/IntMap/Refined.hs
--- a/src/Data/IntMap/Refined.hs
+++ b/src/Data/IntMap/Refined.hs
@@ -34,18 +34,26 @@
   , SingletonProof(..)
   , fromSet
   , Common.fromIntMap
+  , Common.verifyIntMap
+  , fromTraversable
+  , fromTraversableWith
   , fromTraversableWithKey
   , FromTraversableProof(..)
   -- * Insertion
   , insert
+  , insertWith
+  , insertWithKey
   , InsertProof(..)
   , reinsert
   , insertLookupWithKey
   -- * Deletion/Update
   , Common.delete
+  , adjust'
   , adjust
   , adjustWithKey
+  , update'
   , update
+  , updateWithKey
   , updateLookupWithKey
   -- * Query
   , Common.lookup
@@ -61,21 +69,29 @@
   , Common.disjoint
   , DisjointProof(..)
   -- * Combine
+  , zipWith
   , zipWithKey
   , bind
+  , Common.union
+  , unionWith
   , unionWithKey
   , UnionProof(..)
   , Common.difference
   , DifferenceProof(..)
+  , differenceWith
   , differenceWithKey
   , PartialDifferenceProof(..)
+  , Common.intersection
+  , intersectionWith
   , intersectionWithKey
   , IntersectionProof(..)
   -- * Traversal
+  , map
   , mapWithKey
   , traverseWithKey
   , mapAccumLWithKey
   , mapAccumRWithKey
+  , mapKeys
   , mapKeysWith
   , MapProof(..)
   , backpermuteKeys
@@ -93,12 +109,19 @@
   -- * Filter
   , Common.restrictKeys
   , Common.withoutKeys
+  , Common.filter
+  , Common.filterKeys
   , Common.filterWithKey
+  , Common.partition
   , Common.partitionWithKey
   , PartitionProof(..)
+  , Common.takeWhileAntitone
+  , Common.dropWhileAntitone
   , Common.spanAntitone
   , PartialPartitionProof(..)
+  , mapMaybe
   , mapMaybeWithKey
+  , mapEither
   , mapEitherWithKey
   , Common.splitLookup
   , SplitProof(..)
@@ -122,13 +145,13 @@
 import qualified Data.IntMap as IntMap
 import           Data.IntMap.Common.Refined
   ( IntMap(..), Key, unsafeCastKey, unsafeKey, SomeIntMapWith(..)
-  , Some2IntMapWith(..), fromSet, (!), zipWithKey, mapWithKey, traverseWithKey
+  , Some2IntMapWith(..), fromSet, (!), zipWith, mapWithKey, traverseWithKey
   , bind
   )
 import qualified Data.IntMap.Common.Refined as Common
 import           Data.Traversable
 import           Data.Type.Coercion
-import           Prelude hiding (lookup, null)
+import           Prelude hiding (lookup, map, null, zipWith)
 import           Refined
 import           Refined.Unsafe
 
@@ -139,7 +162,42 @@
 singleton k v = SomeIntMapWith (IntMap $ IntMap.singleton k v)
   $ SingletonProof (unsafeKey k)
 
--- | Create a map from an arbitrary traversable of key-value pairs.
+-- | Create a map from an arbitrary traversable of key-value pairs. If a key is
+-- repeated, the retained value is the last one in traversal order. If you're
+-- looking for @fromList@, this is the function you want.
+fromTraversable
+  :: forall t a. Traversable t
+  => t (Int, a) -> SomeIntMapWith (FromTraversableProof 'Int t Int) a
+fromTraversable xs = SomeIntMapWith (IntMap m) $ FromTraversableProof proof
+  where
+    (m, proof) = mapAccumL
+      (\s (k, v) -> let !s' = IntMap.insert k v s in (s', unsafeKey k))
+      IntMap.empty
+      xs
+
+-- | Create a map from an arbitrary traversable of key-value pairs, with a
+-- function for combining values for repeated keys. The function is called as if
+-- by 'foldl1', but flipped:
+--
+-- @
+-- 'fromTraversableWith' f [(k, x1), (k, x2), (k, x3)]
+--   = 'singleton' k (f x3 (f x2 x1))
+-- @
+fromTraversableWith
+  :: forall t a. Traversable t
+  => (a -> a -> a)
+  -> t (Int, a)
+  -> SomeIntMapWith (FromTraversableProof 'Int t Int) a
+fromTraversableWith f xs
+  = SomeIntMapWith (IntMap m) $ FromTraversableProof proof
+  where
+    (m, proof) = mapAccumL
+      (\s (k, v) -> let !s' = IntMap.insertWith f k v s in (s', unsafeKey k))
+      IntMap.empty
+      xs
+
+-- | Create a map from an arbitrary traversable of key-value pairs. Like
+-- 'fromTraversableWith', but the combining function has access to the key.
 fromTraversableWithKey
   :: forall t a. Traversable t
   => (Int -> a -> a -> a)
@@ -164,6 +222,33 @@
 insert k v (IntMap m) = SomeIntMapWith (IntMap $ IntMap.insert k v m)
   $ InsertProof (unsafeKey k) unsafeSubset
 
+-- | Insert a key-value pair into the map to obtain a potentially larger map,
+-- guaranteed to contain the given key. If the key was already present, the
+-- supplied function is used to combine the new value with the old (in that
+-- order).
+insertWith
+  :: forall s a. (a -> a -> a)
+  -> Int
+  -> a
+  -> IntMap s a
+  -> SomeIntMapWith (InsertProof 'Int Int s) a
+insertWith f k v (IntMap m) = SomeIntMapWith
+  (IntMap $ IntMap.insertWith f k v m)
+  $ InsertProof (unsafeKey k) unsafeSubset
+
+-- | Insert a key-value pair into the map to obtain a potentially larger map,
+-- guaranteed to contain the given key. Like 'insertWith', but the combining
+-- function has access to the key, which is guaranteed to be in the old map.
+insertWithKey
+  :: forall s a. (Key s -> a -> a -> a)
+  -> Int
+  -> a
+  -> IntMap s a
+  -> SomeIntMapWith (InsertProof 'Int Int s) a
+insertWithKey f k v (IntMap m) = SomeIntMapWith
+  (IntMap $ IntMap.insertWithKey (f . unsafeKey) k v m)
+  $ InsertProof (unsafeKey k) unsafeSubset
+
 -- | Overwrite a key-value pair that is known to already be in the map. The set
 -- of keys remains the same.
 reinsert
@@ -184,10 +269,19 @@
     (v', !m') -> ((unsafeKey k,) <$> v',)
       $ SomeIntMapWith (IntMap m') $ InsertProof (unsafeKey k) unsafeSubset
 
+-- | If the given key is in the map, update the value at that key using the
+-- given function. In any case, the set of keys remains the same.
+adjust' :: forall s a. (a -> a) -> Int -> IntMap s a -> IntMap s a
+adjust' = coerce $ IntMap.adjust @a
+
 -- | Update the value at a specific key known the be in the map using the given
 -- function. The set of keys remains the same.
+--
+-- @
+-- 'reinsert' k v = 'adjust (const v) k'
+-- @
 adjust :: forall s a. (a -> a) -> Key s -> IntMap s a -> IntMap s a
-adjust = gcoerceWith (unsafeCastKey @s) $ coerce $ IntMap.adjust @a
+adjust = gcoerceWith (unsafeCastKey @s) $ coerce $ adjust' @s @a
 
 -- | If the given key is in the map, update the associated value using the given
 -- function with a proof that the key was in the map; otherwise return the map
@@ -197,6 +291,16 @@
 adjustWithKey = gcoerceWith (unsafeCastKey @s) $ coerce
   $ IntMap.adjustWithKey @a
 
+-- | If a key is present in the map, update its value or delete it using the
+-- given function, returning a potentially smaller map.
+update'
+  :: forall s a. (a -> Maybe a)
+  -> Int
+  -> IntMap s a
+  -> SomeIntMapWith (SupersetProof 'Int s) a
+update' f k (IntMap m) = SomeIntMapWith (IntMap $ IntMap.update f k m)
+  $ SupersetProof unsafeSubset
+
 -- | Update or delete a key known to be in the map using the given function,
 -- returning a potentially smaller map.
 update
@@ -204,7 +308,18 @@
   -> Key s
   -> IntMap s a
   -> SomeIntMapWith (SupersetProof 'Int s) a
-update f k (IntMap m) = SomeIntMapWith (IntMap $ IntMap.update f (unrefine k) m)
+update = gcoerceWith (unsafeCastKey @s) $ coerce $ update' @s @a
+
+-- | If a key is present in the map, update its value or delete it using the
+-- given function with a proof that the key was in the map, returning a
+-- potentially smaller map.
+updateWithKey
+  :: forall s a. (Key s -> a -> Maybe a)
+  -> Int
+  -> IntMap s a
+  -> SomeIntMapWith (SupersetProof 'Int s) a
+updateWithKey f k (IntMap m) = SomeIntMapWith
+  (IntMap $ IntMap.updateWithKey (f . unsafeKey) k m)
   $ SupersetProof unsafeSubset
 
 -- | If the given key is in the map, update or delete it using the given
@@ -221,8 +336,38 @@
     (v', !m') -> ((unsafeKey k,) <$> v',)
       $ SomeIntMapWith (IntMap m') $ SupersetProof unsafeSubset
 
+-- | Given two maps proven to have the same keys, for each key apply the
+-- function to the associated values, to obtain a new map with the same keys.
+zipWithKey
+  :: forall s a b c. (Key s -> a -> b -> c)
+  -> IntMap s a
+  -> IntMap s b
+  -> IntMap s c
+zipWithKey f (IntMap m1) (IntMap m2) = IntMap
+  $ IntMap.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)
+    (\m -> if IntMap.null m
+      then IntMap.empty
+      else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")
+    (\m -> if IntMap.null m
+      then IntMap.empty
+      else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")
+    --  ^ Work around https://github.com/haskell/containers/issues/979
+    m1
+    m2
+
 -- | Return the union of two maps, with a given combining function for keys that
 -- exist in both maps simultaneously.
+unionWith
+  :: forall s t a. (a -> a -> a)
+  -> IntMap s a
+  -> IntMap t a
+  -> SomeIntMapWith (UnionProof 'Int s t) a
+unionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith
+  (IntMap $ IntMap.unionWith f m1 m2)
+  $ UnionProof unsafeSubset unsafeSubsetWith2
+
+-- | Return the union of two maps, with a given combining function for keys that
+-- exist in both maps simultaneously.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@
 -- respectively.
@@ -235,8 +380,19 @@
   = SomeIntMapWith (IntMap $ IntMap.unionWithKey (f . reallyUnsafeRefine) m1 m2)
     $ UnionProof unsafeSubset unsafeSubsetWith2
 
--- | For keys that appear in both maps, the given function decides whether the
--- key is removed from the first map.
+-- | Return the first map, but for keys that appear in both maps, the given
+-- function decides whether the key is removed.
+differenceWith
+  :: forall s t a b. (a -> b -> Maybe a)
+  -> IntMap s a
+  -> IntMap t b
+  -> SomeIntMapWith (PartialDifferenceProof 'Int s t) a
+differenceWith f (IntMap m1) (IntMap m2) = SomeIntMapWith
+  (IntMap $ IntMap.differenceWith f m1 m2)
+  $ PartialDifferenceProof unsafeSubset unsafeSubset
+
+-- | Return the first map, but for keys that appear in both maps, the given
+-- function decides whether the key is removed.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@
 -- respectively.
@@ -253,6 +409,16 @@
   $ PartialDifferenceProof unsafeSubset unsafeSubset
 
 -- | Return the intersection of two maps with the given combining function.
+intersectionWith
+  :: forall s t a b c. (a -> b -> c)
+  -> IntMap s a
+  -> IntMap t b
+  -> SomeIntMapWith (IntersectionProof 'Int s t) c
+intersectionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith
+  (IntMap $ IntMap.intersectionWith f m1 m2)
+  $ IntersectionProof unsafeSubset unsafeSubsetWith2
+
+-- | Return the intersection of two maps with the given combining function.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@
 -- respectively.
@@ -268,6 +434,10 @@
   (IntMap $ IntMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)
   $ IntersectionProof unsafeSubset unsafeSubsetWith2
 
+-- | Apply a function to all values in a map. The set of keys remains the same.
+map :: forall s a b. (a -> b) -> IntMap s a -> IntMap s b
+map = coerce $ IntMap.map @a @b
+
 -- | Thread an accumularing argument through the map in ascending order of keys.
 mapAccumLWithKey
   :: forall s a b c. (a -> Key s -> b -> (a, c))
@@ -287,6 +457,27 @@
 mapAccumRWithKey = gcoerceWith (unsafeCastKey @s) $ coerce
   $ IntMap.mapAccumRWithKey @a @b @c
 
+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results
+-- into a new map. For keys that were mapped to the same new key, the value
+-- corresponding to the greatest of the original keys is retained.
+mapKeys
+  :: forall s a. (Key s -> Int)
+  -> IntMap s a
+  -> SomeIntMapWith (MapProof 'Int s Int Int) a
+mapKeys g (IntMap m)
+  = SomeIntMapWith (IntMap $ IntMap.mapKeys (g . unsafeKey) m)
+    $ MapProof (unsafeKey . g) \k2 ->
+      case IntMap.lookup (unrefine k2) backMap of
+        Nothing -> error
+          "mapKeys: bug: Data.IntMap.Refined has been subverted"
+        Just k1 -> k1
+  where
+    ~backMap = IntMap.fromList
+      [ (k2, unsafeKey k1)
+      | k1 <- IntMap.keys m
+      , let !k2 = g $ unsafeKey k1
+      ]
+
 -- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the
 -- results into a new map. For keys that were mapped to the same new key, @c@
 -- acts as the combining function for corresponding values.
@@ -309,6 +500,15 @@
       , let !k2 = g $ unsafeKey k1
       ]
 
+-- | Apply a function to all values in a map and collect only the 'Just'
+-- results, returning a potentially smaller map.
+mapMaybe
+  :: forall s a b. (a -> Maybe b)
+  -> IntMap s a
+  -> SomeIntMapWith (SupersetProof 'Int s) b
+mapMaybe f (IntMap m) = SomeIntMapWith (IntMap $ IntMap.mapMaybe f m)
+  $ SupersetProof unsafeSubset
+
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, and collect only the 'Just' results, returning a potentially smaller
 -- map.
@@ -319,6 +519,23 @@
 mapMaybeWithKey f (IntMap m)
   = SomeIntMapWith (IntMap $ IntMap.mapMaybeWithKey (f . unsafeKey) m)
     $ SupersetProof unsafeSubset
+
+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'
+-- results into separate (disjoint) maps.
+mapEither
+  :: forall s a b c. (a -> Either b c)
+  -> IntMap s a
+  -> Some2IntMapWith (PartitionProof 'Int s Int) b c
+mapEither p (IntMap m)
+  = case IntMap.mapEither p m of
+    (m1, m2) -> Some2IntMapWith (IntMap m1) (IntMap m2) $ PartitionProof
+      do \k -> case IntMap.lookup (unrefine k) m of
+          Nothing -> error
+            "mapEither: bug: Data.IntMap.Refined has been subverted"
+          Just x -> case p x of
+            Left _ -> Left $ unsafeKey $ unrefine k
+            Right _ -> Right $ unsafeKey $ unrefine k
+      unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g
 
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, and collect the 'Left' and 'Right' results into separate (disjoint)
diff --git a/src/Data/IntMap/Strict/Refined.hs b/src/Data/IntMap/Strict/Refined.hs
--- a/src/Data/IntMap/Strict/Refined.hs
+++ b/src/Data/IntMap/Strict/Refined.hs
@@ -34,18 +34,26 @@
   , SingletonProof(..)
   , fromSet
   , Common.fromIntMap
+  , Common.verifyIntMap
+  , fromTraversable
+  , fromTraversableWith
   , fromTraversableWithKey
   , FromTraversableProof(..)
   -- * Insertion
   , insert
+  , insertWith
+  , insertWithKey
   , InsertProof(..)
   , reinsert
   , insertLookupWithKey
   -- * Deletion/Update
   , Common.delete
+  , adjust'
   , adjust
   , adjustWithKey
+  , update'
   , update
+  , updateWithKey
   , updateLookupWithKey
   -- * Query
   , Common.lookup
@@ -61,21 +69,29 @@
   , Common.disjoint
   , DisjointProof(..)
   -- * Combine
+  , zipWith
   , zipWithKey
   , bind
+  , Common.union
+  , unionWith
   , unionWithKey
   , UnionProof(..)
   , Common.difference
   , DifferenceProof(..)
+  , differenceWith
   , differenceWithKey
   , PartialDifferenceProof(..)
+  , Common.intersection
+  , intersectionWith
   , intersectionWithKey
   , IntersectionProof(..)
   -- * Traversal
+  , map
   , mapWithKey
   , traverseWithKey
   , mapAccumLWithKey
   , mapAccumRWithKey
+  , mapKeys
   , mapKeysWith
   , MapProof(..)
   , backpermuteKeys
@@ -93,12 +109,19 @@
   -- * Filter
   , Common.restrictKeys
   , Common.withoutKeys
+  , Common.filter
+  , Common.filterKeys
   , Common.filterWithKey
+  , Common.partition
   , Common.partitionWithKey
   , PartitionProof(..)
+  , Common.takeWhileAntitone
+  , Common.dropWhileAntitone
   , Common.spanAntitone
   , PartialPartitionProof(..)
+  , mapMaybe
   , mapMaybeWithKey
+  , mapEither
   , mapEitherWithKey
   , Common.splitLookup
   , SplitProof(..)
@@ -122,14 +145,14 @@
 import qualified Data.IntMap.Strict as IntMap
 import           Data.IntMap.Common.Refined
   ( IntMap(..), Key, unsafeCastKey, unsafeKey, SomeIntMapWith(..)
-  , Some2IntMapWith(..), (!)
+  , Some2IntMapWith(..), (!), zipWith
   )
 import qualified Data.IntMap.Common.Refined as Common
 import           Data.Proxy
 import           Data.Reflection
 import           Data.Traversable
 import           Data.Type.Coercion
-import           Prelude hiding (lookup, null)
+import           Prelude hiding (lookup, map, null, zipWith)
 import           Refined
 import           Refined.Unsafe
 
@@ -145,17 +168,52 @@
 fromSet :: forall s a. KnownIntSet s => (Key s -> a) -> IntMap s a
 fromSet f = IntMap $ IntMap.fromSet (f . unsafeKey) (reflect $ Proxy @s)
 
--- | Create a map from an arbitrary traversable of key-value pairs.
+-- | Create a map from an arbitrary traversable of key-value pairs. If a key is
+-- repeated, the retained value is the last one in traversal order. If you're
+-- looking for @fromList@, this is the function you want.
+fromTraversable
+  :: forall t a. Traversable t
+  => t (Int, a) -> SomeIntMapWith (FromTraversableProof 'Int t Int) a
+fromTraversable xs = SomeIntMapWith (IntMap m) $ FromTraversableProof proof
+  where
+    (m, proof) = mapAccumL
+      (\s (k, v) -> let !s' = IntMap.insert k v s in (s', unsafeKey k))
+      IntMap.empty
+      xs
+
+-- | Create a map from an arbitrary traversable of key-value pairs, with a
+-- function for combining values for repeated keys. The function is called as if
+-- by 'foldl1', but flipped:
+--
+-- @
+-- 'fromTraversableWith' f [(k, x1), (k, x2), (k, x3)]
+--   = 'singleton' k (f x3 (f x2 x1))
+-- @
+fromTraversableWith
+  :: forall t a. Traversable t
+  => (a -> a -> a)
+  -> t (Int, a)
+  -> SomeIntMapWith (FromTraversableProof 'Int t Int) a
+fromTraversableWith f xs
+  = SomeIntMapWith (IntMap m) $ FromTraversableProof proof
+  where
+    (m, proof) = mapAccumL
+      (\s (k, v) -> let !s' = IntMap.insertWith f k v s in (s', unsafeKey k))
+      IntMap.empty
+      xs
+
+-- | Create a map from an arbitrary traversable of key-value pairs. Like
+-- 'fromTraversableWith', but the combining function has access to the key.
 fromTraversableWithKey
   :: forall t a. Traversable t
   => (Int -> a -> a -> a)
   -> t (Int, a)
   -> SomeIntMapWith (FromTraversableProof 'Int t Int) a
-fromTraversableWithKey f xs = SomeIntMapWith (IntMap m)
-  $ FromTraversableProof proof
+fromTraversableWithKey f xs
+  = SomeIntMapWith (IntMap m) $ FromTraversableProof proof
   where
     (m, proof) = mapAccumL
-      (\s (k, v) -> (IntMap.insertWithKey f k v s, unsafeKey k))
+      (\s (k, v) -> let !s' = IntMap.insertWithKey f k v s in (s', unsafeKey k))
       IntMap.empty
       xs
 
@@ -170,8 +228,39 @@
 insert k v (IntMap m) = SomeIntMapWith (IntMap $ IntMap.insert k v m)
   $ InsertProof (unsafeKey k) unsafeSubset
 
+-- | Insert a key-value pair into the map to obtain a potentially larger map,
+-- guaranteed to contain the given key. If the key was already present, the
+-- supplied function is used to combine the new value with the old (in that
+-- order).
+insertWith
+  :: forall s a. (a -> a -> a)
+  -> Int
+  -> a
+  -> IntMap s a
+  -> SomeIntMapWith (InsertProof 'Int Int s) a
+insertWith f k v (IntMap m) = SomeIntMapWith
+  (IntMap $ IntMap.insertWith f k v m)
+  $ InsertProof (unsafeKey k) unsafeSubset
+
+-- | Insert a key-value pair into the map to obtain a potentially larger map,
+-- guaranteed to contain the given key. Like 'insertWith', but the combining
+-- function has access to the key, which is guaranteed to be in the old map.
+insertWithKey
+  :: forall s a. (Key s -> a -> a -> a)
+  -> Int
+  -> a
+  -> IntMap s a
+  -> SomeIntMapWith (InsertProof 'Int Int s) a
+insertWithKey f k v (IntMap m) = SomeIntMapWith
+  (IntMap $ IntMap.insertWithKey (f . unsafeKey) k v m)
+  $ InsertProof (unsafeKey k) unsafeSubset
+
 -- | Overwrite a key-value pair that is known to already be in the map. The set
 -- of keys remains the same.
+--
+-- @
+-- 'reinsert' k v = 'adjust (const v) k'
+-- @
 reinsert
   :: forall s a. Key s -> a -> IntMap s a -> IntMap s a
 reinsert = gcoerceWith (unsafeCastKey @s) $ coerce $ IntMap.insert @a
@@ -190,10 +279,15 @@
     (v', !m') -> ((unsafeKey k,) <$> v',)
       $ SomeIntMapWith (IntMap m') $ InsertProof (unsafeKey k) unsafeSubset
 
+-- | If the given key is in the map, update the value at that key using the
+-- given function. In any case, the set of keys remains the same.
+adjust' :: forall s a. (a -> a) -> Int -> IntMap s a -> IntMap s a
+adjust' = coerce $ IntMap.adjust @a
+
 -- | Update the value at a specific key known the be in the map using the given
 -- function. The set of keys remains the same.
 adjust :: forall s a. (a -> a) -> Key s -> IntMap s a -> IntMap s a
-adjust = gcoerceWith (unsafeCastKey @s) $ coerce $ IntMap.adjust @a
+adjust = gcoerceWith (unsafeCastKey @s) $ coerce $ adjust' @s @a
 
 -- | If the given key is in the map, update the associated value using the given
 -- function with a proof that the key was in the map; otherwise return the map
@@ -203,6 +297,16 @@
 adjustWithKey = gcoerceWith (unsafeCastKey @s) $ coerce
   $ IntMap.adjustWithKey @a
 
+-- | If a key is present in the map, update its value or delete it using the
+-- given function, returning a potentially smaller map.
+update'
+  :: forall s a. (a -> Maybe a)
+  -> Int
+  -> IntMap s a
+  -> SomeIntMapWith (SupersetProof 'Int s) a
+update' f k (IntMap m) = SomeIntMapWith (IntMap $ IntMap.update f k m)
+  $ SupersetProof unsafeSubset
+
 -- | Update or delete a key known to be in the map using the given function,
 -- returning a potentially smaller map.
 update
@@ -210,7 +314,18 @@
   -> Key s
   -> IntMap s a
   -> SomeIntMapWith (SupersetProof 'Int s) a
-update f k (IntMap m) = SomeIntMapWith (IntMap $ IntMap.update f (unrefine k) m)
+update = gcoerceWith (unsafeCastKey @s) $ coerce $ update' @s @a
+
+-- | If a key is present in the map, update its value or delete it using the
+-- given function with a proof that the key was in the map, returning a
+-- potentially smaller map.
+updateWithKey
+  :: forall s a. (Key s -> a -> Maybe a)
+  -> Int
+  -> IntMap s a
+  -> SomeIntMapWith (SupersetProof 'Int s) a
+updateWithKey f k (IntMap m) = SomeIntMapWith
+  (IntMap $ IntMap.updateWithKey (f . unsafeKey) k m)
   $ SupersetProof unsafeSubset
 
 -- | If the given key is in the map, update or delete it using the given
@@ -250,6 +365,17 @@
 
 -- | Return the union of two maps, with a given combining function for keys that
 -- exist in both maps simultaneously.
+unionWith
+  :: forall s t a. (a -> a -> a)
+  -> IntMap s a
+  -> IntMap t a
+  -> SomeIntMapWith (UnionProof 'Int s t) a
+unionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith
+  (IntMap $ IntMap.unionWith f m1 m2)
+  $ UnionProof unsafeSubset unsafeSubsetWith2
+
+-- | Return the union of two maps, with a given combining function for keys that
+-- exist in both maps simultaneously.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@
 -- respectively.
@@ -262,8 +388,19 @@
   = SomeIntMapWith (IntMap $ IntMap.unionWithKey (f . reallyUnsafeRefine) m1 m2)
     $ UnionProof unsafeSubset unsafeSubsetWith2
 
--- | For keys that appear in both maps, the given function decides whether the
--- key is removed from the first map.
+-- | Return the first map, but for keys that appear in both maps, the given
+-- function decides whether the key is removed.
+differenceWith
+  :: forall s t a b. (a -> b -> Maybe a)
+  -> IntMap s a
+  -> IntMap t b
+  -> SomeIntMapWith (PartialDifferenceProof 'Int s t) a
+differenceWith f (IntMap m1) (IntMap m2) = SomeIntMapWith
+  (IntMap $ IntMap.differenceWith f m1 m2)
+  $ PartialDifferenceProof unsafeSubset unsafeSubset
+
+-- | Return the first map, but for keys that appear in both maps, the given
+-- function decides whether the key is removed.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@
 -- respectively.
@@ -280,6 +417,16 @@
   $ PartialDifferenceProof unsafeSubset unsafeSubset
 
 -- | Return the intersection of two maps with the given combining function.
+intersectionWith
+  :: forall s t a b c. (a -> b -> c)
+  -> IntMap s a
+  -> IntMap t b
+  -> SomeIntMapWith (IntersectionProof 'Int s t) c
+intersectionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith
+  (IntMap $ IntMap.intersectionWith f m1 m2)
+  $ IntersectionProof unsafeSubset unsafeSubsetWith2
+
+-- | Return the intersection of two maps with the given combining function.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@
 -- respectively.
@@ -295,6 +442,10 @@
   (IntMap $ IntMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)
   $ IntersectionProof unsafeSubset unsafeSubsetWith2
 
+-- | Apply a function to all values in a map. The set of keys remains the same.
+map :: forall s a b. (a -> b) -> IntMap s a -> IntMap s b
+map = coerce $ IntMap.map @a @b
+
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, that are proven to be in the map. The set of keys remains the same.
 mapWithKey :: forall s a b. (Key s -> a -> b) -> IntMap s a -> IntMap s b
@@ -328,6 +479,27 @@
 mapAccumRWithKey = gcoerceWith (unsafeCastKey @s) $ coerce
   $ IntMap.mapAccumRWithKey @a @b @c
 
+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results
+-- into a new map. For keys that were mapped to the same new key, the value
+-- corresponding to the greatest of the original keys is retained.
+mapKeys
+  :: forall s a. (Key s -> Int)
+  -> IntMap s a
+  -> SomeIntMapWith (MapProof 'Int s Int Int) a
+mapKeys g (IntMap m)
+  = SomeIntMapWith (IntMap $ IntMap.mapKeys (g . unsafeKey) m)
+    $ MapProof (unsafeKey . g) \k2 ->
+      case IntMap.lookup (unrefine k2) backMap of
+        Nothing -> error
+          "mapKeys: bug: Data.IntMap.Strict.Refined has been subverted"
+        Just k1 -> k1
+  where
+    ~backMap = IntMap.fromList
+      [ (k2, unsafeKey k1)
+      | k1 <- IntMap.keys m
+      , let !k2 = g $ unsafeKey k1
+      ]
+
 -- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the
 -- results into a new map. For keys that were mapped to the same new key, @c@
 -- acts as the combining function for corresponding values.
@@ -350,6 +522,15 @@
       , let !k2 = g $ unsafeKey k1
       ]
 
+-- | Apply a function to all values in a map and collect only the 'Just'
+-- results, returning a potentially smaller map.
+mapMaybe
+  :: forall s a b. (a -> Maybe b)
+  -> IntMap s a
+  -> SomeIntMapWith (SupersetProof 'Int s) b
+mapMaybe f (IntMap m) = SomeIntMapWith (IntMap $ IntMap.mapMaybe f m)
+  $ SupersetProof unsafeSubset
+
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, and collect only the 'Just' results, returning a potentially smaller
 -- map.
@@ -360,6 +541,23 @@
 mapMaybeWithKey f (IntMap m)
   = SomeIntMapWith (IntMap $ IntMap.mapMaybeWithKey (f . unsafeKey) m)
     $ SupersetProof unsafeSubset
+
+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'
+-- results into separate (disjoint) maps.
+mapEither
+  :: forall s a b c. (a -> Either b c)
+  -> IntMap s a
+  -> Some2IntMapWith (PartitionProof 'Int s Int) b c
+mapEither p (IntMap m)
+  = case IntMap.mapEither p m of
+    (m1, m2) -> Some2IntMapWith (IntMap m1) (IntMap m2) $ PartitionProof
+      do \k -> case IntMap.lookup (unrefine k) m of
+          Nothing -> error
+            "mapEither: bug: Data.IntMap.Refined has been subverted"
+          Just x -> case p x of
+            Left _ -> Left $ unsafeKey $ unrefine k
+            Right _ -> Right $ unsafeKey $ unrefine k
+      unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g
 
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, and collect the 'Left' and 'Right' results into separate (disjoint)
diff --git a/src/Data/IntSet/Refined.hs b/src/Data/IntSet/Refined.hs
--- a/src/Data/IntSet/Refined.hs
+++ b/src/Data/IntSet/Refined.hs
@@ -169,7 +169,7 @@
 -- you a way to refer to the set (the parameter @s@), e.g.:
 --
 -- @
--- 'withIntSet' ('fromIntSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s
+-- 'withIntSet' ('fromIntSet' ...) $ \\(_ :: 'Proxy' s) -> doSomethingWith \@s
 -- @
 withIntSet
   :: forall r. SomeIntSet -> (forall s. KnownIntSet s => Proxy s -> r) -> r
diff --git a/src/Data/Map/Common/Refined.hs b/src/Data/Map/Common/Refined.hs
--- a/src/Data/Map/Common/Refined.hs
+++ b/src/Data/Map/Common/Refined.hs
@@ -16,13 +16,19 @@
 import qualified Data.Map as Map
 import           Data.Proxy
 import           Data.Reflection
+import qualified Data.Set as Set
 import           Data.Traversable.WithIndex
 import           Data.Type.Coercion
 import           Data.Type.Equality ((:~:)(..))
+import           Prelude hiding (zipWith)
 import           Refined
 import           Refined.Unsafe
 import           Unsafe.Coerce
 
+#if MIN_VERSION_containers(0, 6, 3)
+import           Data.Bifoldable
+#endif
+
 #if MIN_VERSION_containers(0, 6, 2)
 #elif MIN_VERSION_containers(0, 5, 8)
 import           Data.Functor.Const (Const(..))
@@ -33,7 +39,11 @@
 import qualified Data.Map.Strict as MapStrict
 #endif
 
+#if MIN_VERSION_containers(0, 5, 9) || MIN_VERSION_hashable(1, 4, 0)
+import           Data.Functor.Classes
+#endif
 
+
 -- | A wrapper around a regular 'Data.Map.Map' with a type parameter @s@
 -- identifying the set of keys present in the map.
 --
@@ -50,6 +60,12 @@
 #if MIN_VERSION_hashable(1, 3, 4)
   deriving newtype (Hashable.Hashable)
 #endif
+#if MIN_VERSION_containers(0, 6, 3)
+  deriving newtype (Bifoldable)
+#endif
+#if MIN_VERSION_containers(0, 5, 9) || MIN_VERSION_hashable(1, 4, 0)
+  deriving newtype (Eq1, Eq2, Ord1, Ord2, Show1, Show2)
+#endif
   deriving stock (Traversable)
 type role Map nominal nominal representational
 
@@ -94,7 +110,7 @@
 -- parameter @s@), e.g.:
 --
 -- @
--- 'withMap' ('fromMap' ...) $ \(m :: 'Map' s k a) -> doSomethingWith \@s
+-- 'withMap' ('fromMap' ...) $ \\(m :: 'Map' s k a) -> doSomethingWith \@s
 -- @
 withMap :: forall k a r. SomeMap k a -> (forall s. Map s k a -> r) -> r
 withMap (SomeMap m) k = k m
@@ -103,6 +119,14 @@
 fromMap :: forall k a. Map.Map k a -> SomeMap k a
 fromMap m = SomeMap (Map m)
 
+-- | Given a set of keys @s@ known ahead of time, verify whether a regular
+-- 'Data.Map.Map' has exactly that set of keys.
+verifyMap
+  :: forall s k a. (Eq k, KnownSet s k) => Map.Map k a -> Maybe (Map s k a)
+verifyMap m
+  | Map.keys m == Set.toList (reflect $ Proxy @s) = Just (Map m)
+  | otherwise = Nothing
+
 -- | An existential wrapper for a 'Map' with an as-yet-unknown set of keys,
 -- together with a proof of some fact @p@ about the set. Pattern matching on it
 -- gives you a way to refer to the set (the parameter @s@). Functions that
@@ -236,21 +260,33 @@
 
 -- | Given two maps proven to have the same keys, for each key apply the
 -- function to the associated values, to obtain a new map with the same keys.
-zipWithKey
+zipWith
   :: forall s k a b c. Ord k
-  => (Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c
-zipWithKey f (Map m1) (Map m2) = Map
-  $ Map.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)
+  => (a -> b -> c) -> Map s k a -> Map s k b -> Map s k c
+zipWith f (Map m1) (Map m2) = Map
+  $ Map.mergeWithKey (\_ x y -> Just $ f x y)
     (\m -> if Map.null m
       then Map.empty
-      else error "zipWithKey: bug: Data.Map.Refined has been subverted")
+      else error "zipWith: bug: Data.Map.Refined has been subverted")
     (\m -> if Map.null m
       then Map.empty
-      else error "zipWithKey: bug: Data.Map.Refined has been subverted")
+      else error "zipWith: bug: Data.Map.Refined has been subverted")
     --  ^ Work around https://github.com/haskell/containers/issues/979
     m1
     m2
 
+-- | Return the union of two maps. For keys that exist in both maps, the value
+-- is taken from the first map.
+--
+-- @
+-- 'union' = unionWith 'const'
+-- @
+union
+  :: forall s t k a. Ord k
+  => Map s k a -> Map t k a -> SomeMapWith (UnionProof 'Regular s t) k a
+union (Map m1) (Map m2) = SomeMapWith (Map $ Map.union m1 m2)
+  $ UnionProof unsafeSubset unsafeSubsetWith2
+
 -- | Remove the keys that appear in the second map from the first map.
 difference
   :: forall s t k a b. Ord k
@@ -258,6 +294,20 @@
 difference (Map m1) (Map m2) = SomeMapWith (Map $ Map.difference m1 m2)
   $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset
 
+-- | Return the intersection of two maps, taking values from the first map.
+--
+-- @
+-- 'intersection' = intersectionWith 'const'
+-- @
+intersection
+  :: forall s t k a b. Ord k
+  => Map s k a
+  -> Map t k b
+  -> SomeMapWith (IntersectionProof 'Regular s t) k a
+intersection (Map m1) (Map m2)
+  = SomeMapWith (Map $ Map.intersection m1 m2)
+    $ IntersectionProof unsafeSubset unsafeSubsetWith2
+
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, that are proven to be in the map. The set of keys remains the same.
 mapWithKey :: forall s k a b. (Key s k -> a -> b) -> Map s k a -> Map s k b
@@ -314,6 +364,29 @@
 toDescList :: forall s k a. Map s k a -> [(Key s k, a)]
 toDescList = gcoerceWith (unsafeCastKey @s @k) $ coerce $ Map.toDescList @k @a
 
+-- | Retain only the values that satisfy the predicate, returning a potentially
+-- smaller map.
+filter
+  :: forall s k a. (a -> Bool)
+  -> Map s k a
+  -> SomeMapWith (SupersetProof 'Regular s) k a
+filter p (Map m) = SomeMapWith (Map $ Map.filter p m)
+  $ SupersetProof unsafeSubset
+
+-- | Retain only the keys that satisfy the predicate, returning a potentially
+-- smaller map.
+filterKeys
+  :: forall s k a. (Key s k -> Bool)
+  -> Map s k a
+  -> SomeMapWith (SupersetProof 'Regular s) k a
+filterKeys p (Map m) = SomeMapWith
+#if MIN_VERSION_containers(0, 8, 0)
+  (Map $ Map.filterKeys (p . unsafeKey) m)
+#else
+  (Map $ Map.filterWithKey (\k _ -> p (unsafeKey k)) m)
+#endif
+  $ SupersetProof unsafeSubset
+
 -- | Retain only the key-value pairs that satisfy the predicate, returning a
 -- potentially smaller map.
 filterWithKey
@@ -348,6 +421,22 @@
 #endif
   $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset
 
+-- | Partition a map into two disjoint submaps: those whose values satisfy the
+-- predicate, and those whose don't.
+partition
+  :: forall s k a. Ord k -- TODO: this is only used in the proof
+  => (a -> Bool)
+  -> Map s k a
+  -> Some2MapWith (PartitionProof 'Regular s k) k a a
+partition p (Map m) = case Map.partition p m of
+  (m1, m2) -> Some2MapWith (Map m1) (Map m2) $ PartitionProof
+    do \k -> case Map.lookup (unrefine k) m of
+        Nothing -> error "partition: bug: Data.Map.Refined has been subverted"
+        Just x -> if p x
+          then Left $ unsafeKey $ unrefine k
+          else Right $ unsafeKey $ unrefine k
+    unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g
+
 -- | Partition a map into two disjoint submaps: those whose key-value pairs
 -- satisfy the predicate, and those whose don't.
 partitionWithKey
@@ -365,6 +454,43 @@
           else Right $ unsafeKey $ unrefine k
     unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g
 
+-- | Take the a submap of keys up to a point where the predicate stops holding.
+--
+-- If @p@ is antitone ( \(\forall x y, x < y \implies p(x) \ge p(y)\) ), then
+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is
+-- chosen in an unspecified way.
+takeWhileAntitone
+  :: forall s k a. (Key s k -> Bool)
+  -> Map s k a
+  -> SomeMapWith (SupersetProof 'Regular s) k a
+takeWhileAntitone p (Map m) = SomeMapWith
+#if MIN_VERSION_containers(0, 5, 8)
+  (Map $ Map.takeWhileAntitone (p . unsafeKey) m)
+#else
+  (Map $ Map.fromDistinctAscList
+    $ List.takeWhile (p . unsafeKey . fst) $ Map.toAscList m)
+#endif
+  $ SupersetProof unsafeSubset
+
+-- | Take the a submap of keys starting from a point where the predicate stops
+-- holding.
+--
+-- If @p@ is antitone ( \(\forall x y, x < y \implies p(x) \ge p(y)\) ), then
+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is
+-- chosen in an unspecified way.
+dropWhileAntitone
+  :: forall s k a. (Key s k -> Bool)
+  -> Map s k a
+  -> SomeMapWith (SupersetProof 'Regular s) k a
+dropWhileAntitone p (Map m) = SomeMapWith
+#if MIN_VERSION_containers(0, 5, 8)
+  (Map $ Map.dropWhileAntitone (p . unsafeKey) m)
+#else
+  (Map $ Map.fromDistinctAscList
+    $ List.dropWhile (p . unsafeKey . fst) $ Map.toAscList m)
+#endif
+  $ SupersetProof unsafeSubset
+
 -- | Divide a map into two disjoint submaps at a point where the predicate on
 -- the keys stops holding.
 --
@@ -437,15 +563,15 @@
 castKey = castRefined
 
 -- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps
--- can be interconverted too. For example, 'zipWithKey' can be implemented via
--- 'Data.Map.Refined.intersectionWithKey' by proving that the set of keys
--- remains unchanged:
+-- can be interconverted too. For example, 'Data.Map.Refined.zipWithKey' can be
+-- implemented via 'Data.Map.Refined.intersectionWithKey' by proving that the
+-- set of keys remains unchanged:
 --
 -- @
--- 'zipWithKey'
+-- 'Data.Map.Refined.zipWithKey'
 --   :: forall s k a b c. 'Ord' k
 --   => ('Key' s k -> a -> b -> c) -> 'Map' s k a -> 'Map' s k b -> 'Map' s k c
--- 'zipWithKey' f m1 m2
+-- 'Data.Map.Refined.zipWithKey' f m1 m2
 --   | v'SomeMapWith' @r m proof <- 'Data.Map.Refined.intersectionWithKey' (f . 'andLeft') m1 m2
 --   , v'IntersectionProof' p1 p2 <- proof
 --   , ( v'Coercion' :: t'Coercion' ('Map' r k c) ('Map' s k c))
@@ -470,10 +596,10 @@
   itraverse = traverseWithKey
 
 -- | Similar to the instance for functions -- zip corresponding keys. To use
--- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWithKey'.
+-- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWith'.
 instance (Ord k, KnownSet s k) => Applicative (Map s k) where
   pure x = fromSet \_ -> x
-  (<*>) = zipWithKey (const id)
+  (<*>) = zipWith id
 
 -- | @'bind' m f@ is a map that for each key @k :: 'Key' s k@, contains the
 -- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.
@@ -493,7 +619,7 @@
 
 -- | Append the values at the corresponding keys
 instance (Ord k, Semigroup a) => Semigroup (Map s k a) where
-  (<>) = zipWithKey (const (<>))
+  (<>) = zipWith (<>)
 
 instance (Ord k, KnownSet s k, Monoid a) => Monoid (Map s k a) where
   mempty = fromSet \_ -> mempty
diff --git a/src/Data/Map/Refined.hs b/src/Data/Map/Refined.hs
--- a/src/Data/Map/Refined.hs
+++ b/src/Data/Map/Refined.hs
@@ -43,18 +43,26 @@
   , SingletonProof(..)
   , fromSet
   , Common.fromMap
+  , Common.verifyMap
+  , fromTraversable
+  , fromTraversableWith
   , fromTraversableWithKey
   , FromTraversableProof(..)
   -- * Insertion
   , insert
+  , insertWith
+  , insertWithKey
   , InsertProof(..)
   , reinsert
   , insertLookupWithKey
   -- * Deletion/Update
   , Common.delete
+  , adjust'
   , adjust
   , adjustWithKey
+  , update'
   , update
+  , updateWithKey
   , updateLookupWithKey
   -- * Query
   , Common.lookup
@@ -70,21 +78,29 @@
   , Common.disjoint
   , DisjointProof(..)
   -- * Combine
+  , zipWith
   , zipWithKey
   , bind
+  , Common.union
+  , unionWith
   , unionWithKey
   , UnionProof(..)
   , Common.difference
   , DifferenceProof(..)
+  , differenceWith
   , differenceWithKey
   , PartialDifferenceProof(..)
+  , Common.intersection
+  , intersectionWith
   , intersectionWithKey
   , IntersectionProof(..)
   -- * Traversal
+  , map
   , mapWithKey
   , traverseWithKey
   , mapAccumLWithKey
   , mapAccumRWithKey
+  , mapKeys
   , mapKeysWith
   , MapProof(..)
   , backpermuteKeys
@@ -102,12 +118,19 @@
   -- * Filter
   , Common.restrictKeys
   , Common.withoutKeys
+  , Common.filter
+  , Common.filterKeys
   , Common.filterWithKey
+  , Common.partition
   , Common.partitionWithKey
   , PartitionProof(..)
+  , Common.takeWhileAntitone
+  , Common.dropWhileAntitone
   , Common.spanAntitone
   , PartialPartitionProof(..)
+  , mapMaybe
   , mapMaybeWithKey
+  , mapEither
   , mapEitherWithKey
   , Common.splitLookup
   , SplitProof(..)
@@ -131,12 +154,12 @@
 import qualified Data.Map as Map
 import           Data.Map.Common.Refined
   ( Map(..), Key, unsafeCastKey, unsafeKey, SomeMapWith(..), Some2MapWith(..)
-  , fromSet, (!), zipWithKey, mapWithKey, traverseWithKey, bind
+  , fromSet, (!), zipWith, mapWithKey, traverseWithKey, bind
   )
 import qualified Data.Map.Common.Refined as Common
 import           Data.Traversable
 import           Data.Type.Coercion
-import           Prelude hiding (lookup, null)
+import           Prelude hiding (lookup, map, null, zipWith)
 import           Refined
 import           Refined.Unsafe
 
@@ -147,7 +170,41 @@
 singleton k v = SomeMapWith (Map $ Map.singleton k v)
   $ SingletonProof (unsafeKey k)
 
--- | Create a map from an arbitrary traversable of key-value pairs.
+-- | Create a map from an arbitrary traversable of key-value pairs. If a key is
+-- repeated, the retained value is the last one in traversal order. If you're
+-- looking for @fromList@, this is the function you want.
+fromTraversable
+  :: forall t k a. (Traversable t, Ord k)
+  => t (k, a) -> SomeMapWith (FromTraversableProof 'Regular t k) k a
+fromTraversable xs = SomeMapWith (Map m) $ FromTraversableProof proof
+  where
+    (m, proof) = mapAccumL
+      (\s (k, v) -> let !s' = Map.insert k v s in (s', unsafeKey k))
+      Map.empty
+      xs
+
+-- | Create a map from an arbitrary traversable of key-value pairs, with a
+-- function for combining values for repeated keys. The function is called as if
+-- by 'foldl1', but flipped:
+--
+-- @
+-- 'fromTraversableWith' f [(k, x1), (k, x2), (k, x3)]
+--   = 'singleton' k (f x3 (f x2 x1))
+-- @
+fromTraversableWith
+  :: forall t k a. (Traversable t, Ord k)
+  => (a -> a -> a)
+  -> t (k, a)
+  -> SomeMapWith (FromTraversableProof 'Regular t k) k a
+fromTraversableWith f xs = SomeMapWith (Map m) $ FromTraversableProof proof
+  where
+    (m, proof) = mapAccumL
+      (\s (k, v) -> let !s' = Map.insertWith f k v s in (s', unsafeKey k))
+      Map.empty
+      xs
+
+-- | Create a map from an arbitrary traversable of key-value pairs. Like
+-- 'fromTraversableWith', but the combining function has access to the key.
 fromTraversableWithKey
   :: forall t k a. (Traversable t, Ord k)
   => (k -> a -> a -> a)
@@ -169,8 +226,40 @@
 insert k v (Map m) = SomeMapWith (Map $ Map.insert k v m)
   $ InsertProof (unsafeKey k) unsafeSubset
 
+-- | Insert a key-value pair into the map to obtain a potentially larger map,
+-- guaranteed to contain the given key. If the key was already present, the
+-- supplied function is used to combine the new value with the old (in that
+-- order).
+insertWith
+  :: forall s k a. Ord k
+  => (a -> a -> a)
+  -> k
+  -> a
+  -> Map s k a
+  -> SomeMapWith (InsertProof 'Regular k s) k a
+insertWith f k v (Map m) = SomeMapWith (Map $ Map.insertWith f k v m)
+  $ InsertProof (unsafeKey k) unsafeSubset
+
+-- | Insert a key-value pair into the map to obtain a potentially larger map,
+-- guaranteed to contain the given key. Like 'insertWith', but the combining
+-- function has access to the key, which is guaranteed to be in the old map.
+insertWithKey
+  :: forall s k a. Ord k
+  => (Key s k -> a -> a -> a)
+  -> k
+  -> a
+  -> Map s k a
+  -> SomeMapWith (InsertProof 'Regular k s) k a
+insertWithKey f k v (Map m) = SomeMapWith
+  (Map $ Map.insertWithKey (f . unsafeKey) k v m)
+  $ InsertProof (unsafeKey k) unsafeSubset
+
 -- | Overwrite a key-value pair that is known to already be in the map. The set
 -- of keys remains the same.
+--
+-- @
+-- 'reinsert' k v = 'adjust (const v) k'
+-- @
 reinsert
   :: forall s k a. Ord k
   => Key s k -> a -> Map s k a -> Map s k a
@@ -191,10 +280,15 @@
     (v', !m') -> ((unsafeKey k,) <$> v',)
       $ SomeMapWith (Map m') $ InsertProof (unsafeKey k) unsafeSubset
 
+-- | If the given key is in the map, update the value at that key using the
+-- given function. In any case, the set of keys remains the same.
+adjust' :: forall s k a. Ord k => (a -> a) -> k -> Map s k a -> Map s k a
+adjust' = coerce $ Map.adjust @k @a
+
 -- | Update the value at a specific key known the be in the map using the given
 -- function. The set of keys remains the same.
 adjust :: forall s k a. Ord k => (a -> a) -> Key s k -> Map s k a -> Map s k a
-adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ Map.adjust @k @a
+adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ adjust' @s @k @a
 
 -- | If the given key is in the map, update the associated value using the given
 -- function with a proof that the key was in the map; otherwise return the map
@@ -204,6 +298,17 @@
 adjustWithKey = gcoerceWith (unsafeCastKey @s @k) $ coerce
   $ Map.adjustWithKey @k @a
 
+-- | If a key is present in the map, update its value or delete it using the
+-- given function, returning a potentially smaller map.
+update'
+  :: forall s k a. Ord k
+  => (a -> Maybe a)
+  -> k
+  -> Map s k a
+  -> SomeMapWith (SupersetProof 'Regular s) k a
+update' f k (Map m) = SomeMapWith (Map $ Map.update f k m)
+  $ SupersetProof unsafeSubset
+
 -- | Update or delete a key known to be in the map using the given function,
 -- returning a potentially smaller map.
 update
@@ -212,7 +317,19 @@
   -> Key s k
   -> Map s k a
   -> SomeMapWith (SupersetProof 'Regular s) k a
-update f k (Map m) = SomeMapWith (Map $ Map.update f (unrefine k) m)
+update = gcoerceWith (unsafeCastKey @s @k) $ coerce $ update' @s @k @a
+
+-- | If a key is present in the map, update its value or delete it using the
+-- given function with a proof that the key was in the map, returning a
+-- potentially smaller map.
+updateWithKey
+  :: forall s k a. Ord k
+  => (Key s k -> a -> Maybe a)
+  -> k
+  -> Map s k a
+  -> SomeMapWith (SupersetProof 'Regular s) k a
+updateWithKey f k (Map m) = SomeMapWith
+  (Map $ Map.updateWithKey (f . unsafeKey) k m)
   $ SupersetProof unsafeSubset
 
 -- | If the given key is in the map, update or delete it using the given
@@ -230,8 +347,36 @@
     (v', !m') -> ((unsafeKey k,) <$> v',)
       $ SomeMapWith (Map m') $ SupersetProof unsafeSubset
 
+-- | Given two maps proven to have the same keys, for each key apply the
+-- function to the associated values, to obtain a new map with the same keys.
+zipWithKey
+  :: forall s k a b c. Ord k
+  => (Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c
+zipWithKey f (Map m1) (Map m2) = Map
+  $ Map.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)
+    (\m -> if Map.null m
+      then Map.empty
+      else error "zipWithKey: bug: Data.Map.Refined has been subverted")
+    (\m -> if Map.null m
+      then Map.empty
+      else error "zipWithKey: bug: Data.Map.Refined has been subverted")
+    --  ^ Work around https://github.com/haskell/containers/issues/979
+    m1
+    m2
+
 -- | Return the union of two maps, with a given combining function for keys that
 -- exist in both maps simultaneously.
+unionWith
+  :: forall s t k a. Ord k
+  => (a -> a -> a)
+  -> Map s k a
+  -> Map t k a
+  -> SomeMapWith (UnionProof 'Regular s t) k a
+unionWith f (Map m1) (Map m2) = SomeMapWith (Map $ Map.unionWith f m1 m2)
+  $ UnionProof unsafeSubset unsafeSubsetWith2
+
+-- | Return the union of two maps, with a given combining function for keys that
+-- exist in both maps simultaneously.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@
 -- respectively.
@@ -245,8 +390,20 @@
   = SomeMapWith (Map $ Map.unionWithKey (f . reallyUnsafeRefine) m1 m2)
     $ UnionProof unsafeSubset unsafeSubsetWith2
 
--- | For keys that appear in both maps, the given function decides whether the
--- key is removed from the first map.
+-- | Return the first map, but for keys that appear in both maps, the given
+-- function decides whether the key is removed.
+differenceWith
+  :: forall s t k a b. Ord k
+  => (a -> b -> Maybe a)
+  -> Map s k a
+  -> Map t k b
+  -> SomeMapWith (PartialDifferenceProof 'Regular s t) k a
+differenceWith f (Map m1) (Map m2)
+  = SomeMapWith (Map $ Map.differenceWith f m1 m2)
+    $ PartialDifferenceProof unsafeSubset unsafeSubset
+
+-- | Return the first map, but for keys that appear in both maps, the given
+-- function decides whether the key is removed.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@
 -- respectively.
@@ -261,6 +418,17 @@
     $ PartialDifferenceProof unsafeSubset unsafeSubset
 
 -- | Return the intersection of two maps with the given combining function.
+intersectionWith
+  :: forall s t k a b c. Ord k
+  => (a -> b -> c)
+  -> Map s k a
+  -> Map t k b
+  -> SomeMapWith (IntersectionProof 'Regular s t) k c
+intersectionWith f (Map m1) (Map m2)
+  = SomeMapWith (Map $ Map.intersectionWith f m1 m2)
+    $ IntersectionProof unsafeSubset unsafeSubsetWith2
+
+-- | Return the intersection of two maps with the given combining function.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@
 -- respectively.
@@ -274,6 +442,10 @@
   = SomeMapWith (Map $ Map.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)
     $ IntersectionProof unsafeSubset unsafeSubsetWith2
 
+-- | Apply a function to all values in a map. The set of keys remains the same.
+map :: forall s k a b. (a -> b) -> Map s k a -> Map s k b
+map = coerce $ Map.map @a @b @k
+
 -- | Thread an accumularing argument through the map in ascending order of keys.
 mapAccumLWithKey
   :: forall s k a b c. (a -> Key s k -> b -> (a, c))
@@ -293,6 +465,26 @@
 mapAccumRWithKey = gcoerceWith (unsafeCastKey @s @k) $ coerce
   $ Map.mapAccumRWithKey @a @k @b @c
 
+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results
+-- into a new map. For keys that were mapped to the same new key, the value
+-- corresponding to the greatest of the original keys is retained.
+mapKeys
+  :: forall s k1 k2 a. Ord k2
+  => (Key s k1 -> k2)
+  -> Map s k1 a
+  -> SomeMapWith (MapProof 'Regular s k1 k2) k2 a
+mapKeys g (Map m)
+  = SomeMapWith (Map $ Map.mapKeys (g . unsafeKey) m)
+    $ MapProof (unsafeKey . g) \k2 -> case Map.lookup (unrefine k2) backMap of
+      Nothing -> error "mapKeys: bug: Data.Map.Refined has been subverted"
+      Just k1 -> k1
+  where
+    ~backMap = Map.fromList
+      [ (k2, unsafeKey k1)
+      | k1 <- Map.keys m
+      , let !k2 = g $ unsafeKey k1
+      ]
+
 -- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the
 -- results into a new map. For keys that were mapped to the same new key, @c@
 -- acts as the combining function for corresponding values.
@@ -314,6 +506,15 @@
       , let !k2 = g $ unsafeKey k1
       ]
 
+-- | Apply a function to all values in a map and collect only the 'Just'
+-- results, returning a potentially smaller map.
+mapMaybe
+  :: forall s k a b. (a -> Maybe b)
+  -> Map s k a
+  -> SomeMapWith (SupersetProof 'Regular s) k b
+mapMaybe f (Map m) = SomeMapWith (Map $ Map.mapMaybe f m)
+  $ SupersetProof unsafeSubset
+
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, and collect only the 'Just' results, returning a potentially smaller
 -- map.
@@ -324,6 +525,23 @@
 mapMaybeWithKey f (Map m)
   = SomeMapWith (Map $ Map.mapMaybeWithKey (f . unsafeKey) m)
     $ SupersetProof unsafeSubset
+
+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'
+-- results into separate (disjoint) maps.
+mapEither
+  :: forall s k a b c. Ord k -- TODO: this is only used in the proof
+  => (a -> Either b c)
+  -> Map s k a
+  -> Some2MapWith (PartitionProof 'Regular s k) k b c
+mapEither p (Map m) = case Map.mapEither p m of
+  (m1, m2) -> Some2MapWith (Map m1) (Map m2) $ PartitionProof
+    do \k -> case Map.lookup (unrefine k) m of
+        Nothing -> error
+          "mapEither: bug: Data.Map.Refined has been subverted"
+        Just x -> case p x of
+          Left _ -> Left $ unsafeKey $ unrefine k
+          Right _ -> Right $ unsafeKey $ unrefine k
+    unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g
 
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, and collect the 'Left' and 'Right' results into separate (disjoint)
diff --git a/src/Data/Map/Strict/Refined.hs b/src/Data/Map/Strict/Refined.hs
--- a/src/Data/Map/Strict/Refined.hs
+++ b/src/Data/Map/Strict/Refined.hs
@@ -43,18 +43,26 @@
   , SingletonProof(..)
   , fromSet
   , Common.fromMap
+  , Common.verifyMap
+  , fromTraversable
+  , fromTraversableWith
   , fromTraversableWithKey
   , FromTraversableProof(..)
   -- * Insertion
   , insert
+  , insertWith
+  , insertWithKey
   , InsertProof(..)
   , reinsert
   , insertLookupWithKey
   -- * Deletion/Update
   , Common.delete
+  , adjust'
   , adjust
   , adjustWithKey
+  , update'
   , update
+  , updateWithKey
   , updateLookupWithKey
   -- * Query
   , Common.lookup
@@ -72,19 +80,26 @@
   -- * Combine
   , zipWithKey
   , bind
+  , Common.union
+  , unionWith
   , unionWithKey
   , UnionProof(..)
   , Common.difference
   , DifferenceProof(..)
+  , differenceWith
   , differenceWithKey
   , PartialDifferenceProof(..)
+  , Common.intersection
+  , intersectionWith
   , intersectionWithKey
   , IntersectionProof(..)
   -- * Traversal
+  , map
   , mapWithKey
   , traverseWithKey
   , mapAccumLWithKey
   , mapAccumRWithKey
+  , mapKeys
   , mapKeysWith
   , MapProof(..)
   , backpermuteKeys
@@ -102,12 +117,19 @@
   -- * Filter
   , Common.restrictKeys
   , Common.withoutKeys
+  , Common.filter
+  , Common.filterKeys
   , Common.filterWithKey
+  , Common.partition
   , Common.partitionWithKey
   , PartitionProof(..)
+  , Common.takeWhileAntitone
+  , Common.dropWhileAntitone
   , Common.spanAntitone
   , PartialPartitionProof(..)
+  , mapMaybe
   , mapMaybeWithKey
+  , mapEither
   , mapEitherWithKey
   , Common.splitLookup
   , SplitProof(..)
@@ -138,7 +160,7 @@
 import           Data.Reflection
 import           Data.Traversable
 import           Data.Type.Coercion
-import           Prelude hiding (lookup, null)
+import           Prelude hiding (lookup, map, null)
 import           Refined
 import           Refined.Unsafe
 
@@ -154,7 +176,41 @@
 fromSet :: forall s k a. KnownSet s k => (Key s k -> a) -> Map s k a
 fromSet f = Map $ Map.fromSet (f . unsafeKey) (reflect $ Proxy @s)
 
--- | Create a map from an arbitrary traversable of key-value pairs.
+-- | Create a map from an arbitrary traversable of key-value pairs. If a key is
+-- repeated, the retained value is the last one in traversal order. If you're
+-- looking for @fromList@, this is the function you want.
+fromTraversable
+  :: forall t k a. (Traversable t, Ord k)
+  => t (k, a) -> SomeMapWith (FromTraversableProof 'Regular t k) k a
+fromTraversable xs = SomeMapWith (Map m) $ FromTraversableProof proof
+  where
+    (m, proof) = mapAccumL
+      (\s (k, v) -> let !s' = Map.insert k v s in (s', unsafeKey k))
+      Map.empty
+      xs
+
+-- | Create a map from an arbitrary traversable of key-value pairs, with a
+-- function for combining values for repeated keys. The function is called as if
+-- by 'foldl1', but flipped:
+--
+-- @
+-- 'fromTraversableWith' f [(k, x1), (k, x2), (k, x3)]
+--   = 'singleton' k (f x3 (f x2 x1))
+-- @
+fromTraversableWith
+  :: forall t k a. (Traversable t, Ord k)
+  => (a -> a -> a)
+  -> t (k, a)
+  -> SomeMapWith (FromTraversableProof 'Regular t k) k a
+fromTraversableWith f xs = SomeMapWith (Map m) $ FromTraversableProof proof
+  where
+    (m, proof) = mapAccumL
+      (\s (k, v) -> let !s' = Map.insertWith f k v s in (s', unsafeKey k))
+      Map.empty
+      xs
+
+-- | Create a map from an arbitrary traversable of key-value pairs. Like
+-- 'fromTraversableWith', but the combining function has access to the key.
 fromTraversableWithKey
   :: forall t k a. (Traversable t, Ord k)
   => (k -> a -> a -> a)
@@ -176,8 +232,40 @@
 insert k v (Map m) = SomeMapWith (Map $ Map.insert k v m)
   $ InsertProof (unsafeKey k) unsafeSubset
 
+-- | Insert a key-value pair into the map to obtain a potentially larger map,
+-- guaranteed to contain the given key. If the key was already present, the
+-- supplied function is used to combine the new value with the old (in that
+-- order).
+insertWith
+  :: forall s k a. Ord k
+  => (a -> a -> a)
+  -> k
+  -> a
+  -> Map s k a
+  -> SomeMapWith (InsertProof 'Regular k s) k a
+insertWith f k v (Map m) = SomeMapWith (Map $ Map.insertWith f k v m)
+  $ InsertProof (unsafeKey k) unsafeSubset
+
+-- | Insert a key-value pair into the map to obtain a potentially larger map,
+-- guaranteed to contain the given key. Like 'insertWith', but the combining
+-- function has access to the key, which is guaranteed to be in the old map.
+insertWithKey
+  :: forall s k a. Ord k
+  => (Key s k -> a -> a -> a)
+  -> k
+  -> a
+  -> Map s k a
+  -> SomeMapWith (InsertProof 'Regular k s) k a
+insertWithKey f k v (Map m) = SomeMapWith
+  (Map $ Map.insertWithKey (f . unsafeKey) k v m)
+  $ InsertProof (unsafeKey k) unsafeSubset
+
 -- | Overwrite a key-value pair that is known to already be in the map. The set
 -- of keys remains the same.
+--
+-- @
+-- 'reinsert' k v = 'adjust (const v) k'
+-- @
 reinsert
   :: forall s k a. Ord k
   => Key s k -> a -> Map s k a -> Map s k a
@@ -198,10 +286,15 @@
     (v', !m') -> ((unsafeKey k,) <$> v',)
       $ SomeMapWith (Map m') $ InsertProof (unsafeKey k) unsafeSubset
 
+-- | If the given key is in the map, update the value at that key using the
+-- given function. In any case, the set of keys remains the same.
+adjust' :: forall s k a. Ord k => (a -> a) -> k -> Map s k a -> Map s k a
+adjust' = coerce $ Map.adjust @k @a
+
 -- | Update the value at a specific key known the be in the map using the given
 -- function. The set of keys remains the same.
 adjust :: forall s k a. Ord k => (a -> a) -> Key s k -> Map s k a -> Map s k a
-adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ Map.adjust @k @a
+adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ adjust' @s @k @a
 
 -- | If the given key is in the map, update the associated value using the given
 -- function with a proof that the key was in the map; otherwise return the map
@@ -211,6 +304,17 @@
 adjustWithKey = gcoerceWith (unsafeCastKey @s @k) $ coerce
   $ Map.adjustWithKey @k @a
 
+-- | If a key is present in the map, update its value or delete it using the
+-- given function, returning a potentially smaller map.
+update'
+  :: forall s k a. Ord k
+  => (a -> Maybe a)
+  -> k
+  -> Map s k a
+  -> SomeMapWith (SupersetProof 'Regular s) k a
+update' f k (Map m) = SomeMapWith (Map $ Map.update f k m)
+  $ SupersetProof unsafeSubset
+
 -- | Update or delete a key known to be in the map using the given function,
 -- returning a potentially smaller map.
 update
@@ -219,7 +323,19 @@
   -> Key s k
   -> Map s k a
   -> SomeMapWith (SupersetProof 'Regular s) k a
-update f k (Map m) = SomeMapWith (Map $ Map.update f (unrefine k) m)
+update = gcoerceWith (unsafeCastKey @s @k) $ coerce $ update' @s @k @a
+
+-- | If a key is present in the map, update its value or delete it using the
+-- given function with a proof that the key was in the map, returning a
+-- potentially smaller map.
+updateWithKey
+  :: forall s k a. Ord k
+  => (Key s k -> a -> Maybe a)
+  -> k
+  -> Map s k a
+  -> SomeMapWith (SupersetProof 'Regular s) k a
+updateWithKey f k (Map m) = SomeMapWith
+  (Map $ Map.updateWithKey (f . unsafeKey) k m)
   $ SupersetProof unsafeSubset
 
 -- | If the given key is in the map, update or delete it using the given
@@ -256,6 +372,17 @@
 
 -- | Return the union of two maps, with a given combining function for keys that
 -- exist in both maps simultaneously.
+unionWith
+  :: forall s t k a. Ord k
+  => (a -> a -> a)
+  -> Map s k a
+  -> Map t k a
+  -> SomeMapWith (UnionProof 'Regular s t) k a
+unionWith f (Map m1) (Map m2) = SomeMapWith (Map $ Map.unionWith f m1 m2)
+  $ UnionProof unsafeSubset unsafeSubsetWith2
+
+-- | Return the union of two maps, with a given combining function for keys that
+-- exist in both maps simultaneously.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@
 -- respectively.
@@ -269,8 +396,20 @@
   = SomeMapWith (Map $ Map.unionWithKey (f . reallyUnsafeRefine) m1 m2)
     $ UnionProof unsafeSubset unsafeSubsetWith2
 
--- | For keys that appear in both maps, the given function decides whether the
--- key is removed from the first map.
+-- | Return the first map, but for keys that appear in both maps, the given
+-- function decides whether the key is removed.
+differenceWith
+  :: forall s t k a b. Ord k
+  => (a -> b -> Maybe a)
+  -> Map s k a
+  -> Map t k b
+  -> SomeMapWith (PartialDifferenceProof 'Regular s t) k a
+differenceWith f (Map m1) (Map m2)
+  = SomeMapWith (Map $ Map.differenceWith f m1 m2)
+    $ PartialDifferenceProof unsafeSubset unsafeSubset
+
+-- | Return the first map, but for keys that appear in both maps, the given
+-- function decides whether the key is removed.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@
 -- respectively.
@@ -285,6 +424,17 @@
     $ PartialDifferenceProof unsafeSubset unsafeSubset
 
 -- | Return the intersection of two maps with the given combining function.
+intersectionWith
+  :: forall s t k a b c. Ord k
+  => (a -> b -> c)
+  -> Map s k a
+  -> Map t k b
+  -> SomeMapWith (IntersectionProof 'Regular s t) k c
+intersectionWith f (Map m1) (Map m2)
+  = SomeMapWith (Map $ Map.intersectionWith f m1 m2)
+    $ IntersectionProof unsafeSubset unsafeSubsetWith2
+
+-- | Return the intersection of two maps with the given combining function.
 --
 -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@
 -- respectively.
@@ -298,6 +448,10 @@
   = SomeMapWith (Map $ Map.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)
     $ IntersectionProof unsafeSubset unsafeSubsetWith2
 
+-- | Apply a function to all values in a map. The set of keys remains the same.
+map :: forall s k a b. (a -> b) -> Map s k a -> Map s k b
+map = coerce $ Map.map @a @b @k
+
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, that are proven to be in the map. The set of keys remains the same.
 mapWithKey :: forall s k a b. (Key s k -> a -> b) -> Map s k a -> Map s k b
@@ -331,6 +485,27 @@
 mapAccumRWithKey = gcoerceWith (unsafeCastKey @s @k) $ coerce
   $ Map.mapAccumRWithKey @a @k @b @c
 
+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results
+-- into a new map. For keys that were mapped to the same new key, the value
+-- corresponding to the greatest of the original keys is retained.
+mapKeys
+  :: forall s k1 k2 a. Ord k2
+  => (Key s k1 -> k2)
+  -> Map s k1 a
+  -> SomeMapWith (MapProof 'Regular s k1 k2) k2 a
+mapKeys g (Map m)
+  = SomeMapWith (Map $ Map.mapKeys (g . unsafeKey) m)
+    $ MapProof (unsafeKey . g) \k2 -> case Map.lookup (unrefine k2) backMap of
+      Nothing -> error
+        "mapKeys: bug: Data.Map.Strict.Refined has been subverted"
+      Just k1 -> k1
+  where
+    ~backMap = Map.fromList
+      [ (k2, unsafeKey k1)
+      | k1 <- Map.keys m
+      , let !k2 = g $ unsafeKey k1
+      ]
+
 -- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the
 -- results into a new map. For keys that were mapped to the same new key, @c@
 -- acts as the combining function for corresponding values.
@@ -353,6 +528,15 @@
       , let !k2 = g $ unsafeKey k1
       ]
 
+-- | Apply a function to all values in a map and collect only the 'Just'
+-- results, returning a potentially smaller map.
+mapMaybe
+  :: forall s k a b. (a -> Maybe b)
+  -> Map s k a
+  -> SomeMapWith (SupersetProof 'Regular s) k b
+mapMaybe f (Map m) = SomeMapWith (Map $ Map.mapMaybe f m)
+  $ SupersetProof unsafeSubset
+
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, and collect only the 'Just' results, returning a potentially smaller
 -- map.
@@ -363,6 +547,23 @@
 mapMaybeWithKey f (Map m)
   = SomeMapWith (Map $ Map.mapMaybeWithKey (f . unsafeKey) m)
     $ SupersetProof unsafeSubset
+
+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'
+-- results into separate (disjoint) maps.
+mapEither
+  :: forall s k a b c. Ord k -- TODO: this is only used in the proof
+  => (a -> Either b c)
+  -> Map s k a
+  -> Some2MapWith (PartitionProof 'Regular s k) k b c
+mapEither p (Map m) = case Map.mapEither p m of
+  (m1, m2) -> Some2MapWith (Map m1) (Map m2) $ PartitionProof
+    do \k -> case Map.lookup (unrefine k) m of
+        Nothing -> error
+          "mapEither: bug: Data.Map.Strict.Refined has been subverted"
+        Just x -> case p x of
+          Left _ -> Left $ unsafeKey $ unrefine k
+          Right _ -> Right $ unsafeKey $ unrefine k
+    unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g
 
 -- | Apply a function to all values in a map, together with their corresponding
 -- keys, and collect the 'Left' and 'Right' results into separate (disjoint)
diff --git a/src/Data/Set/Refined.hs b/src/Data/Set/Refined.hs
--- a/src/Data/Set/Refined.hs
+++ b/src/Data/Set/Refined.hs
@@ -185,7 +185,7 @@
 -- you a way to refer to the set (the parameter @s@), e.g.:
 --
 -- @
--- 'withSet' ('fromSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s
+-- 'withSet' ('fromSet' ...) $ \\(_ :: 'Proxy' s) -> doSomethingWith \@s
 -- @
 withSet
   :: forall a r. SomeSet a -> (forall s. KnownSet s a => Proxy s -> r) -> r