diff --git a/CHANGELOG.md b/CHANGELOG.md
index c8934aea512fb23e6baee70eb1466ab1151bb7d2..a9da76d1e2e592994e3a5f162ec7b67675e341ef 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -88,6 +88,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   `inv N P -∗ ▷ □ (P ↔ Q) -∗ inv N Q` and (similar for `na_inv_iff` and
   `cinv_iff`), following e.g., `inv_alter` and `wp_wand`.
 * Add lemma `is_lock_iff` and show that `is_lock` is contractive.
+* Rename `{o,r,ur}Functor_{ne,id,compose,contractive}` into
+  `{o,r,ur}Functor_map_{ne,id,compose,contractive}`.
+* Add `{o,r,ur}Functor_oFunctor_compose` for composition of functors.
 
 **Changes in heap_lang:**
 
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index ee4d65d20b86764decf7d0de98e076abb687fec6..1071f99732248863931bdd804bcd2f429aaf2580 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -310,20 +310,20 @@ Program Definition agreeRF (F : oFunctor) : rFunctor := {|
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeO_map_ne, oFunctor_ne.
+  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
-  apply (agree_map_ext _)=>y. by rewrite oFunctor_id.
+  apply (agree_map_ext _)=>y. by rewrite oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -agree_map_compose.
-  apply (agree_map_ext _)=>y; apply oFunctor_compose.
+  apply (agree_map_ext _)=>y; apply oFunctor_map_compose.
 Qed.
 
 Instance agreeRF_contractive F :
   oFunctorContractive F → rFunctorContractive (agreeRF F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
-  by apply agreeO_map_ne, oFunctor_contractive.
+  by apply agreeO_map_ne, oFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 90441e3150f2ad191addc3b020075f66059e8427..49467a7703537cae0736836e341a18c01566f53c 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -455,21 +455,21 @@ Program Definition authRF (F : urFunctor) : rFunctor := {|
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authO_map (urFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
-  apply (auth_map_ext _ _)=>y; apply urFunctor_id.
+  apply (auth_map_ext _ _)=>y; apply urFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -auth_map_compose.
-  apply (auth_map_ext _ _)=>y; apply urFunctor_compose.
+  apply (auth_map_ext _ _)=>y; apply urFunctor_map_compose.
 Qed.
 
 Instance authRF_contractive F :
   urFunctorContractive F → rFunctorContractive (authRF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_contractive.
 Qed.
 
 Program Definition authURF (F : urFunctor) : urFunctor := {|
@@ -477,19 +477,19 @@ Program Definition authURF (F : urFunctor) : urFunctor := {|
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authO_map (urFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
-  apply (auth_map_ext _ _)=>y; apply urFunctor_id.
+  apply (auth_map_ext _ _)=>y; apply urFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -auth_map_compose.
-  apply (auth_map_ext _ _)=>y; apply urFunctor_compose.
+  apply (auth_map_ext _ _)=>y; apply urFunctor_map_compose.
 Qed.
 
 Instance authURF_contractive F :
   urFunctorContractive F → urFunctorContractive (authURF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index b0f608cc58b6b1617f985a785ab302e26386ae88..54a984004e7c94a5331b0c97ae5dfe37e9ea4d81 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -779,30 +779,65 @@ Record rFunctor := RFunctor {
   rFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, cmraT;
   rFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
-  rFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
+  rFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     NonExpansive (@rFunctor_map A1 _ A2 _ B1 _ B2 _);
-  rFunctor_id `{!Cofe A, !Cofe B} (x : rFunctor_car A B) :
+  rFunctor_map_id `{!Cofe A, !Cofe B} (x : rFunctor_car A B) :
     rFunctor_map (cid,cid) x ≡ x;
-  rFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
+  rFunctor_map_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
   rFunctor_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
       (fg : (A2 -n> A1) * (B1 -n> B2)) :
     CmraMorphism (rFunctor_map fg)
 }.
-Existing Instances rFunctor_ne rFunctor_mor.
+Existing Instances rFunctor_map_ne rFunctor_mor.
 Instance: Params (@rFunctor_map) 9 := {}.
 
 Delimit Scope rFunctor_scope with RF.
 Bind Scope rFunctor_scope with rFunctor.
 
 Class rFunctorContractive (F : rFunctor) :=
-  rFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+  rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
 
 Definition rFunctor_apply (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
   rFunctor_car F A A.
 
+Program Definition rFunctor_oFunctor_compose (F1 : rFunctor) (F2 : oFunctor)
+  `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} : rFunctor := {|
+  rFunctor_car A _ B _ := rFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ 'fg :=
+    rFunctor_map F1 (oFunctor_map F2 (fg.2,fg.1),oFunctor_map F2 fg)
+|}.
+Next Obligation.
+  intros F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
+  apply rFunctor_map_ne; split; apply oFunctor_map_ne; by split.
+Qed.
+Next Obligation.
+  intros F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(rFunctor_map_id F1 x).
+  apply equiv_dist=> n. apply rFunctor_map_ne.
+  split=> y /=; by rewrite !oFunctor_map_id.
+Qed.
+Next Obligation.
+  intros F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
+  rewrite -rFunctor_map_compose. apply equiv_dist=> n. apply rFunctor_map_ne.
+  split=> y /=; by rewrite !oFunctor_map_compose.
+Qed.
+Instance rFunctor_oFunctor_compose_contractive_1 (F1 : rFunctor) (F2 : oFunctor)
+    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+  rFunctorContractive F1 → rFunctorContractive (rFunctor_oFunctor_compose F1 F2).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
+  f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
+Qed.
+Instance rFunctor_oFunctor_compose_contractive_2 (F1 : rFunctor) (F2 : oFunctor)
+    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+  oFunctorContractive F2 → rFunctorContractive (rFunctor_oFunctor_compose F1 F2).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
+  f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
+Qed.
+
 Program Definition constRF (B : cmraT) : rFunctor :=
   {| rFunctor_car A1 _ A2 _ := B; rFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
 Solve Obligations with done.
@@ -816,30 +851,65 @@ Record urFunctor := URFunctor {
   urFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ucmraT;
   urFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
-  urFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
+  urFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     NonExpansive (@urFunctor_map A1 _ A2 _ B1 _ B2 _);
-  urFunctor_id `{!Cofe A, !Cofe B} (x : urFunctor_car A B) :
+  urFunctor_map_id `{!Cofe A, !Cofe B} (x : urFunctor_car A B) :
     urFunctor_map (cid,cid) x ≡ x;
-  urFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
+  urFunctor_map_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     urFunctor_map (f◎g, g'◎f') x ≡ urFunctor_map (g,g') (urFunctor_map (f,f') x);
   urFunctor_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
       (fg : (A2 -n> A1) * (B1 -n> B2)) :
     CmraMorphism (urFunctor_map fg)
 }.
-Existing Instances urFunctor_ne urFunctor_mor.
+Existing Instances urFunctor_map_ne urFunctor_mor.
 Instance: Params (@urFunctor_map) 9 := {}.
 
 Delimit Scope urFunctor_scope with URF.
 Bind Scope urFunctor_scope with urFunctor.
 
 Class urFunctorContractive (F : urFunctor) :=
-  urFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+  urFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).
 
 Definition urFunctor_apply (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
   urFunctor_car F A A.
 
+Program Definition urFunctor_oFunctor_compose (F1 : urFunctor) (F2 : oFunctor)
+  `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} : urFunctor := {|
+  urFunctor_car A _ B _ := urFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ 'fg :=
+    urFunctor_map F1 (oFunctor_map F2 (fg.2,fg.1),oFunctor_map F2 fg)
+|}.
+Next Obligation.
+  intros F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
+  apply urFunctor_map_ne; split; apply oFunctor_map_ne; by split.
+Qed.
+Next Obligation.
+  intros F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(urFunctor_map_id F1 x).
+  apply equiv_dist=> n. apply urFunctor_map_ne.
+  split=> y /=; by rewrite !oFunctor_map_id.
+Qed.
+Next Obligation.
+  intros F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
+  rewrite -urFunctor_map_compose. apply equiv_dist=> n. apply urFunctor_map_ne.
+  split=> y /=; by rewrite !oFunctor_map_compose.
+Qed.
+Instance urFunctor_oFunctor_compose_contractive_1 (F1 : urFunctor) (F2 : oFunctor)
+    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+  urFunctorContractive F1 → urFunctorContractive (urFunctor_oFunctor_compose F1 F2).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
+  f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
+Qed.
+Instance urFunctor_oFunctor_compose_contractive_2 (F1 : urFunctor) (F2 : oFunctor)
+    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+  oFunctorContractive F2 → urFunctorContractive (urFunctor_oFunctor_compose F1 F2).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
+  f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
+Qed.
+
 Program Definition constURF (B : ucmraT) : urFunctor :=
   {| urFunctor_car A1 _ A2 _ := B; urFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
 Solve Obligations with done.
@@ -1253,12 +1323,12 @@ Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
     prodO_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply rFunctor_ne.
+  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply rFunctor_map_ne.
 Qed.
-Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !rFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !rFunctor_map_id. Qed.
 Next Obligation.
   intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
-  by rewrite !rFunctor_compose.
+  by rewrite !rFunctor_map_compose.
 Qed.
 Notation "F1 * F2" := (prodRF F1%RF F2%RF) : rFunctor_scope.
 
@@ -1267,7 +1337,7 @@ Instance prodRF_contractive F1 F2 :
   rFunctorContractive (prodRF F1 F2).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
-    by apply prodO_map_ne; apply rFunctor_contractive.
+    by apply prodO_map_ne; apply rFunctor_map_contractive.
 Qed.
 
 Program Definition prodURF (F1 F2 : urFunctor) : urFunctor := {|
@@ -1276,12 +1346,12 @@ Program Definition prodURF (F1 F2 : urFunctor) : urFunctor := {|
     prodO_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply urFunctor_ne.
+  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply urFunctor_map_ne.
 Qed.
-Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !urFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !urFunctor_map_id. Qed.
 Next Obligation.
   intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
-  by rewrite !urFunctor_compose.
+  by rewrite !urFunctor_map_compose.
 Qed.
 Notation "F1 * F2" := (prodURF F1%URF F2%URF) : urFunctor_scope.
 
@@ -1290,7 +1360,7 @@ Instance prodURF_contractive F1 F2 :
   urFunctorContractive (prodURF F1 F2).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
-    by apply prodO_map_ne; apply urFunctor_contractive.
+    by apply prodO_map_ne; apply urFunctor_map_contractive.
 Qed.
 
 (** ** CMRA for the option type *)
@@ -1527,21 +1597,21 @@ Program Definition optionRF (F : rFunctor) : rFunctor := {|
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_equiv_ext=>y; apply rFunctor_id.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_map_compose.
 Qed.
 
 Instance optionRF_contractive F :
   rFunctorContractive F → rFunctorContractive (optionRF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
 Qed.
 
 Program Definition optionURF (F : rFunctor) : urFunctor := {|
@@ -1549,21 +1619,21 @@ Program Definition optionURF (F : rFunctor) : urFunctor := {|
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_equiv_ext=>y; apply rFunctor_id.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_map_compose.
 Qed.
 
 Instance optionURF_contractive F :
   rFunctorContractive F → urFunctorContractive (optionURF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
 Qed.
 
 (* Dependently-typed functions over a discrete domain *)
@@ -1650,19 +1720,19 @@ Program Definition discrete_funURF {C} (F : C → urFunctor) : urFunctor := {|
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := discrete_funO_map (λ c, urFunctor_map (F c) fg)
 |}.
 Next Obligation.
-  intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply discrete_funO_map_ne=>?; apply urFunctor_ne.
+  intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply discrete_funO_map_ne=>?; apply urFunctor_map_ne.
 Qed.
 Next Obligation.
   intros C F A ? B ? g; simpl. rewrite -{2}(discrete_fun_map_id g).
-  apply discrete_fun_map_ext=> y; apply urFunctor_id.
+  apply discrete_fun_map_ext=> y; apply urFunctor_map_id.
 Qed.
 Next Obligation.
   intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g. rewrite /=-discrete_fun_map_compose.
-  apply discrete_fun_map_ext=>y; apply urFunctor_compose.
+  apply discrete_fun_map_ext=>y; apply urFunctor_map_compose.
 Qed.
 Instance discrete_funURF_contractive {C} (F : C → urFunctor) :
   (∀ c, urFunctorContractive (F c)) → urFunctorContractive (discrete_funURF F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
-  by apply discrete_funO_map_ne=>c; apply urFunctor_contractive.
+  by apply discrete_funO_map_ne=>c; apply urFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index f64b166540f9ff2986746d2599e09e1f51351546..f5a1900511bf1f0f1070cd9fa319f9ef1e9064a9 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -34,14 +34,15 @@ Arguments g : simpl never.
 Lemma gf {k} (x : A k) : g k (f k x) ≡ x.
 Proof using Fcontr.
   induction k as [|k IH]; simpl in *; [by destruct x|].
-  rewrite -oFunctor_compose -{2}[x]oFunctor_id. by apply (contractive_proper map).
+  rewrite -oFunctor_map_compose -{2}[x]oFunctor_map_id.
+  by apply (contractive_proper map).
 Qed.
 Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) ≡{k}≡ x.
 Proof using Fcontr.
   induction k as [|k IH]; simpl.
-  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
+  - rewrite f_S g_S -{2}[x]oFunctor_map_id -oFunctor_map_compose.
     apply (contractive_0 map).
-  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
+  - rewrite f_S g_S -{2}[x]oFunctor_map_id -oFunctor_map_compose.
     by apply (contractive_S map).
 Qed.
 
@@ -183,7 +184,7 @@ Next Obligation.
   assert (∃ k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
   induction k as [|k IH]; simpl; first done.
   rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia.
-  rewrite f_S -oFunctor_compose.
+  rewrite f_S -oFunctor_map_compose.
   by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
 Qed.
 Definition unfold (X : T) : oFunctor_apply F T := compl (unfold_chain X).
@@ -197,7 +198,7 @@ Program Definition fold (X : oFunctor_apply F T) : T :=
   {| tower_car n := g n (map (embed' n,project n) X) |}.
 Next Obligation.
   intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)).
-  rewrite g_S -oFunctor_compose.
+  rewrite g_S -oFunctor_map_compose.
   apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower].
 Qed.
 Instance fold_ne : NonExpansive fold.
@@ -212,7 +213,7 @@ Proof using Type*.
     { rewrite /unfold (conv_compl n (unfold_chain X)).
       rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
       rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
-      rewrite f_S -!oFunctor_compose; apply (contractive_ne map); split=> Y.
+      rewrite f_S -!oFunctor_map_compose; apply (contractive_ne map); split=> Y.
       + rewrite /embed' /= /embed_coerce.
         destruct (le_lt_dec _ _); simpl; [exfalso; lia|].
         by rewrite (ff_ff _ (eq_refl (S n + (0 + k)))) /= gf.
@@ -222,14 +223,14 @@ Proof using Type*.
     assert (∀ i k (x : A (S i + k)) (H : S i + k = i + S k),
       map (ff i, gg i) x ≡ gg i (coerce H x)) as map_ff_gg.
     { intros i; induction i as [|i IH]; intros k' x H; simpl.
-      { by rewrite coerce_id oFunctor_id. }
-      rewrite oFunctor_compose g_coerce; apply IH. }
+      { by rewrite coerce_id oFunctor_map_id. }
+      rewrite oFunctor_map_compose g_coerce; apply IH. }
     assert (H: S n + k = n + S k) by lia.
     rewrite (map_ff_gg _ _ _ H).
     apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
   - intros X; rewrite equiv_dist=> n /=.
     rewrite /unfold /= (conv_compl' n (unfold_chain (fold X))) /=.
-    rewrite g_S -!oFunctor_compose -{2}[X]oFunctor_id.
+    rewrite g_S -!oFunctor_map_compose -{2}[X]oFunctor_map_id.
     apply (contractive_ne map); split => Y /=.
     + rewrite f_tower. apply dist_S. by rewrite embed_tower.
     + etrans; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 86d121530b3324068869965191cdac31736212d8..477c3f3e51efd780b7ef49b87d6ab729b860a1cd 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -375,15 +375,15 @@ Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := csumO_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
 |}.
 Next Obligation.
-  by intros Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumO_map_ne; try apply rFunctor_ne.
+  by intros Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumO_map_ne; try apply rFunctor_map_ne.
 Qed.
 Next Obligation.
   intros Fa Fb A ? B ? x. rewrite /= -{2}(csum_map_id x).
-  apply csum_map_ext=>y; apply rFunctor_id.
+  apply csum_map_ext=>y; apply rFunctor_map_id.
 Qed.
 Next Obligation.
   intros Fa Fb A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -csum_map_compose.
-  apply csum_map_ext=>y; apply rFunctor_compose.
+  apply csum_map_ext=>y; apply rFunctor_map_compose.
 Qed.
 
 Instance csumRF_contractive Fa Fb :
@@ -391,5 +391,5 @@ Instance csumRF_contractive Fa Fb :
   rFunctorContractive (csumRF Fa Fb).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
-  by apply csumO_map_ne; try apply rFunctor_contractive.
+  by apply csumO_map_ne; try apply rFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index 6467624323e8915259dde9528e4a56be58ad5d90..027517d48d8cf92a6de77a4c98540e729ee89d57 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -154,19 +154,19 @@ Program Definition exclRF (F : oFunctor) : rFunctor := {|
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := exclO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  intros F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_ne.
+  intros F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x; simpl. rewrite -{2}(excl_map_id x).
-  apply excl_map_ext=>y. by rewrite oFunctor_id.
+  apply excl_map_ext=>y. by rewrite oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -excl_map_compose.
-  apply excl_map_ext=>y; apply oFunctor_compose.
+  apply excl_map_ext=>y; apply oFunctor_map_compose.
 Qed.
 
 Instance exclRF_contractive F :
   oFunctorContractive F → rFunctorContractive (exclRF F).
 Proof.
-  intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_contractive.
+  intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index d499dfa7db0c15fe543000009094b351e4ecf2fb..01d97b757819dc562af34bee7ca915f02aa0e4e2 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -628,20 +628,20 @@ Program Definition gmapOF K `{Countable K} (F : oFunctor) : oFunctor := {|
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_ne.
+  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_equiv_ext=>y ??; apply oFunctor_id.
+  apply map_fmap_equiv_ext=>y ??; apply oFunctor_map_id.
 Qed.
 Next Obligation.
   intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_equiv_ext=>y ??; apply oFunctor_compose.
+  apply map_fmap_equiv_ext=>y ??; apply oFunctor_map_compose.
 Qed.
 Instance gmapOF_contractive K `{Countable K} F :
   oFunctorContractive F → oFunctorContractive (gmapOF K F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_map_contractive.
 Qed.
 
 Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
@@ -649,18 +649,18 @@ Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_ne.
+  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_map_ne.
 Qed.
 Next Obligation.
   intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_equiv_ext=>y ??; apply rFunctor_id.
+  apply map_fmap_equiv_ext=>y ??; apply rFunctor_map_id.
 Qed.
 Next Obligation.
   intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_equiv_ext=>y ??; apply rFunctor_compose.
+  apply map_fmap_equiv_ext=>y ??; apply rFunctor_map_compose.
 Qed.
 Instance gmapRF_contractive K `{Countable K} F :
   rFunctorContractive F → urFunctorContractive (gmapURF K F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index b631b236a0c185eaf10096497b01a46fdbb567a5..492ffe0b37e0d15fd97f44796f0174757d19ad7e 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -162,21 +162,21 @@ Program Definition listOF (F : oFunctor) : oFunctor := {|
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_equiv_ext=>y. apply oFunctor_id.
+  apply list_fmap_equiv_ext=>y. apply oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_equiv_ext=>y; apply oFunctor_compose.
+  apply list_fmap_equiv_ext=>y; apply oFunctor_map_compose.
 Qed.
 
 Instance listOF_contractive F :
   oFunctorContractive F → oFunctorContractive (listOF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_contractive.
 Qed.
 
 (* CMRA *)
@@ -550,19 +550,19 @@ Program Definition listURF (F : urFunctor) : urFunctor := {|
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (urFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_equiv_ext=>y. apply urFunctor_id.
+  apply list_fmap_equiv_ext=>y. apply urFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_equiv_ext=>y; apply urFunctor_compose.
+  apply list_fmap_equiv_ext=>y; apply urFunctor_map_compose.
 Qed.
 
 Instance listURF_contractive F :
   urFunctorContractive F → urFunctorContractive (listURF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 07b2993a16a0745c048bcac36d907b7832a3e29c..82d3e7dc89b4993f46099039d075d6860c5537c4 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -689,22 +689,22 @@ Record oFunctor := OFunctor {
   oFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ofeT;
   oFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → oFunctor_car A1 B1 -n> oFunctor_car A2 B2;
-  oFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
+  oFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     NonExpansive (@oFunctor_map A1 _ A2 _ B1 _ B2 _);
-  oFunctor_id `{!Cofe A, !Cofe B} (x : oFunctor_car A B) :
+  oFunctor_map_id `{!Cofe A, !Cofe B} (x : oFunctor_car A B) :
     oFunctor_map (cid,cid) x ≡ x;
-  oFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
+  oFunctor_map_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     oFunctor_map (f◎g, g'◎f') x ≡ oFunctor_map (g,g') (oFunctor_map (f,f') x)
 }.
-Existing Instance oFunctor_ne.
+Existing Instance oFunctor_map_ne.
 Instance: Params (@oFunctor_map) 9 := {}.
 
 Delimit Scope oFunctor_scope with OF.
 Bind Scope oFunctor_scope with oFunctor.
 
 Class oFunctorContractive (F : oFunctor) :=
-  oFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+  oFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@oFunctor_map F A1 _ A2 _ B1 _ B2 _).
 Hint Mode oFunctorContractive ! : typeclass_instances.
 
@@ -713,6 +713,41 @@ ambiguous coercion paths, see https://gitlab.mpi-sws.org/iris/iris/issues/240. *
 Definition oFunctor_apply (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
   oFunctor_car F A A.
 
+Program Definition oFunctor_oFunctor_compose (F1 F2 : oFunctor)
+  `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} : oFunctor := {|
+  oFunctor_car A _ B _ := oFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
+  oFunctor_map A1 _ A2 _ B1 _ B2 _ 'fg :=
+    oFunctor_map F1 (oFunctor_map F2 (fg.2,fg.1),oFunctor_map F2 fg)
+|}.
+Next Obligation.
+  intros F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
+  apply oFunctor_map_ne; split; apply oFunctor_map_ne; by split.
+Qed.
+Next Obligation.
+  intros F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(oFunctor_map_id F1 x).
+  apply equiv_dist=> n. apply oFunctor_map_ne.
+  split=> y /=; by rewrite !oFunctor_map_id.
+Qed.
+Next Obligation.
+  intros F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
+  rewrite -oFunctor_map_compose. apply equiv_dist=> n. apply oFunctor_map_ne.
+  split=> y /=; by rewrite !oFunctor_map_compose.
+Qed.
+Instance oFunctor_oFunctor_compose_contractive_1 (F1 F2 : oFunctor)
+    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+  oFunctorContractive F1 → oFunctorContractive (oFunctor_oFunctor_compose F1 F2).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
+  f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
+Qed.
+Instance oFunctor_oFunctor_compose_contractive_2 (F1 F2 : oFunctor)
+    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+  oFunctorContractive F2 → oFunctorContractive (oFunctor_oFunctor_compose F1 F2).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
+  f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
+Qed.
+
 Program Definition constOF (B : ofeT) : oFunctor :=
   {| oFunctor_car A1 A2 _ _ := B; oFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
 Solve Obligations with done.
@@ -732,12 +767,12 @@ Program Definition prodOF (F1 F2 : oFunctor) : oFunctor := {|
     prodO_map (oFunctor_map F1 fg) (oFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply prodO_map_ne; apply oFunctor_ne.
+  intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply prodO_map_ne; apply oFunctor_map_ne.
 Qed.
-Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !oFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !oFunctor_map_id. Qed.
 Next Obligation.
   intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
-  by rewrite !oFunctor_compose.
+  by rewrite !oFunctor_map_compose.
 Qed.
 Notation "F1 * F2" := (prodOF F1%OF F2%OF) : oFunctor_scope.
 
@@ -746,7 +781,7 @@ Instance prodOF_contractive F1 F2 :
   oFunctorContractive (prodOF F1 F2).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
-    by apply prodO_map_ne; apply oFunctor_contractive.
+    by apply prodO_map_ne; apply oFunctor_map_contractive.
 Qed.
 
 Program Definition ofe_morOF (F1 F2 : oFunctor) : oFunctor := {|
@@ -756,15 +791,15 @@ Program Definition ofe_morOF (F1 F2 : oFunctor) : oFunctor := {|
 |}.
 Next Obligation.
   intros F1 F2 A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *.
-  apply ofe_morO_map_ne; apply oFunctor_ne; split; by apply Hfg.
+  apply ofe_morO_map_ne; apply oFunctor_map_ne; split; by apply Hfg.
 Qed.
 Next Obligation.
-  intros F1 F2 A ? B ? [f ?] ?; simpl. rewrite /= !oFunctor_id.
-  apply (ne_proper f). apply oFunctor_id.
+  intros F1 F2 A ? B ? [f ?] ?; simpl. rewrite /= !oFunctor_map_id.
+  apply (ne_proper f). apply oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [h ?] ?; simpl in *.
-  rewrite -!oFunctor_compose. do 2 apply (ne_proper _). apply oFunctor_compose.
+  rewrite -!oFunctor_map_compose. do 2 apply (ne_proper _). apply oFunctor_map_compose.
 Qed.
 Notation "F1 -n> F2" := (ofe_morOF F1%OF F2%OF) : oFunctor_scope.
 
@@ -773,7 +808,7 @@ Instance ofe_morOF_contractive F1 F2 :
   oFunctorContractive (ofe_morOF F1 F2).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *.
-  apply ofe_morO_map_ne; apply oFunctor_contractive; destruct n, Hfg; by split.
+  apply ofe_morO_map_ne; apply oFunctor_map_contractive; destruct n, Hfg; by split.
 Qed.
 
 (** * Sum type *)
@@ -848,12 +883,12 @@ Program Definition sumOF (F1 F2 : oFunctor) : oFunctor := {|
     sumO_map (oFunctor_map F1 fg) (oFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply sumO_map_ne; apply oFunctor_ne.
+  intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply sumO_map_ne; apply oFunctor_map_ne.
 Qed.
-Next Obligation. by intros F1 F2 A ? B ? [?|?]; rewrite /= !oFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [?|?]; rewrite /= !oFunctor_map_id. Qed.
 Next Obligation.
   intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [?|?]; simpl;
-    by rewrite !oFunctor_compose.
+    by rewrite !oFunctor_map_compose.
 Qed.
 Notation "F1 + F2" := (sumOF F1%OF F2%OF) : oFunctor_scope.
 
@@ -862,7 +897,7 @@ Instance sumOF_contractive F1 F2 :
   oFunctorContractive (sumOF F1 F2).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
-    by apply sumO_map_ne; apply oFunctor_contractive.
+    by apply sumO_map_ne; apply oFunctor_map_contractive.
 Qed.
 
 (** * Discrete OFEs *)
@@ -1005,21 +1040,22 @@ Program Definition optionOF (F : oFunctor) : oFunctor := {|
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, oFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_equiv_ext=>y; apply oFunctor_id.
+  apply option_fmap_equiv_ext=>y; apply oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_equiv_ext=>y; apply oFunctor_compose.
+  apply option_fmap_equiv_ext=>y; apply oFunctor_map_compose.
 Qed.
 
 Instance optionOF_contractive F :
   oFunctorContractive F → oFunctorContractive (optionOF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, oFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg;
+    apply optionO_map_ne, oFunctor_map_contractive.
 Qed.
 
 (** * Later type *)
@@ -1113,22 +1149,22 @@ Program Definition laterOF (F : oFunctor) : oFunctor := {|
 |}.
 Next Obligation.
   intros F A1 ? A2 ? B1 ? B2 ? n fg fg' ?.
-  by apply (contractive_ne laterO_map), oFunctor_ne.
+  by apply (contractive_ne laterO_map), oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x; simpl. rewrite -{2}(later_map_id x).
-  apply later_map_ext=>y. by rewrite oFunctor_id.
+  apply later_map_ext=>y. by rewrite oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -later_map_compose.
-  apply later_map_ext=>y; apply oFunctor_compose.
+  apply later_map_ext=>y; apply oFunctor_map_compose.
 Qed.
 Notation "â–¶ F"  := (laterOF F%OF) (at level 20, right associativity) : oFunctor_scope.
 
 Instance laterOF_contractive F : oFunctorContractive (laterOF F).
 Proof.
   intros A1 ? A2 ? B1 ? B2 ? n fg fg' Hfg. apply laterO_map_contractive.
-  destruct n as [|n]; simpl in *; first done. apply oFunctor_ne, Hfg.
+  destruct n as [|n]; simpl in *; first done. apply oFunctor_map_ne, Hfg.
 Qed.
 
 (** * Dependently-typed functions over a discrete domain *)
@@ -1222,16 +1258,17 @@ Program Definition discrete_funOF {C} (F : C → oFunctor) : oFunctor := {|
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := discrete_funO_map (λ c, oFunctor_map (F c) fg)
 |}.
 Next Obligation.
-  intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply discrete_funO_map_ne=>?; apply oFunctor_ne.
+  intros C F A1 ? A2 ? B1 ? B2 ? n ?? g.
+  by apply discrete_funO_map_ne=>?; apply oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros C F A ? B ? g; simpl. rewrite -{2}(discrete_fun_map_id g).
-  apply discrete_fun_map_ext=> y; apply oFunctor_id.
+  apply discrete_fun_map_ext=> y; apply oFunctor_map_id.
 Qed.
 Next Obligation.
   intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g.
   rewrite /= -discrete_fun_map_compose.
-  apply discrete_fun_map_ext=>y; apply oFunctor_compose.
+  apply discrete_fun_map_ext=>y; apply oFunctor_map_compose.
 Qed.
 
 Notation "T -d> F" := (@discrete_funOF T%type (λ _, F%OF)) : oFunctor_scope.
@@ -1240,7 +1277,7 @@ Instance discrete_funOF_contractive {C} (F : C → oFunctor) :
   (∀ c, oFunctorContractive (F c)) → oFunctorContractive (discrete_funOF F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
-  by apply discrete_funO_map_ne=>c; apply oFunctor_contractive.
+  by apply discrete_funO_map_ne=>c; apply oFunctor_map_contractive.
 Qed.
 
 (** * Constructing isomorphic OFEs *)
@@ -1503,16 +1540,16 @@ Section sigTOF.
     repeat intro. exists eq_refl => /=. solve_proper.
   Qed.
   Next Obligation.
-    simpl; intros. apply (existT_proper eq_refl), oFunctor_id.
+    simpl; intros. apply (existT_proper eq_refl), oFunctor_map_id.
   Qed.
   Next Obligation.
-    simpl; intros. apply (existT_proper eq_refl), oFunctor_compose.
+    simpl; intros. apply (existT_proper eq_refl), oFunctor_map_compose.
   Qed.
 
   Global Instance sigTOF_contractive {F} :
     (∀ a, oFunctorContractive (F a)) → oFunctorContractive (sigTOF F).
   Proof.
-    repeat intro. apply sigT_map => a. exact: oFunctor_contractive.
+    repeat intro. apply sigT_map => a. exact: oFunctor_map_contractive.
   Qed.
 End sigTOF.
 Arguments sigTOF {_} _%OF.
@@ -1586,14 +1623,14 @@ Program Definition iso_ofe_cong (F : oFunctor) `{!Cofe A, !Cofe B}
   OfeIso (oFunctor_map F (ofe_iso_2 I, ofe_iso_1 I))
     (oFunctor_map F (ofe_iso_1 I, ofe_iso_2 I)) _ _.
 Next Obligation.
-  intros F A ? B ? I x. rewrite -oFunctor_compose -{2}(oFunctor_id F x).
+  intros F A ? B ? I x. rewrite -oFunctor_map_compose -{2}(oFunctor_map_id F x).
   apply equiv_dist=> n.
-  apply oFunctor_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
+  apply oFunctor_map_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
 Qed.
 Next Obligation.
-  intros F A ? B ? I y. rewrite -oFunctor_compose -{2}(oFunctor_id F y).
+  intros F A ? B ? I y. rewrite -oFunctor_map_compose -{2}(oFunctor_map_id F y).
   apply equiv_dist=> n.
-  apply oFunctor_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
+  apply oFunctor_map_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
 Qed.
 Instance iso_ofe_cong_ne (F : oFunctor) `{!Cofe A, !Cofe B} :
   NonExpansive (iso_ofe_cong F (A:=A) (B:=B)).
diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v
index 3ec31e2238ae39054832c7a95ec7f22a04509193..a72c887bb918d58b4026a3a1b63ea0355ec660bf 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -92,7 +92,7 @@ Program Definition vecOF (F : oFunctor) m : oFunctor := {|
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := vecO_map m (oFunctor_map F fg)
 |}.
 Next Obligation.
-  intros F A1 ? A2 ? B1 ? B2 ? n m f g Hfg. by apply vecO_map_ne, oFunctor_ne.
+  intros F A1 ? A2 ? B1 ? B2 ? n m f g Hfg. by apply vecO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F m A ? B ? l.
@@ -103,11 +103,11 @@ Next Obligation.
   intros F m A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' l.
   change (vec_to_list (vec_map m (oFunctor_map F (f â—Ž g, g' â—Ž f')) l)
     ≡ vec_map m (oFunctor_map F (g, g')) (vec_map m (oFunctor_map F (f, f')) l)).
-  rewrite !vec_to_list_map. by apply: (oFunctor_compose (listOF F) f g f' g').
+  rewrite !vec_to_list_map. by apply: (oFunctor_map_compose (listOF F) f g f' g').
 Qed.
 
 Instance vecOF_contractive F m :
   oFunctorContractive F → oFunctorContractive (vecOF F m).
 Proof.
-  by intros ?? A1 ? A2 ? B1 ? B2 ? n ???; apply vecO_map_ne; first apply oFunctor_contractive.
+  by intros ?? A1 ? A2 ? B1 ? B2 ? n ???; apply vecO_map_ne; first apply oFunctor_map_contractive.
 Qed.
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 45fb5407c9553e0473aa302218d465c39d2f969c..8f4cb5cd6902a8ef116d7da60df95847077194ca 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -26,10 +26,10 @@ the agreement CMRA. *)
 category of CMRAs with a proof that it is locally contractive. *)
 Structure gFunctor := GFunctor {
   gFunctor_F :> rFunctor;
-  gFunctor_contractive : rFunctorContractive gFunctor_F;
+  gFunctor_map_contractive : rFunctorContractive gFunctor_F;
 }.
 Arguments GFunctor _ {_}.
-Existing Instance gFunctor_contractive.
+Existing Instance gFunctor_map_contractive.
 Add Printing Constructor gFunctor.
 
 (** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 2f6252b7e5d88267a5c35565f16b5734a7eea50d..d9cc45f05e96bd153ac9bef583f746fd8e7f3957 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -60,7 +60,7 @@ Section saved_anything.
     set (G1 := oFunctor_map F (iProp_fold, iProp_unfold)).
     set (G2 := oFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
     assert (∀ z, G2 (G1 z) ≡ z) as help.
-    { intros z. rewrite /G1 /G2 -oFunctor_compose -{2}[z]oFunctor_id.
+    { intros z. rewrite /G1 /G2 -oFunctor_map_compose -{2}[z]oFunctor_map_id.
       apply (ne_proper (oFunctor_map F)); split=>?; apply iProp_fold_unfold. }
     rewrite -{2}[x]help -{2}[y]help. by iApply f_equiv.
   Qed.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 2d7ce1524b0404281918a62df06f82dde81eae72..e602f4a933a562490cd3a249e99cf501133923bb 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -165,22 +165,22 @@ Program Definition uPredOF (F : urFunctor) : oFunctor := {|
 |}.
 Next Obligation.
   intros F A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
-  apply uPredO_map_ne, urFunctor_ne; split; by apply HPQ.
+  apply uPredO_map_ne, urFunctor_map_ne; split; by apply HPQ.
 Qed.
 Next Obligation.
   intros F A ? B ? P; simpl. rewrite -{2}(uPred_map_id P).
-  apply uPred_map_ext=>y. by rewrite urFunctor_id.
+  apply uPred_map_ext=>y. by rewrite urFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' P; simpl. rewrite -uPred_map_compose.
-  apply uPred_map_ext=>y; apply urFunctor_compose.
+  apply uPred_map_ext=>y; apply urFunctor_map_compose.
 Qed.
 
 Instance uPredOF_contractive F :
   urFunctorContractive F → oFunctorContractive (uPredOF F).
 Proof.
-  intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ. apply uPredO_map_ne, urFunctor_contractive.
-  destruct n; split; by apply HPQ.
+  intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
+  apply uPredO_map_ne, urFunctor_map_contractive. destruct n; split; by apply HPQ.
 Qed.
 
 (** logical entailement *)