diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 8c6a51f9fef68d37fc5b7c0266825f9e06f0484c..6df092d8c8ce059d7a245014a69d346dc53edc83 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -470,28 +470,6 @@ Lemma authO_map_ne A B : NonExpansive (@authO_map A B).
 Proof. intros n f f' Hf [[[]|] ]; repeat constructor; try naive_solver;
   apply agreeO_map_ne; auto. Qed.
 
-Program Definition authRF (F : urFunctor) : rFunctor := {|
-  rFunctor_car A _ B _ := authR (urFunctor_car F A B);
-  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_map_ne.
-Qed.
-Next Obligation.
-  intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
-  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_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_map_contractive.
-Qed.
-
 Program Definition authURF (F : urFunctor) : urFunctor := {|
   urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authO_map (urFunctor_map F fg)
@@ -513,3 +491,6 @@ Instance authURF_contractive F :
 Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_contractive.
 Qed.
+
+Definition authRF (F : urFunctor) :=
+  urFunctor_to_rFunctor (authURF F).
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index a3d20798d9166cf2d72f88f76d68191431cb2aa7..e8fd4744495d2386a19e7a34e709f1eadc4db281 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -805,6 +805,24 @@ Class rFunctorContractive (F : rFunctor) :=
 Definition rFunctor_apply (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
   rFunctor_car F A A.
 
+Program Definition rFunctor_to_oFunctor (F: rFunctor) : oFunctor := {|
+  oFunctor_car A _ B _ := rFunctor_car F A B;
+  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := rFunctor_map F fg
+|}.
+Next Obligation.
+  intros F A ? B ? x. simpl in *. apply rFunctor_map_id.
+Qed.
+Next Obligation.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. simpl in *.
+  apply rFunctor_map_compose.
+Qed.
+
+Global Instance rFunctor_to_oFunctor_contractive F :
+  rFunctorContractive F → oFunctorContractive (rFunctor_to_oFunctor F).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg. apply rFunctor_map_contractive. done.
+Qed.
+
 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);
@@ -878,6 +896,24 @@ Class urFunctorContractive (F : urFunctor) :=
 Definition urFunctor_apply (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
   urFunctor_car F A A.
 
+Program Definition urFunctor_to_rFunctor (F: urFunctor) : rFunctor := {|
+  rFunctor_car A _ B _ := urFunctor_car F A B;
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := urFunctor_map F fg
+|}.
+Next Obligation.
+  intros F A ? B ? x. simpl in *. apply urFunctor_map_id.
+Qed.
+Next Obligation.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. simpl in *.
+  apply urFunctor_map_compose.
+Qed.
+
+Global Instance urFunctor_to_rFunctor_contractive F :
+  urFunctorContractive F → rFunctorContractive (urFunctor_to_rFunctor F).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg. apply urFunctor_map_contractive. done.
+Qed.
+
 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);
@@ -1502,28 +1538,6 @@ Proof.
   - move=> [a|] [b|] //=. by rewrite (cmra_morphism_op f).
 Qed.
 
-Program Definition optionRF (F : rFunctor) : rFunctor := {|
-  rFunctor_car A _ B _ := optionR (rFunctor_car F A B);
-  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_map_ne.
-Qed.
-Next Obligation.
-  intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
-  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_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_map_contractive.
-Qed.
-
 Program Definition optionURF (F : rFunctor) : urFunctor := {|
   urFunctor_car A _ B _ := optionUR (rFunctor_car F A B);
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
@@ -1546,6 +1560,9 @@ Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
 Qed.
 
+Definition optionRF (F : rFunctor) : rFunctor :=
+  urFunctor_to_rFunctor (optionURF F).
+
 (* Dependently-typed functions over a discrete domain *)
 Section discrete_fun_cmra.
   Context `{B : A → ucmraT}.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 714a62663e71eb8ec800f54b6e9c593f767ff851..e487eb44f02b838cc440bf74e59e5a40f0e1042f 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -675,8 +675,11 @@ 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_map_compose.
 Qed.
-Instance gmapRF_contractive K `{Countable K} F :
+Instance gmapURF_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_map_contractive.
 Qed.
+
+Definition gmapRF K `{Countable K} (F : rFunctor) : rFunctor :=
+  urFunctor_to_rFunctor (gmapURF K F).
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 5c94e79b684c3113c3b5163a60ba3bfef0a11c3b..9aa39210779a5fd5cf85bfdbee53229fc3e344ad 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -186,7 +186,7 @@ Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_contractive.
 Qed.
 
-(* CMRA *)
+(* CMRA. Only works if [A] has a unit! *)
 Section cmra.
   Context {A : ucmraT}.
   Implicit Types l : list A.
@@ -571,3 +571,6 @@ Instance listURF_contractive F :
 Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_map_contractive.
 Qed.
+
+Definition listRF (F : urFunctor) : rFunctor :=
+  urFunctor_to_rFunctor (listURF F).