diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 2944df3d03d3981e40ea0bb4eb03537473ec6306..1cd3f8d222b52321c57c4577dd64b736e09ae4cd 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -774,7 +774,7 @@ Section cmra_morphism.
   Proof. rewrite !cmra_valid_validN; eauto using cmra_morphism_validN. Qed.
 End cmra_morphism.
 
-(** Functors *)
+(** OFE → CMRA Functors *)
 Record rFunctor := RFunctor {
   rFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, cmraT;
   rFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
@@ -812,6 +812,7 @@ Coercion constRF : cmraT >-> rFunctor.
 Instance constRF_contractive B : rFunctorContractive (constRF B).
 Proof. rewrite /rFunctorContractive; apply _. Qed.
 
+(** OFE → UCMRA Functors *)
 Record urFunctor := URFunctor {
   urFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ucmraT;
   urFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 7a1407ffaab6ad911a0e0fefb905a1a8e2d505b8..d9a817ce96c719512a1be7deb2388ede5cf57834 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -684,7 +684,7 @@ Instance prodO_map_ne {A A' B B'} :
   NonExpansive2 (@prodO_map A A' B B').
 Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
 
-(** Functors *)
+(** OFE → OFE Functors *)
 Record oFunctor := OFunctor {
   oFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ofeT;
   oFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :