diff --git a/CHANGELOG.md b/CHANGELOG.md
index 70a994380bfe6cc68856b81ff7c4598bf46d9d50..fcb01da5bd8841b1d20b64371a3d2ac20e9c5b07 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -12,6 +12,12 @@ lemma.
   custom proof mode tactics. All other unsealing lemmas should be internal, so
   in principle you should not rely on them.
 
+**Changes in `algebra`:**
+
+* Add some missing algebra functors: `dfrac_agreeRF`, `excl_authURF`, `excl_authRF`,
+  `frac_authURF`, `frac_authRF`, `ufrac_authURF`, `ufrac_authRF`, `max_prefix_listURF`,
+  `max_prefix_listRF`, `mono_listURF`, and `mono_listRF`.
+
 **Changes in `bi`:**
 
 * Generalize `big_op` lemmas that were previously assuming `Absorbing`ness of
diff --git a/iris/algebra/lib/dfrac_agree.v b/iris/algebra/lib/dfrac_agree.v
index 8bd125b3caa5c3848ba71e9fb2b3d5f71dfd6f73..ed13d9e04f9ac2d2259a279196ff69df265c5c04 100644
--- a/iris/algebra/lib/dfrac_agree.v
+++ b/iris/algebra/lib/dfrac_agree.v
@@ -125,5 +125,12 @@ Section lemmas.
 
 End lemmas.
 
+Definition dfrac_agreeRF (F : oFunctor) : rFunctor :=
+  prodRF (constRF dfracR) (agreeRF F).
+
+Global Instance dfrac_agreeRF_contractive F :
+  oFunctorContractive F → rFunctorContractive (dfrac_agreeRF F).
+Proof. apply _. Qed.
+
 Typeclasses Opaque to_dfrac_agree.
 (* [to_frac_agree] is deliberately transparent to reuse the [to_dfrac_agree] instances *)
diff --git a/iris/algebra/lib/excl_auth.v b/iris/algebra/lib/excl_auth.v
index b1cda8d1d872a0c2985bc46e16ab040e1673bafc..da52b48cc41ad090b81ba08c6bb4b6ab363ff217 100644
--- a/iris/algebra/lib/excl_auth.v
+++ b/iris/algebra/lib/excl_auth.v
@@ -69,3 +69,17 @@ Section excl_auth.
     intros. by apply auth_update, option_local_update, exclusive_local_update.
   Qed.
 End excl_auth.
+
+Definition excl_authURF (F : oFunctor) : urFunctor :=
+  authURF (optionURF (exclRF F)).
+
+Global Instance excl_authURF_contractive F :
+  oFunctorContractive F → urFunctorContractive (excl_authURF F).
+Proof. apply _. Qed.
+
+Definition excl_authRF (F : oFunctor) : rFunctor :=
+  authRF (optionURF (exclRF F)).
+
+Global Instance excl_authRF_contractive F :
+  oFunctorContractive F → rFunctorContractive (excl_authRF F).
+Proof. apply _. Qed.
diff --git a/iris/algebra/lib/frac_auth.v b/iris/algebra/lib/frac_auth.v
index 4f456bbc99d92e797902b16d643869b2e8ceeeba..412ada8e4ba9fe1f3bc714f33d8ad3eb8112009c 100644
--- a/iris/algebra/lib/frac_auth.v
+++ b/iris/algebra/lib/frac_auth.v
@@ -119,3 +119,17 @@ Section frac_auth.
     intros. by apply auth_update, option_local_update, exclusive_local_update.
   Qed.
 End frac_auth.
+
+Definition frac_authURF (F : rFunctor) : urFunctor :=
+  authURF (optionURF (prodRF (constRF fracR) F)).
+
+Global Instance frac_authURF_contractive F :
+  rFunctorContractive F → urFunctorContractive (frac_authURF F).
+Proof. apply _. Qed.
+
+Definition frac_authRF (F : rFunctor) : rFunctor :=
+  authRF (optionURF (prodRF (constRF fracR) F)).
+
+Global Instance frac_authRF_contractive F :
+  rFunctorContractive F → rFunctorContractive (frac_authRF F).
+Proof. apply _. Qed.
diff --git a/iris/algebra/lib/mono_list.v b/iris/algebra/lib/mono_list.v
index 60679ecfe04035c69a1f09b69b082363db5479b8..b91656f250e99ff7dd7be95fa5ad5e4f7711ad2b 100644
--- a/iris/algebra/lib/mono_list.v
+++ b/iris/algebra/lib/mono_list.v
@@ -182,3 +182,17 @@ Section mono_list_props.
     by apply auth_update_auth_persist.
   Qed.
 End mono_list_props.
+
+Definition mono_listURF (F : oFunctor) : urFunctor :=
+  authURF (max_prefix_listURF F).
+
+Global Instance mono_listURF_contractive F :
+  oFunctorContractive F → urFunctorContractive (mono_listURF F).
+Proof. apply _. Qed.
+
+Definition mono_listRF (F : oFunctor) : rFunctor :=
+  authRF (max_prefix_listURF F).
+
+Global Instance mono_listRF_contractive F :
+  oFunctorContractive F → rFunctorContractive (mono_listRF F).
+Proof. apply _. Qed.
diff --git a/iris/algebra/lib/ufrac_auth.v b/iris/algebra/lib/ufrac_auth.v
index 12311d84c50c738d969474554e48c1bbcbd6c399..d577614c7d5312097cfb22edeef643551556c338 100644
--- a/iris/algebra/lib/ufrac_auth.v
+++ b/iris/algebra/lib/ufrac_auth.v
@@ -147,3 +147,17 @@ Section ufrac_auth.
       destruct m; simpl; [rewrite left_id | rewrite right_id]; done.
   Qed.
 End ufrac_auth.
+
+Definition ufrac_authURF (F : rFunctor) : urFunctor :=
+  authURF (optionURF (prodRF (constRF ufracR) F)).
+
+Global Instance ufrac_authURF_contractive F :
+  rFunctorContractive F → urFunctorContractive (ufrac_authURF F).
+Proof. apply _. Qed.
+
+Definition ufrac_authRF (F : rFunctor) : rFunctor :=
+  authRF (optionURF (prodRF (constRF ufracR) F)).
+
+Global Instance ufrac_authRF_contractive F :
+  rFunctorContractive F → rFunctorContractive (ufrac_authRF F).
+Proof. apply _. Qed.
diff --git a/iris/algebra/max_prefix_list.v b/iris/algebra/max_prefix_list.v
index 3643c1d83310810f58d7f9fc76dd75579eb70b16..373463caab2a90eae2a02bd584cada856aebed56 100644
--- a/iris/algebra/max_prefix_list.v
+++ b/iris/algebra/max_prefix_list.v
@@ -171,3 +171,17 @@ Section max_prefix_list.
     apply to_max_prefix_list_validN.
   Qed.
 End max_prefix_list.
+
+Definition max_prefix_listURF (F : oFunctor) : urFunctor :=
+  gmapURF nat (agreeRF F).
+
+Global Instance max_prefix_listURF_contractive F :
+  oFunctorContractive F → urFunctorContractive (max_prefix_listURF F).
+Proof. apply _. Qed.
+
+Definition max_prefix_listRF (F : oFunctor) : rFunctor :=
+  gmapRF nat (agreeRF F).
+
+Global Instance max_prefix_listRF_contractive F :
+  oFunctorContractive F → rFunctorContractive (max_prefix_listRF F).
+Proof. apply _. Qed.