diff --git a/libs/base/Data/DPair.idr b/libs/base/Data/DPair.idr
index 379fb95da..7fde1b2b8 100644
--- a/libs/base/Data/DPair.idr
+++ b/libs/base/Data/DPair.idr
@@ -12,6 +12,10 @@ namespace DPair
   uncurry : {0 p : a -> Type} -> ((x : a) -> p x -> c) -> (x : a ** p x) -> c
   uncurry f s = f s.fst s.snd
 
+  public export
+  bimap : {0 p : a -> Type} -> {0 q : b -> Type} -> (f : a -> b) -> (forall x. p x -> q (f x)) -> (x : a ** p x) -> (y : b ** q y)
+  bimap f g (x ** y) = (f x ** g y)
+
 namespace Exists
 
   ||| A dependent pair in which the first field (witness) should be
@@ -39,6 +43,10 @@ namespace Exists
   uncurry : {0 p : a -> Type} -> ({0 x : a} -> p x -> c) -> Exists {type=a} p -> c
   uncurry f ex = f ex.snd
 
+  public export
+  bimap : (0 f : a -> b) -> (forall x. p x -> q (f x)) -> Exists {type=a} p -> Exists {type=b} q
+  bimap f g (Evidence x y) = Evidence (f x) (g y)
+
 namespace Subset
 
   ||| A dependent pair in which the second field (evidence) should not
@@ -63,3 +71,7 @@ namespace Subset
   public export
   uncurry : {0 p : a -> Type} -> ((x : a) -> (0 _ : p x) -> c) -> Subset a p -> c
   uncurry f s = f s.fst s.snd
+
+  public export
+  bimap : (f : a -> b) -> (0 _ : forall x. p x -> q (f x)) -> Subset a p -> Subset b q
+  bimap f g (Element x y) = Element (f x) (g y)