From ef41b4a587abcf86674df0f2c07873a98d06aee5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 1 Apr 2020 08:53:20 +0200
Subject: [PATCH] mention which categories these functors map to which

---
 theories/algebra/cmra.v | 3 ++-
 theories/algebra/ofe.v  | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 2944df3d0..1cd3f8d22 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 7a1407ffa..d9a817ce9 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} :
-- 
GitLab