diff --git a/theories/base.v b/theories/base.v
index 41fb9c5b9b7593c7b6bd6f822c46c98abff10d57..575a0671ffc421b3c0cf5646b1842f46cb2665d7 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -91,6 +91,8 @@ Notation "(, y )" := (λ x, (x,y)) (only parsing) : C_scope.
 Notation "p .1" := (fst p) (at level 10, format "p .1").
 Notation "p .2" := (snd p) (at level 10, format "p .2").
 
+Definition fun_map {A A' B B'} (f : A' -> A) (g : B -> B')
+  (h : A -> B) : A' -> B' := g ∘ h ∘ f.
 Definition prod_map {A A' B B'} (f : A → A') (g : B → B')
   (p : A * B) : A' * B' := (f (p.1), g (p.2)).
 Arguments prod_map {_ _ _ _} _ _ !_ /.