diff --git a/algebra/cmra.v b/algebra/cmra.v
index 27afdb0be10b5cf255d659319157698a520d76aa..e2a4d8791a47ebb404aa83a28cc7783520532e1c 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -443,7 +443,7 @@ End cmra_monotone.
 
 (** Functors *)
 Structure rFunctor := RFunctor {
-  rFunctor_car : cofeT → cofeT -> cmraT;
+  rFunctor_car : cofeT → cofeT → cmraT;
   rFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
   rFunctor_ne A1 A2 B1 B2 n :
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 8a157856080bf7dc78e9f4aa77a6672ea8dc6f7a..fe969f567b6b8e17e8ad2497d62b0f3122c53a1c 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -340,7 +340,7 @@ Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
 
 (** Functors *)
 Structure cFunctor := CFunctor {
-  cFunctor_car : cofeT → cofeT -> cofeT;
+  cFunctor_car : cofeT → cofeT → cofeT;
   cFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
   cFunctor_ne {A1 A2 B1 B2} n :
diff --git a/prelude/base.v b/prelude/base.v
index ab142229f48a9a4310c5e9f6157f059476936d52..7089551e68e5ee45f7efbb19a0155bd6e24f5f1f 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -91,8 +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 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 {_ _ _ _} _ _ !_ /.