From 5b0c6378cbf42d0247fa5e437b405a5775fad513 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 2 Mar 2016 02:26:22 +0100
Subject: [PATCH] Introduce cofeT -> cofeT functors, switch to bifunctors.

This cleans up some ad-hoc stuff and prepares for a generalization
of saved propositions.
---
 _CoqProject                     |   1 -
 algebra/agree.v                 |  20 +++-
 algebra/auth.v                  |  17 ++--
 algebra/cmra.v                  |  56 +++++++++++
 algebra/cofe.v                  |  51 ++++++++++
 algebra/cofe_solver.v           |  52 +++++------
 algebra/excl.v                  |  12 ++-
 algebra/fin_maps.v              |  33 +++++--
 algebra/frac.v                  |  17 ++--
 algebra/functor.v               |  41 --------
 algebra/iprod.v                 |  34 +++++--
 algebra/option.v                |  33 +++++--
 algebra/upred.v                 |  18 +++-
 barrier/client.v                |   4 +-
 barrier/proof.v                 |   6 +-
 barrier/specification.v         |   2 +-
 heap_lang/derived.v             |   2 +-
 heap_lang/heap.v                |   4 +-
 heap_lang/lifting.v             |   2 +-
 heap_lang/tests.v               |   2 +-
 program_logic/adequacy.v        |   2 +-
 program_logic/auth.v            |   2 +-
 program_logic/ghost_ownership.v |  11 ++-
 program_logic/global_functor.v  |  60 ++++++------
 program_logic/hoare.v           |   2 +-
 program_logic/hoare_lifting.v   |   2 +-
 program_logic/invariants.v      |   2 +-
 program_logic/language.v        |   2 +-
 program_logic/lifting.v         |   2 +-
 program_logic/model.v           |  48 ++++------
 program_logic/ownership.v       |   2 +-
 program_logic/pviewshifts.v     |   2 +-
 program_logic/resources.v       | 159 ++++++++++++++++++--------------
 program_logic/saved_prop.v      |   2 +-
 program_logic/sts.v             |   2 +-
 program_logic/tests.v           |   2 +-
 program_logic/viewshifts.v      |   2 +-
 program_logic/weakestpre.v      |   2 +-
 program_logic/wsat.v            |   2 +-
 39 files changed, 432 insertions(+), 283 deletions(-)
 delete mode 100644 algebra/functor.v

diff --git a/_CoqProject b/_CoqProject
index e6b7feed3..ea8f064ff 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -50,7 +50,6 @@ algebra/agree.v
 algebra/dec_agree.v
 algebra/excl.v
 algebra/iprod.v
-algebra/functor.v
 algebra/upred.v
 algebra/upred_tactics.v
 algebra/upred_big_op.v
diff --git a/algebra/agree.v b/algebra/agree.v
index 34e11c545..df3085f9b 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -1,5 +1,5 @@
 From algebra Require Export cmra.
-From algebra Require Import functor upred.
+From algebra Require Import upred.
 Local Hint Extern 10 (_ ≤ _) => omega.
 
 Record agree (A : Type) : Type := Agree {
@@ -180,6 +180,18 @@ Proof.
   by apply dist_le with n; try apply Hfg.
 Qed.
 
-Program Definition agreeF : iFunctor :=
-  {| ifunctor_car := agreeR; ifunctor_map := @agreeC_map |}.
-Solve Obligations with done.
+Program Definition agreeRF (F : cFunctor) : rFunctor := {|
+  rFunctor_car A B := agreeR (cFunctor_car F A B);
+  rFunctor_map A1 A2 B1 B2 fg := agreeC_map (cFunctor_map F fg)
+|}.
+Next Obligation.
+  intros F A1 A2 B1 B2 n ???; simpl. by apply agreeC_map_ne, cFunctor_ne.
+Qed.
+Next Obligation.
+  intros F A B x; simpl. rewrite -{2}(agree_map_id x).
+  apply agree_map_ext=>y. by rewrite cFunctor_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 cFunctor_compose.
+Qed.
diff --git a/algebra/auth.v b/algebra/auth.v
index 87265cb0e..85487ebe4 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -1,5 +1,5 @@
 From algebra Require Export excl.
-From algebra Require Import functor upred.
+From algebra Require Import upred.
 Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
 
@@ -240,17 +240,18 @@ Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
 Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
 Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed.
 
-Program Definition authF (Σ : iFunctor) : iFunctor := {|
-  ifunctor_car := authR ∘ Σ; ifunctor_map A B := authC_map ∘ ifunctor_map Σ
+Program Definition authRF (F : rFunctor) : rFunctor := {|
+  rFunctor_car A B := authR (rFunctor_car F A B);
+  rFunctor_map A1 A2 B1 B2 fg := authC_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros Σ A B n f g Hfg; apply authC_map_ne, ifunctor_map_ne.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, rFunctor_ne.
 Qed.
 Next Obligation.
-  intros Σ A x. rewrite /= -{2}(auth_map_id x).
-  apply auth_map_ext=>y; apply ifunctor_map_id.
+  intros F A B x. rewrite /= -{2}(auth_map_id x).
+  apply auth_map_ext=>y; apply rFunctor_id.
 Qed.
 Next Obligation.
-  intros Σ A B C f g x. rewrite /= -auth_map_compose.
-  apply auth_map_ext=>y; apply ifunctor_map_compose.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
+  apply auth_map_ext=>y; apply rFunctor_compose.
 Qed.
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 0cd4cb09d..a8642311e 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -617,3 +617,59 @@ Proof.
   - intros x y; rewrite !prod_included=> -[??] /=.
     by split; apply included_preserving.
 Qed.
+
+(** Functors *)
+Structure rFunctor := RFunctor {
+  rFunctor_car : cofeT → cofeT -> cmraT;
+  rFunctor_map {A1 A2 B1 B2} :
+    ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
+  rFunctor_ne {A1 A2 B1 B2} n :
+    Proper (dist n ==> dist n) (@rFunctor_map A1 A2 B1 B2);
+  rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x ≡ x;
+  rFunctor_compose {A1 A2 A3 B1 B2 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_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
+    CMRAMonotone (rFunctor_map fg) 
+}.
+Existing Instances rFunctor_ne rFunctor_mono.
+Instance: Params (@rFunctor_map) 5.
+
+Definition rFunctor_diag (F: rFunctor) (A: cofeT) : cmraT := rFunctor_car F A A.
+Coercion rFunctor_diag : rFunctor >-> Funclass.
+
+Program Definition constRF (B : cmraT) : rFunctor :=
+  {| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
+Solve Obligations with done.
+
+Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
+  rFunctor_car A B := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
+  rFunctor_map A1 A2 B1 B2 fg :=
+    prodC_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
+|}.
+Next Obligation.
+  by intros F1 F2 A1 A2 B1 B2 n ???; apply prodC_map_ne; apply rFunctor_ne.
+Qed.
+Next Obligation. by intros F1 F2 A B [??]; rewrite /= !rFunctor_id. Qed.
+Next Obligation.
+  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
+  by rewrite !rFunctor_compose.
+Qed.
+
+Program Definition laterRF (F : rFunctor) : rFunctor := {|
+  rFunctor_car A B := rFunctor_car F (laterC A) (laterC B);
+  rFunctor_map A1 A2 B1 B2 fg :=
+    rFunctor_map F (prod_map laterC_map laterC_map fg)
+|}.
+Next Obligation.
+  intros F A1 A2 B1 B2 n x y [??].
+  by apply rFunctor_ne; split; apply (contractive_ne laterC_map).
+Qed.
+Next Obligation.
+  intros F A B x; simpl. rewrite -{2}[x]rFunctor_id.
+  apply (ne_proper (rFunctor_map F)); split; by intros [].
+Qed.
+Next Obligation.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl in *. rewrite -rFunctor_compose.
+  apply (ne_proper (rFunctor_map F)); split; by intros [].
+Qed.
diff --git a/algebra/cofe.v b/algebra/cofe.v
index d8c5c3391..e56587124 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -310,6 +310,47 @@ Instance prodC_map_ne {A A' B B'} n :
   Proper (dist n ==> dist n ==> dist n) (@prodC_map A A' B B').
 Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
 
+(** Functors *)
+Structure cFunctor := CFunctor {
+  cFunctor_car : cofeT → cofeT -> cofeT;
+  cFunctor_map {A1 A2 B1 B2} :
+    ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
+  cFunctor_ne {A1 A2 B1 B2} n :
+    Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2);
+  cFunctor_id {A B : cofeT} (x : cFunctor_car A B) :
+    cFunctor_map (cid,cid) x ≡ x;
+  cFunctor_compose {A1 A2 A3 B1 B2 B3}
+      (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
+    cFunctor_map (f◎g, g'◎f') x ≡ cFunctor_map (g,g') (cFunctor_map (f,f') x)
+}.
+Existing Instances cFunctor_ne.
+Instance: Params (@cFunctor_map) 5.
+
+Definition cFunctor_diag (F: cFunctor) (A: cofeT) : cofeT := cFunctor_car F A A.
+Coercion cFunctor_diag : cFunctor >-> Funclass.
+
+Program Definition idCF : cFunctor :=
+  {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}.
+Solve Obligations with done.
+
+Program Definition constCF (B : cofeT) : cFunctor :=
+  {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}.
+Solve Obligations with done.
+
+Program Definition prodCF (F1 F2 : cFunctor) : cFunctor := {|
+  cFunctor_car A B := prodC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
+  cFunctor_map A1 A2 B1 B2 fg :=
+    prodC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg)
+|}.
+Next Obligation.
+  by intros F1 F2 A1 A2 B1 B2 n ???; apply prodC_map_ne; apply cFunctor_ne.
+Qed.
+Next Obligation. by intros F1 F2 A B [??]; rewrite /= !cFunctor_id. Qed.
+Next Obligation.
+  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
+  by rewrite !cFunctor_compose.
+Qed.
+
 (** Discrete cofe *)
 Section discrete_cofe.
   Context `{Equiv A, @Equivalence A (≡)}.
@@ -390,3 +431,13 @@ Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
   CofeMor (later_map f).
 Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
 Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
+
+Program Definition laterCF : cFunctor := {|
+  cFunctor_car A B := laterC B;
+  cFunctor_map A1 A2 B1 B2 fg := laterC_map (fg.2)
+|}.
+Next Obligation.
+  intros F A1 A2 B1 B2 n ? [??]; simpl. by apply (contractive_ne laterC_map).
+Qed.
+Next Obligation. by intros A B []. Qed.
+Next Obligation. by intros A1 A2 A3 B1 B2 B3 f g f' g' []. Qed.
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index 8012d3287..ba4fffea1 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -1,9 +1,9 @@
 From algebra Require Export cofe.
 
-Record solution (F : cofeT → cofeT → cofeT) := Solution {
+Record solution (F : cFunctor) := Solution {
   solution_car :> cofeT;
-  solution_unfold : solution_car -n> F solution_car solution_car;
-  solution_fold : F solution_car solution_car -n> solution_car;
+  solution_unfold : solution_car -n> F solution_car;
+  solution_fold : F solution_car -n> solution_car;
   solution_fold_unfold X : solution_fold (solution_unfold X) ≡ X;
   solution_unfold_fold X : solution_unfold (solution_fold X) ≡ X
 }.
@@ -11,20 +11,13 @@ Arguments solution_unfold {_} _.
 Arguments solution_fold {_} _.
 
 Module solver. Section solver.
-Context (F : cofeT → cofeT → cofeT).
-Context `{Finhab : Inhabited (F unitC unitC)}.
-Context (map : ∀ {A1 A2 B1 B2 : cofeT},
-  ((A2 -n> A1) * (B1 -n> B2)) → (F A1 B1 -n> F A2 B2)).
-Arguments map {_ _ _ _} _.
-Instance: Params (@map) 4.
-Context (map_id : ∀ {A B : cofeT} (x : F A B), map (cid, cid) x ≡ x).
-Context (map_comp : ∀ {A1 A2 A3 B1 B2 B3 : cofeT}
-    (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x,
-  map (f ◎ g, g' ◎ f') x ≡ map (g,g') (map (f,f') x)).
-Context (map_contractive : ∀ {A1 A2 B1 B2}, Contractive (@map A1 A2 B1 B2)).
+Context (F : cFunctor) `{Finhab : Inhabited (F unitC)}.
+Context (map_contractive : ∀ {A1 A2 B1 B2},
+  Contractive (@cFunctor_map F A1 A2 B1 B2)).
+Notation map := (cFunctor_map F).
 
 Fixpoint A (k : nat) : cofeT :=
-  match k with 0 => unitC | S k => F (A k) (A k) end.
+  match k with 0 => unitC | S k => F (A k) end.
 Fixpoint f (k : nat) : A k -n> A (S k) :=
   match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
 with g (k : nat) : A (S k) -n> A k :=
@@ -38,13 +31,15 @@ Arguments g : simpl never.
 Lemma gf {k} (x : A k) : g k (f k x) ≡ x.
 Proof.
   induction k as [|k IH]; simpl in *; [by destruct x|].
-  rewrite -map_comp -{2}(map_id _ _ x). by apply (contractive_proper map).
+  rewrite -cFunctor_compose -{2}[x]cFunctor_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.
   induction k as [|k IH]; simpl.
-  - rewrite f_S g_S -{2}(map_id _ _ x) -map_comp. apply (contractive_0 map).
-  - rewrite f_S g_S -{2}(map_id _ _ x) -map_comp. by apply (contractive_S map).
+  - rewrite f_S g_S -{2}[x]cFunctor_id -cFunctor_compose.
+    apply (contractive_0 map).
+  - rewrite f_S g_S -{2}[x]cFunctor_id -cFunctor_compose.
+    by apply (contractive_S map).
 Qed.
 
 Record tower := {
@@ -174,28 +169,28 @@ Proof.
   - rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
 Qed.
 
-Program Definition unfold_chain (X : T) : chain (F T T) :=
+Program Definition unfold_chain (X : T) : chain (F T) :=
   {| chain_car n := map (project n,embed' n) (X (S n)) |}.
 Next Obligation.
   intros X n i Hi.
   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 -map_comp.
+  rewrite f_S -cFunctor_compose.
   by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
 Qed.
-Definition unfold (X : T) : F T T := compl (unfold_chain X).
+Definition unfold (X : T) : F T := compl (unfold_chain X).
 Instance unfold_ne : Proper (dist n ==> dist n) unfold.
 Proof.
   intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X))
     (conv_compl n (unfold_chain Y)) /= (HXY (S n)).
 Qed.
 
-Program Definition fold (X : F T T) : T :=
+Program Definition fold (X : 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 -map_comp.
+  rewrite g_S -cFunctor_compose.
   apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower].
 Qed.
 Instance fold_ne : Proper (dist n ==> dist n) fold.
@@ -204,14 +199,13 @@ Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
 Theorem result : solution F.
 Proof.
   apply (Solution F T (CofeMor unfold) (CofeMor fold)).
-  - move=> X /=.
-    rewrite equiv_dist; intros n k; unfold unfold, fold; simpl.
+  - move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=.
     rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
     trans (map (ff n, gg n) (X (S (n + k)))).
     { 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 -!map_comp; apply (contractive_ne map); split=> Y.
+      rewrite f_S -!cFunctor_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.
@@ -221,14 +215,14 @@ Proof.
     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 map_id. }
-      rewrite map_comp g_coerce; apply IH. }
+      { by rewrite coerce_id cFunctor_id. }
+      rewrite cFunctor_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 -!map_comp -{2}(map_id _ _ X).
+    rewrite g_S -!cFunctor_compose -{2}[X]cFunctor_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/algebra/excl.v b/algebra/excl.v
index cabc2bf34..6fa18deac 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -1,5 +1,5 @@
 From algebra Require Export cmra.
-From algebra Require Import functor upred.
+From algebra Require Import upred.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
@@ -201,7 +201,9 @@ Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
 Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
 Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
 
-Program Definition exclF : iFunctor :=
-  {| ifunctor_car := exclR; ifunctor_map := @exclC_map |}.
-Next Obligation. by intros A x; rewrite /= excl_map_id. Qed.
-Next Obligation. by intros A B C f g x; rewrite /= excl_map_compose. Qed.
+Program Definition exclF : rFunctor := {|
+  rFunctor_car A B := exclR B; rFunctor_map A1 A2 B1 B2 fg := exclC_map (fg.2)
+|}.
+Next Obligation. intros A1 A2 B1 B2 n x1 x2 [??]. by apply exclC_map_ne. Qed.
+Next Obligation. by intros A B x; rewrite /= excl_map_id. Qed.
+Next Obligation. by intros A1 A2 A3 B1 B2 B3 *;rewrite /= excl_map_compose. Qed.
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index af5f44612..d18158e22 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -1,6 +1,6 @@
 From algebra Require Export cmra option.
 From prelude Require Export gmap.
-From algebra Require Import functor upred.
+From algebra Require Import upred.
 
 Section cofe.
 Context `{Countable K} {A : cofeT}.
@@ -352,17 +352,34 @@ Proof.
   destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
 Qed.
 
-Program Definition mapF K `{Countable K} (Σ : iFunctor) : iFunctor := {|
-  ifunctor_car := mapR K ∘ Σ; ifunctor_map A B := mapC_map ∘ ifunctor_map Σ
+Program Definition mapCF K `{Countable K} (F : cFunctor) : cFunctor := {|
+  cFunctor_car A B := mapC K (cFunctor_car F A B);
+  cFunctor_map A1 A2 B1 B2 fg := mapC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros K ?? Σ A B n f g Hfg; apply mapC_map_ne, ifunctor_map_ne.
+  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, cFunctor_ne.
 Qed.
 Next Obligation.
-  intros K ?? Σ A x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_id.
+  intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
+  apply map_fmap_setoid_ext=>y ??; apply cFunctor_id.
 Qed.
 Next Obligation.
-  intros K ?? Σ A B C f g x. rewrite /= -map_fmap_compose.
-  apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_compose.
+  intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
+  apply map_fmap_setoid_ext=>y ??; apply cFunctor_compose.
+Qed.
+
+Program Definition mapRF K `{Countable K} (F : rFunctor) : rFunctor := {|
+  rFunctor_car A B := mapR K (rFunctor_car F A B);
+  rFunctor_map A1 A2 B1 B2 fg := mapC_map (rFunctor_map F fg)
+|}.
+Next Obligation.
+  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, rFunctor_ne.
+Qed.
+Next Obligation.
+  intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
+  apply map_fmap_setoid_ext=>y ??; apply rFunctor_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_setoid_ext=>y ??; apply rFunctor_compose.
 Qed.
diff --git a/algebra/frac.v b/algebra/frac.v
index 6421ded82..ea3777620 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From algebra Require Export cmra.
-From algebra Require Import functor upred.
+From algebra Require Import upred.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments div _ _ !_ !_ /.
@@ -244,17 +244,18 @@ Proof.
     by exists (Frac q3 b); constructor.
 Qed.
 
-Program Definition fracF (Σ : iFunctor) : iFunctor := {|
-  ifunctor_car := fracR ∘ Σ; ifunctor_map A B := fracC_map ∘ ifunctor_map Σ
+Program Definition fracRF (F : rFunctor) : rFunctor := {|
+  rFunctor_car A B := fracR (rFunctor_car F A B);
+  rFunctor_map A1 A2 B1 B2 fg := fracC_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros Σ A B n f g Hfg; apply fracC_map_ne, ifunctor_map_ne.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_ne.
 Qed.
 Next Obligation.
-  intros Σ A x. rewrite /= -{2}(frac_map_id x).
-  apply frac_map_ext=>y; apply ifunctor_map_id.
+  intros F A B x. rewrite /= -{2}(frac_map_id x).
+  apply frac_map_ext=>y; apply rFunctor_id.
 Qed.
 Next Obligation.
-  intros Σ A B C f g x. rewrite /= -frac_map_compose.
-  apply frac_map_ext=>y; apply ifunctor_map_compose.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -frac_map_compose.
+  apply frac_map_ext=>y; apply rFunctor_compose.
 Qed.
diff --git a/algebra/functor.v b/algebra/functor.v
deleted file mode 100644
index 8a8d675eb..000000000
--- a/algebra/functor.v
+++ /dev/null
@@ -1,41 +0,0 @@
-From algebra Require Export cmra.
-
-(** * Functors from COFE to CMRA *)
-(* TODO RJ: Maybe find a better name for this? It is not PL-specific any more. *)
-Structure iFunctor := IFunctor {
-  ifunctor_car :> cofeT → cmraT;
-  ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B;
-  ifunctor_map_ne {A B} n : Proper (dist n ==> dist n) (@ifunctor_map A B);
-  ifunctor_map_id {A : cofeT} (x : ifunctor_car A) : ifunctor_map cid x ≡ x;
-  ifunctor_map_compose {A B C} (f : A -n> B) (g : B -n> C) x :
-    ifunctor_map (g ◎ f) x ≡ ifunctor_map g (ifunctor_map f x);
-  ifunctor_map_mono {A B} (f : A -n> B) : CMRAMonotone (ifunctor_map f)
-}.
-Existing Instances ifunctor_map_ne ifunctor_map_mono.
-
-Lemma ifunctor_map_ext (Σ : iFunctor) {A B} (f g : A -n> B) m :
-  (∀ x, f x ≡ g x) → ifunctor_map Σ f m ≡ ifunctor_map Σ g m.
-Proof. by intros; apply (ne_proper (@ifunctor_map Σ A B)). Qed.
-
-(** * Functor combinators *)
-(** We create a functor combinators for all CMRAs in the algebra directory.
-These combinators can be used to conveniently construct the global CMRA of
-the Iris program logic. Note that we have explicitly built in functor
-composition into these combinators, instead of having a notion of a functor
-from the category of CMRAs to the category of CMRAs which we can compose. This
-way we can convenient deal with (indexed) products in a uniform way. *)
-Program Definition constF (B : cmraT) : iFunctor :=
-  {| ifunctor_car A := B; ifunctor_map A1 A2 f := cid |}.
-Solve Obligations with done.
-
-Program Definition prodF (Σ1 Σ2 : iFunctor) : iFunctor := {|
-  ifunctor_car A := prodR (Σ1 A) (Σ2 A);
-  ifunctor_map A B f := prodC_map (ifunctor_map Σ1 f) (ifunctor_map Σ2 f)
-|}.
-Next Obligation.
-  by intros Σ1 Σ2 A B n f g Hfg; apply prodC_map_ne; apply ifunctor_map_ne.
-Qed.
-Next Obligation. by intros Σ1 Σ2 A [??]; rewrite /= !ifunctor_map_id. Qed.
-Next Obligation.
-  by intros Σ1 Σ2 A B C f g [??]; rewrite /= !ifunctor_map_compose.
-Qed.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index b5d6f1d43..68da8987f 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -1,5 +1,5 @@
 From algebra Require Export cmra.
-From algebra Require Import functor upred.
+From algebra Require Import upred.
 
 (** * Indexed product *)
 (** Need to put this in a definition to make canonical structures to work. *)
@@ -288,18 +288,34 @@ Instance iprodC_map_ne {A} {B1 B2 : A → cofeT} n :
   Proper (dist n ==> dist n) (@iprodC_map A B1 B2).
 Proof. intros f1 f2 Hf g x; apply Hf. Qed.
 
-Program Definition iprodF {A} (Σ : A → iFunctor) : iFunctor := {|
-  ifunctor_car B := iprodR (λ x, Σ x B);
-  ifunctor_map B1 B2 f := iprodC_map (λ x, ifunctor_map (Σ x) f);
+Program Definition iprodCF {C} (F : C → cFunctor) : cFunctor := {|
+  cFunctor_car A B := iprodC (λ c, cFunctor_car (F c) A B);
+  cFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, cFunctor_map (F c) fg)
 |}.
 Next Obligation.
-  by intros A Σ B1 B2 n f f' ? g; apply iprodC_map_ne=>x; apply ifunctor_map_ne.
+  by intros C F A1 A2 B1 B2 n ?? g; apply iprodC_map_ne=>c; apply cFunctor_ne.
 Qed.
 Next Obligation.
-  intros A Σ B g. rewrite /= -{2}(iprod_map_id g).
-  apply iprod_map_ext=> x; apply ifunctor_map_id.
+  intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).
+  apply iprod_map_ext=> y; apply cFunctor_id.
 Qed.
 Next Obligation.
-  intros A Σ B1 B2 B3 f1 f2 g. rewrite /= -iprod_map_compose.
-  apply iprod_map_ext=> y; apply ifunctor_map_compose.
+  intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
+  apply iprod_map_ext=>y; apply cFunctor_compose.
+Qed.
+
+Program Definition iprodRF {C} (F : C → rFunctor) : rFunctor := {|
+  rFunctor_car A B := iprodR (λ c, rFunctor_car (F c) A B);
+  rFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, rFunctor_map (F c) fg)
+|}.
+Next Obligation.
+  by intros C F A1 A2 B1 B2 n ?? g; apply iprodC_map_ne=>c; apply rFunctor_ne.
+Qed.
+Next Obligation.
+  intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).
+  apply iprod_map_ext=> y; apply rFunctor_id.
+Qed.
+Next Obligation.
+  intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
+  apply iprod_map_ext=>y; apply rFunctor_compose.
 Qed.
diff --git a/algebra/option.v b/algebra/option.v
index dab77e881..b68ea13f5 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -1,5 +1,5 @@
 From algebra Require Export cmra.
-From algebra Require Import functor upred.
+From algebra Require Import upred.
 
 (* COFE *)
 Section cofe.
@@ -189,17 +189,34 @@ Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
 Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B).
 Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
 
-Program Definition optionF (Σ : iFunctor) : iFunctor := {|
-  ifunctor_car := optionR ∘ Σ; ifunctor_map A B := optionC_map ∘ ifunctor_map Σ
+Program Definition optionCF (F : cFunctor) : cFunctor := {|
+  cFunctor_car A B := optionC (cFunctor_car F A B);
+  cFunctor_map A1 A2 B1 B2 fg := optionC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros Σ A B n f g Hfg; apply optionC_map_ne, ifunctor_map_ne.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_ne.
 Qed.
 Next Obligation.
-  intros Σ A x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_setoid_ext=>y; apply ifunctor_map_id.
+  intros F A B x. rewrite /= -{2}(option_fmap_id x).
+  apply option_fmap_setoid_ext=>y; apply cFunctor_id.
 Qed.
 Next Obligation.
-  intros Σ A B C f g x. rewrite /= -option_fmap_compose.
-  apply option_fmap_setoid_ext=>y; apply ifunctor_map_compose.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
+  apply option_fmap_setoid_ext=>y; apply cFunctor_compose.
+Qed.
+
+Program Definition optionRF (F : rFunctor) : rFunctor := {|
+  rFunctor_car A B := optionR (rFunctor_car F A B);
+  rFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
+|}.
+Next Obligation.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
+Qed.
+Next Obligation.
+  intros F A B x. rewrite /= -{2}(option_fmap_id x).
+  apply option_fmap_setoid_ext=>y; apply rFunctor_id.
+Qed.
+Next Obligation.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
+  apply option_fmap_setoid_ext=>y; apply rFunctor_compose.
 Qed.
diff --git a/algebra/upred.v b/algebra/upred.v
index 659af0b65..c1dbf38f6 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -89,7 +89,7 @@ Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
 Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
 Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
   uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
-Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
+Lemma uPredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
     `{!CMRAMonotone f, !CMRAMonotone g} n :
   f ≡{n}≡ g → uPredC_map f ≡{n}≡ uPredC_map g.
 Proof.
@@ -97,6 +97,22 @@ Proof.
     rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
 Qed.
 
+Program Definition uPredCF (F : rFunctor) : cFunctor := {|
+  cFunctor_car A B := uPredC (rFunctor_car F B A);
+  cFunctor_map A1 A2 B1 B2 fg := uPredC_map (rFunctor_map F (fg.2, fg.1))
+|}.
+Next Obligation.
+  intros F A1 A2 B1 B2 n P Q [??]. by apply uPredC_map_ne, rFunctor_ne.
+Qed.
+Next Obligation.
+  intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
+  apply uPred_map_ext=>y. by rewrite rFunctor_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 rFunctor_compose.
+Qed.
+
 (** logical entailement *)
 Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
   { uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }.
diff --git a/barrier/client.v b/barrier/client.v
index 8493373c9..30c450921 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -11,7 +11,7 @@ Definition client : expr :=
   "y" <- (λ: "z", "z" + '42) ;; signal "b".
 
 Section client.
-  Context {Σ : iFunctorG} `{!heapG Σ, !barrierG Σ} (heapN N : namespace).
+  Context {Σ : rFunctorG} `{!heapG Σ, !barrierG Σ} (heapN N : namespace).
   Local Notation iProp := (iPropG heap_lang Σ).
 
   Definition y_inv q y : iProp := (∃ f : val, y ↦{q} f ★ □ ∀ n : Z,
@@ -72,7 +72,7 @@ Section client.
 End client.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := #[ heapGF ; barrierGF ].
+  Definition Σ : rFunctorG := #[ heapGF ; barrierGF ].
   Notation iProp := (iPropG heap_lang Σ).
 
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
diff --git a/barrier/proof.v b/barrier/proof.v
index ca58bd09a..bb051fec7 100644
--- a/barrier/proof.v
+++ b/barrier/proof.v
@@ -12,15 +12,15 @@ Class barrierG Σ := BarrierG {
   barrier_stsG :> stsG heap_lang Σ sts;
   barrier_savedPropG :> savedPropG heap_lang Σ;
 }.
-Definition barrierGF : iFunctors := [stsGF sts; agreeF].
+Definition barrierGF : rFunctors := [stsGF sts; agreeRF idCF].
 
 Instance inGF_barrierG
-  `{inGF heap_lang Σ (stsGF sts), inGF heap_lang Σ agreeF} : barrierG Σ.
+  `{inGF heap_lang Σ (stsGF sts), inGF heap_lang Σ (agreeRF idCF)} : barrierG Σ.
 Proof. split; apply _. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-Context {Σ : iFunctorG} `{!heapG Σ, !barrierG Σ}.
+Context {Σ : rFunctorG} `{!heapG Σ, !barrierG Σ}.
 Context (heapN N : namespace).
 Local Notation iProp := (iPropG heap_lang Σ).
 
diff --git a/barrier/specification.v b/barrier/specification.v
index 5024c3b9a..499e810e0 100644
--- a/barrier/specification.v
+++ b/barrier/specification.v
@@ -4,7 +4,7 @@ From barrier Require Import proof.
 Import uPred.
 
 Section spec.
-Context {Σ : iFunctorG} `{!heapG Σ} `{!barrierG Σ}. 
+Context {Σ : rFunctorG} `{!heapG Σ} `{!barrierG Σ}. 
 
 Local Notation iProp := (iPropG heap_lang Σ).
 
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index d3772f31c..0b5eaa8b0 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -11,7 +11,7 @@ Notation SeqCtx e2 := (LetCtx "" e2).
 Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
 
 Section derived.
-Context {Σ : iFunctor}.
+Context {Σ : rFunctor}.
 Implicit Types P Q : iProp heap_lang Σ.
 Implicit Types Φ : val → iProp heap_lang Σ.
 
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index ed67f6f46..e26849fa0 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -8,7 +8,7 @@ Import uPred.
    predicates over finmaps instead of just ownP. *)
 
 Definition heapR : cmraT := mapR loc (fracR (dec_agreeR val)).
-Definition heapGF : iFunctor := authGF heapR.
+Definition heapGF : rFunctor := authGF heapR.
 
 Class heapG Σ := HeapG {
   heap_inG : inG heap_lang Σ (authR heapR);
@@ -38,7 +38,7 @@ Notation "l ↦{ q } v" := (heap_mapsto l q v)
 Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
 
 Section heap.
-  Context {Σ : iFunctorG}.
+  Context {Σ : rFunctorG}.
   Implicit Types N : namespace.
   Implicit Types P Q : iPropG heap_lang Σ.
   Implicit Types Φ : val → iPropG heap_lang Σ.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index d602f699d..3a0ac49bd 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -8,7 +8,7 @@ Import uPred.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
 
 Section lifting.
-Context {Σ : iFunctor}.
+Context {Σ : rFunctor}.
 Implicit Types P Q : iProp heap_lang Σ.
 Implicit Types Φ : val → iProp heap_lang Σ.
 Implicit Types K : ectx.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 23acbf0c9..bda2555cc 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -81,7 +81,7 @@ Section LiftingTests.
 End LiftingTests.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := #[ heapGF ].
+  Definition Σ : rFunctorG := #[ heapGF ].
   Notation iProp := (iPropG heap_lang Σ).
 
   Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index fdf32f50d..0a0156feb 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -8,7 +8,7 @@ Local Hint Extern 10 (✓{_} _) =>
   end; solve_validN.
 
 Section adequacy.
-Context {Λ : language} {Σ : iFunctor}.
+Context {Λ : language} {Σ : rFunctor}.
 Implicit Types e : expr Λ.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 961428f87..4e99d933f 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -8,7 +8,7 @@ Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
   auth_timeless :> CMRADiscrete A;
 }.
 
-Definition authGF (A : cmraT) : iFunctor := constF (authR A).
+Definition authGF (A : cmraT) : rFunctor := constRF (authR A).
 Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
   `{CMRAIdentity A, CMRADiscrete A} : authG Λ Σ A.
 Proof. split; try apply _. apply: inGF_inG. Qed.
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index ad194c529..8d95ee44d 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -11,12 +11,12 @@ Definition gid := nat.
 Definition gname := positive.
 
 (** The global CMRA: Indexed product over a gid i to (gname --fin--> Σ i) *)
-Definition globalF (Σ : gid → iFunctor) : iFunctor :=
-  iprodF (λ i, mapF gname (Σ i)).
-Notation iFunctorG := (gid → iFunctor).
+Definition globalF (Σ : gid → rFunctor) : rFunctor :=
+  iprodRF (λ i, mapRF gname (Σ i)).
+Notation rFunctorG := (gid → rFunctor).
 Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
 
-Class inG (Λ : language) (Σ : iFunctorG) (A : cmraT) := InG {
+Class inG (Λ : language) (Σ : rFunctorG) (A : cmraT) := InG {
   inG_id : gid;
   inG_prf : A = Σ inG_id (laterC (iPreProp Λ (globalF Σ)))
 }.
@@ -80,7 +80,8 @@ Proof.
   rewrite /own ownG_valid /to_globalF.
   rewrite iprod_validI (forall_elim inG_id) iprod_lookup_singleton.
   rewrite map_validI (forall_elim γ) lookup_singleton option_validI.
-  by destruct inG_prf.
+  (* implicit arguments differ a bit *)
+  by trans (✓ cmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf.
 Qed.
 Lemma own_valid_r γ a : own γ a ⊑ (own γ a ★ ✓ a).
 Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index 035ecf4da..666739403 100644
--- a/program_logic/global_functor.v
+++ b/program_logic/global_functor.v
@@ -1,46 +1,46 @@
 From program_logic Require Export ghost_ownership.
 
-Module iFunctors.
-  Inductive iFunctors :=
-    | nil  : iFunctors
-    | cons : iFunctor → iFunctors → iFunctors.
-  Coercion singleton (F : iFunctor) : iFunctors := cons F nil.
-End iFunctors.
-Notation iFunctors := iFunctors.iFunctors.
-
-Delimit Scope iFunctors_scope with iFunctors.
-Bind Scope iFunctors_scope with iFunctors.
-Arguments iFunctors.cons _ _%iFunctors.
-
-Notation "[ ]" := iFunctors.nil (format "[ ]") : iFunctors_scope.
-Notation "[ F ]" := (iFunctors.cons F iFunctors.nil) : iFunctors_scope.
+Module rFunctors.
+  Inductive rFunctors :=
+    | nil  : rFunctors
+    | cons : rFunctor → rFunctors → rFunctors.
+  Coercion singleton (F : rFunctor) : rFunctors := cons F nil.
+End rFunctors.
+Notation rFunctors := rFunctors.rFunctors.
+
+Delimit Scope rFunctors_scope with rFunctors.
+Bind Scope rFunctors_scope with rFunctors.
+Arguments rFunctors.cons _ _%rFunctors.
+
+Notation "[ ]" := rFunctors.nil (format "[ ]") : rFunctors_scope.
+Notation "[ F ]" := (rFunctors.cons F rFunctors.nil) : rFunctors_scope.
 Notation "[ F ; .. ; F' ]" :=
-  (iFunctors.cons F .. (iFunctors.cons F' iFunctors.nil) ..) : iFunctors_scope.
+  (rFunctors.cons F .. (rFunctors.cons F' rFunctors.nil) ..) : rFunctors_scope.
 
-Module iFunctorG.
-  Definition nil : iFunctorG := const (constF unitR).
+Module rFunctorG.
+  Definition nil : rFunctorG := const (constRF unitR).
 
-  Definition cons (F : iFunctor) (Σ : iFunctorG) : iFunctorG :=
+  Definition cons (F : rFunctor) (Σ : rFunctorG) : rFunctorG :=
     λ n, match n with O => F | S n => Σ n end.
 
-  Fixpoint app (Fs : iFunctors) (Σ : iFunctorG) : iFunctorG :=
+  Fixpoint app (Fs : rFunctors) (Σ : rFunctorG) : rFunctorG :=
     match Fs with
-    | iFunctors.nil => Σ
-    | iFunctors.cons F Fs => cons F (app Fs Σ)
+    | rFunctors.nil => Σ
+    | rFunctors.cons F Fs => cons F (app Fs Σ)
     end.
-End iFunctorG.
+End rFunctorG.
 
-(** Cannot bind this scope with the [iFunctorG] since [iFunctorG] is a
+(** Cannot bind this scope with the [rFunctorG] since [rFunctorG] is a
 notation hiding a more complex type. *)
-Notation "#[ ]" := iFunctorG.nil (format "#[ ]").
-Notation "#[ Fs ]" := (iFunctorG.app Fs iFunctorG.nil).
+Notation "#[ ]" := rFunctorG.nil (format "#[ ]").
+Notation "#[ Fs ]" := (rFunctorG.app Fs rFunctorG.nil).
 Notation "#[ Fs ; .. ; Fs' ]" :=
-  (iFunctorG.app Fs .. (iFunctorG.app Fs' iFunctorG.nil) ..).
+  (rFunctorG.app Fs .. (rFunctorG.app Fs' rFunctorG.nil) ..).
 
 (** We need another typeclass to identify the *functor* in the Σ. Basing inG on
    the functor breaks badly because Coq is unable to infer the correct
    typeclasses, it does not unfold the functor. *)
-Class inGF (Λ : language) (Σ : iFunctorG) (F : iFunctor) := InGF {
+Class inGF (Λ : language) (Σ : rFunctorG) (F : rFunctor) := InGF {
   inGF_id : gid;
   inGF_prf : F = Σ inGF_id;
 }.
@@ -53,8 +53,8 @@ Hint Mode inGF + + - : typeclass_instances.
 
 Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
 Proof. exists inGF_id. by rewrite -inGF_prf. Qed.
-Instance inGF_here {Λ Σ} (F: iFunctor) : inGF Λ (iFunctorG.cons F Σ) F.
+Instance inGF_here {Λ Σ} (F: rFunctor) : inGF Λ (rFunctorG.cons F Σ) F.
 Proof. by exists 0. Qed.
-Instance inGF_further {Λ Σ} (F F': iFunctor) :
-  inGF Λ Σ F → inGF Λ (iFunctorG.cons F' Σ) F.
+Instance inGF_further {Λ Σ} (F F': rFunctor) :
+  inGF Λ Σ F → inGF Λ (rFunctorG.cons F' Σ) F.
 Proof. intros [i ?]. by exists (S i). Qed.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 95992a776..b988a7fe9 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -19,7 +19,7 @@ Notation "{{ P } } e {{ Φ } }" := (True ⊑ ht ⊤ P e Φ)
    format "{{  P  } }  e  {{  Φ  } }") : C_scope.
 
 Section hoare.
-Context {Λ : language} {Σ : iFunctor}.
+Context {Λ : language} {Σ : rFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types Φ Ψ : val Λ → iProp Λ Σ.
 Implicit Types v : val Λ.
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index b5c38de20..ada18d5bb 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -12,7 +12,7 @@ Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
    format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : C_scope.
 
 Section lifting.
-Context {Λ : language} {Σ : iFunctor}.
+Context {Λ : language} {Σ : rFunctor}.
 Implicit Types e : expr Λ.
 Implicit Types P Q R : iProp Λ Σ.
 Implicit Types Ψ : val Λ → iProp Λ Σ.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index b9dcdea18..6e64e4041 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -14,7 +14,7 @@ Instance: Params (@inv) 3.
 Typeclasses Opaque inv.
 
 Section inv.
-Context {Λ : language} {Σ : iFunctor}.
+Context {Λ : language} {Σ : rFunctor}.
 Implicit Types i : positive.
 Implicit Types N : namespace.
 Implicit Types P Q R : iProp Λ Σ.
diff --git a/program_logic/language.v b/program_logic/language.v
index 7be7c9266..4bd430131 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -27,7 +27,7 @@ Arguments values_stuck {_} _ _ _ _ _ _.
 Arguments atomic_not_val {_} _ _.
 Arguments atomic_step {_} _ _ _ _ _ _ _.
 
-Canonical Structure istateC Σ := leibnizC (state Σ).
+Canonical Structure stateC Σ := leibnizC (state Σ).
 
 Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
 
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 0982d5242..20079e46b 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -8,7 +8,7 @@ Local Hint Extern 10 (✓{_} _) =>
   end; solve_validN.
 
 Section lifting.
-Context {Λ : language} {Σ : iFunctor}.
+Context {Λ : language} {Σ : rFunctor}.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 Implicit Types σ : state Λ.
diff --git a/program_logic/model.v b/program_logic/model.v
index 73c40d828..8b8376970 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -6,39 +6,29 @@ From algebra Require Import cofe_solver.
 COFEs to the category of CMRAs, which is instantiated with [laterC iProp]. The
 [laterC iProp] can be used to construct impredicate CMRAs, such as the stored
 propositions using the agreement CMRA. *)
-
-(* TODO RJ: Can we make use of resF, the resource functor? *)
-Module iProp.
-Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT :=
-  uPredC (resR Λ Σ (laterC A)).
-Definition map {Λ : language} {Σ : iFunctor} {A1 A2 B1 B2 : cofeT}
-    (f : (A2 -n> A1) * (B1 -n> B2)) : F Λ Σ A1 B1 -n> F Λ Σ A2 B2 :=
-  uPredC_map (resC_map (laterC_map (f.1))).
-Definition result Λ Σ : solution (F Λ Σ).
+Definition iProp_result (Λ : language) (Σ : rFunctor) :
+  solution (uPredCF (resRF Λ laterCF (laterRF Σ))).
 Proof.
-  apply (solver.result _ (@map Λ Σ)).
-  - intros A B P. rewrite /map /= -{2}(uPred_map_id P). apply uPred_map_ext=> r.
-    rewrite /= -{2}(res_map_id r); apply res_map_ext=>{r} r /=.
-    by rewrite later_map_id.
-  - intros A1 A2 A3 B1 B2 B3 f g f' g' P. rewrite /map /=.
-    rewrite -uPred_map_compose. apply uPred_map_ext=>{P} r /=.
-    rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
-    by rewrite -later_map_compose.
-  - intros A1 A2 B1 B2 n f f' Hf P; split=> n' -[???].
-    apply upredC_map_ne, resC_map_ne, laterC_map_contractive.
-    by intros i ?; apply Hf.
+  (* Contractiveness should be derived from general properties about functors *)
+  apply (solver.result _)=> A1 A2 B1 B2.
+  intros n fg fg' Hf P; split=> n' -[???].
+  apply uPredC_map_ne, resC_map_ne; simpl.
+  - apply laterC_map_contractive=> i ?. by apply Hf.
+  - apply rFunctor_ne; split; apply laterC_map_contractive=> i ?; by apply Hf.
 Qed.
-End iProp.
 
 (* Solution *)
-Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp.result Λ Σ.
-Definition iRes Λ Σ := res Λ Σ (laterC (iPreProp Λ Σ)).
-Definition iResR Λ Σ := resR Λ Σ (laterC (iPreProp Λ Σ)).
-Definition iWld Λ Σ := mapR positive (agreeR (laterC (iPreProp Λ Σ))).
-Definition iPst Λ := exclR (istateC Λ).
-Definition iGst Λ Σ := ifunctor_car Σ (laterC (iPreProp Λ Σ)).
-Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResR Λ Σ).
-Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ := solution_fold _.
+Definition iPreProp (Λ : language) (Σ : rFunctor) : cofeT := iProp_result Λ Σ.
+Definition iGst (Λ : language) (Σ : rFunctor) : cmraT :=
+  Σ (laterC (iPreProp Λ Σ)).
+Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
+Definition iResR Λ Σ := resR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
+Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
+Definition iPst Λ := excl (state Λ).
+
+Definition iProp (Λ : language) (Σ : rFunctor) : cofeT := uPredC (iResR Λ Σ).
+Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ :=
+  solution_fold (iProp_result Λ Σ).
 Definition iProp_fold {Λ Σ} : iPreProp Λ Σ -n> iProp Λ Σ := solution_unfold _.
 Lemma iProp_fold_unfold {Λ Σ} (P : iProp Λ Σ) : iProp_fold (iProp_unfold P) ≡ P.
 Proof. apply solution_unfold_fold. Qed.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 4b657f72b..af0c10c03 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -12,7 +12,7 @@ Instance: Params (@ownG) 2.
 Typeclasses Opaque ownI ownG ownP.
 
 Section ownership.
-Context {Λ : language} {Σ : iFunctor}.
+Context {Λ : language} {Σ : rFunctor}.
 Implicit Types r : iRes Λ Σ.
 Implicit Types σ : state Λ.
 Implicit Types P : iProp Λ Σ.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index f99d37720..6d1312c3e 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -40,7 +40,7 @@ Notation "|={ E }=> Q" := (pvs E E Q%I)
    format "|={ E }=>  Q") : uPred_scope.
 
 Section pvs.
-Context {Λ : language} {Σ : iFunctor}.
+Context {Λ : language} {Σ : rFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types m : iGst Λ Σ.
 
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 725119058..eabb26b70 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -1,11 +1,11 @@
-From algebra Require Export fin_maps agree excl functor.
+From algebra Require Export fin_maps agree excl.
 From algebra Require Import upred.
 From program_logic Require Export language.
 
-Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res {
+Record res (Λ : language) (A : cofeT) (M : cmraT) := Res {
   wld : mapR positive (agreeR A);
-  pst : exclR (istateC Λ);
-  gst : optionR (Σ A);
+  pst : exclR (stateC Λ);
+  gst : optionR M;
 }.
 Add Printing Constructor res.
 Arguments Res {_ _ _} _ _ _.
@@ -18,39 +18,39 @@ Instance: Params (@pst) 3.
 Instance: Params (@gst) 3.
 
 Section res.
-Context {Λ : language} {Σ : iFunctor} {A : cofeT}.
-Implicit Types r : res Λ Σ A.
+Context {Λ : language} {A : cofeT} {M : cmraT}.
+Implicit Types r : res Λ A M.
 
-Inductive res_equiv' (r1 r2 : res Λ Σ A) := Res_equiv :
+Inductive res_equiv' (r1 r2 : res Λ A M) := Res_equiv :
   wld r1 ≡ wld r2 → pst r1 ≡ pst r2 → gst r1 ≡ gst r2 → res_equiv' r1 r2.
-Instance res_equiv : Equiv (res Λ Σ A) := res_equiv'.
-Inductive res_dist' (n : nat) (r1 r2 : res Λ Σ A) := Res_dist :
+Instance res_equiv : Equiv (res Λ A M) := res_equiv'.
+Inductive res_dist' (n : nat) (r1 r2 : res Λ A M) := Res_dist :
   wld r1 ≡{n}≡ wld r2 → pst r1 ≡{n}≡ pst r2 → gst r1 ≡{n}≡ gst r2 →
   res_dist' n r1 r2.
-Instance res_dist : Dist (res Λ Σ A) := res_dist'.
+Instance res_dist : Dist (res Λ A M) := res_dist'.
 Global Instance Res_ne n :
-  Proper (dist n ==> dist n ==> dist n ==> dist n) (@Res Λ Σ A).
+  Proper (dist n ==> dist n ==> dist n ==> dist n) (@Res Λ A M).
 Proof. done. Qed.
-Global Instance Res_proper : Proper ((≡) ==> (≡) ==> (≡) ==> (≡)) (@Res Λ Σ A).
+Global Instance Res_proper : Proper ((≡) ==> (≡) ==> (≡) ==> (≡)) (@Res Λ A M).
 Proof. done. Qed.
-Global Instance wld_ne n : Proper (dist n ==> dist n) (@wld Λ Σ A).
+Global Instance wld_ne n : Proper (dist n ==> dist n) (@wld Λ A M).
 Proof. by destruct 1. Qed.
-Global Instance wld_proper : Proper ((≡) ==> (≡)) (@wld Λ Σ A).
+Global Instance wld_proper : Proper ((≡) ==> (≡)) (@wld Λ A M).
 Proof. by destruct 1. Qed.
-Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Λ Σ A).
+Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Λ A M).
 Proof. by destruct 1. Qed.
-Global Instance pst_ne' n : Proper (dist n ==> (≡)) (@pst Λ Σ A).
+Global Instance pst_ne' n : Proper (dist n ==> (≡)) (@pst Λ A M).
 Proof. destruct 1; apply: timeless; apply dist_le with n; auto with lia. Qed.
-Global Instance pst_proper : Proper ((≡) ==> (=)) (@pst Λ Σ A).
+Global Instance pst_proper : Proper ((≡) ==> (=)) (@pst Λ A M).
 Proof. by destruct 1; unfold_leibniz. Qed.
-Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Λ Σ A).
+Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Λ A M).
 Proof. by destruct 1. Qed.
-Global Instance gst_proper : Proper ((≡) ==> (≡)) (@gst Λ Σ A).
+Global Instance gst_proper : Proper ((≡) ==> (≡)) (@gst Λ A M).
 Proof. by destruct 1. Qed.
-Instance res_compl : Compl (res Λ Σ A) := λ c,
+Instance res_compl : Compl (res Λ A M) := λ c,
   Res (compl (chain_map wld c))
       (compl (chain_map pst c)) (compl (chain_map gst c)).
-Definition res_cofe_mixin : CofeMixin (res Λ Σ A).
+Definition res_cofe_mixin : CofeMixin (res Λ A M).
 Proof.
   split.
   - intros w1 w2; split.
@@ -71,32 +71,32 @@ Global Instance res_timeless r :
   Timeless (wld r) → Timeless (gst r) → Timeless r.
 Proof. by destruct 3; constructor; try apply: timeless. Qed.
 
-Instance res_op : Op (res Λ Σ A) := λ r1 r2,
+Instance res_op : Op (res Λ A M) := λ r1 r2,
   Res (wld r1 â‹… wld r2) (pst r1 â‹… pst r2) (gst r1 â‹… gst r2).
-Global Instance res_empty : Empty (res Λ Σ A) := Res ∅ ∅ ∅.
-Instance res_unit : Unit (res Λ Σ A) := λ r,
+Global Instance res_empty : Empty (res Λ A M) := Res ∅ ∅ ∅.
+Instance res_unit : Unit (res Λ A M) := λ r,
   Res (unit (wld r)) (unit (pst r)) (unit (gst r)).
-Instance res_valid : Valid (res Λ Σ A) := λ r, ✓ wld r ∧ ✓ pst r ∧ ✓ gst r.
-Instance res_validN : ValidN (res Λ Σ A) := λ n r,
+Instance res_valid : Valid (res Λ A M) := λ r, ✓ wld r ∧ ✓ pst r ∧ ✓ gst r.
+Instance res_validN : ValidN (res Λ A M) := λ n r,
   ✓{n} wld r ∧ ✓{n} pst r ∧ ✓{n} gst r.
-Instance res_minus : Div (res Λ Σ A) := λ r1 r2,
+Instance res_minus : Div (res Λ A M) := λ r1 r2,
   Res (wld r1 ÷ wld r2) (pst r1 ÷ pst r2) (gst r1 ÷ gst r2).
 
-Lemma res_included (r1 r2 : res Λ Σ A) :
+Lemma res_included (r1 r2 : res Λ A M) :
   r1 ≼ r2 ↔ wld r1 ≼ wld r2 ∧ pst r1 ≼ pst r2 ∧ gst r1 ≼ gst r2.
 Proof.
   split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
   intros [r Hr]; split_and?;
     [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
 Qed.
-Lemma res_includedN (r1 r2 : res Λ Σ A) n :
+Lemma res_includedN (r1 r2 : res Λ A M) n :
   r1 ≼{n} r2 ↔ wld r1 ≼{n} wld r2 ∧ pst r1 ≼{n} pst r2 ∧ gst r1 ≼{n} gst r2.
 Proof.
   split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
   intros [r Hr]; split_and?;
     [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
 Qed.
-Definition res_cmra_mixin : CMRAMixin (res Λ Σ A).
+Definition res_cmra_mixin : CMRAMixin (res Λ A M).
 Proof.
   split.
   - by intros n x [???] ? [???]; constructor; cofe_subst.
@@ -132,9 +132,9 @@ Proof.
   - apply _.
 Qed.
 
-Definition update_pst (σ : state Λ) (r : res Λ Σ A) : res Λ Σ A :=
+Definition update_pst (σ : state Λ) (r : res Λ A M) : res Λ A M :=
   Res (wld r) (Excl σ) (gst r).
-Definition update_gst (m : Σ A) (r : res Λ Σ A) : res Λ Σ A :=
+Definition update_gst (m : M) (r : res Λ A M) : res Λ A M :=
   Res (wld r) (pst r) (Some m).
 
 Lemma wld_validN n r : ✓{n} r → ✓{n} wld r.
@@ -156,73 +156,90 @@ Qed.
 Lemma lookup_wld_op_r n r1 r2 i P :
   ✓{n} (r1⋅r2) → wld r2 !! i ≡{n}≡ Some P → (wld r1 ⋅ wld r2) !! i ≡{n}≡ Some P.
 Proof. rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l. Qed.
-Global Instance Res_timeless eσ m : Timeless m → Timeless (Res ∅ eσ m).
+Global Instance Res_timeless eσ m : Timeless m → Timeless (@Res Λ A M ∅ eσ m).
 Proof. by intros ? ? [???]; constructor; apply: timeless. Qed.
 
 (** Internalized properties *)
-Lemma res_equivI {M} r1 r2 :
-  (r1 ≡ r2)%I ≡ (wld r1 ≡ wld r2 ∧ pst r1 ≡ pst r2 ∧ gst r1 ≡ gst r2: uPred M)%I.
+Lemma res_equivI {M'} r1 r2 :
+  (r1 ≡ r2)%I
+  ≡ (wld r1 ≡ wld r2 ∧ pst r1 ≡ pst r2 ∧ gst r1 ≡ gst r2: uPred M')%I.
 Proof.
   uPred.unseal. do 2 split. by destruct 1. by intros (?&?&?); by constructor.
 Qed.
-Lemma res_validI {M} r : (✓ r)%I ≡ (✓ wld r ∧ ✓ pst r ∧ ✓ gst r : uPred M)%I.
+Lemma res_validI {M'} r : (✓ r)%I ≡ (✓ wld r ∧ ✓ pst r ∧ ✓ gst r : uPred M')%I.
 Proof. by uPred.unseal. Qed.
 End res.
 
 Arguments resC : clear implicits.
 Arguments resR : clear implicits.
 
-Definition res_map {Λ Σ A B} (f : A -n> B) (r : res Λ Σ A) : res Λ Σ B :=
-  Res (agree_map f <$> wld r) (pst r) (ifunctor_map Σ f <$> gst r).
-Instance res_map_ne Λ Σ (A B : cofeT) (f : A -n> B) :
-  (∀ n, Proper (dist n ==> dist n) f) →
-  ∀ n, Proper (dist n ==> dist n) (@res_map Λ Σ _ _ f).
-Proof. by intros Hf n [] ? [???]; constructor; simpl in *; cofe_subst. Qed.
-Lemma res_map_id {Λ Σ A} (r : res Λ Σ A) : res_map cid r ≡ r.
+(* Functor *)
+Definition res_map {Λ} {A A' : cofeT} {M M' : cmraT}
+    (f : A → A') (g : M → M') (r : res Λ A M) : res Λ A' M' :=
+  Res (agree_map f <$> wld r) (pst r) (g <$> gst r).
+Instance res_map_ne {Λ} {A A': cofeT} {M M' : cmraT} (f : A → A') (g : M → M') :
+  (∀ n, Proper (dist n ==> dist n) f) → (∀ n, Proper (dist n ==> dist n) g) →
+  ∀ n, Proper (dist n ==> dist n) (@res_map Λ _ _ _ _ f g).
+Proof. intros Hf n [] ? [???]; constructor; by cofe_subst. Qed.
+Lemma res_map_id {Λ A M} (r : res Λ A M) : res_map id id r ≡ r.
 Proof.
-  constructor; simpl; [|done|].
-  - rewrite -{2}(map_fmap_id (wld r)); apply map_fmap_setoid_ext=> i y ? /=.
-    by rewrite -{2}(agree_map_id y); apply agree_map_ext.
-  - rewrite -{2}(option_fmap_id (gst r)); apply option_fmap_setoid_ext=> m /=.
-    by rewrite -{2}(ifunctor_map_id Σ m); apply ifunctor_map_ext.
+  constructor; rewrite /res_map /=; f_equal.
+  - rewrite -{2}(map_fmap_id (wld r)). apply map_fmap_setoid_ext=> i y ? /=.
+    by rewrite -{2}(agree_map_id y).
+  - by rewrite option_fmap_id.
 Qed.
-Lemma res_map_compose {Λ Σ A B C} (f : A -n> B) (g : B -n> C) (r : res Λ Σ A) :
-  res_map (g ◎ f) r ≡ res_map g (res_map f r).
+Lemma res_map_compose {Λ} {A1 A2 A3 : cofeT} {M1 M2 M3 : cmraT}
+   (f : A1 → A2) (f' : A2 → A3) (g : M1 → M2) (g' : M2 → M3) (r : res Λ A1 M1) :
+  res_map (f' ∘ f) (g' ∘ g) r ≡ res_map f' g' (res_map f g r).
 Proof.
-  constructor; simpl; [|done|].
+  constructor; rewrite /res_map /=; f_equal.
   - rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
-    by rewrite -agree_map_compose; apply agree_map_ext.
-  - rewrite -option_fmap_compose; apply option_fmap_setoid_ext=> m /=.
-    by rewrite -ifunctor_map_compose; apply ifunctor_map_ext.
+    by rewrite -agree_map_compose.
+  - by rewrite option_fmap_compose.
 Qed.
-Lemma res_map_ext {Λ Σ A B} (f g : A -n> B) (r : res Λ Σ A) :
-  (∀ x, f x ≡ g x) → res_map f r ≡ res_map g r.
+Lemma res_map_ext {Λ} {A A' : cofeT} {M M' : cmraT}
+    (f f' : A → A') (g g' : M → M') (r : res Λ A M) :
+  (∀ x, f x ≡ f' x) → (∀ m, g m ≡ g' m) → res_map f g r ≡ res_map f' g' r.
 Proof.
-  intros Hfg; split; simpl; auto.
+  intros Hf Hg; split; simpl; auto.
   - by apply map_fmap_setoid_ext=>i x ?; apply agree_map_ext.
-  - by apply option_fmap_setoid_ext=>m; apply ifunctor_map_ext.
+  - by apply option_fmap_setoid_ext.
 Qed.
-Instance res_map_cmra_monotone {Λ Σ} {A B : cofeT} (f : A -n> B) :
-  CMRAMonotone (@res_map Λ Σ _ _ f).
+Instance res_map_cmra_monotone {Λ}
+    {A A' : cofeT} {M M': cmraT} (f: A → A') (g: M → M') :
+  (∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone g →
+  CMRAMonotone (@res_map Λ _ _ _ _ f g).
 Proof.
   split; first apply _.
-  - by intros n r (?&?&?); split_and!; simpl; try apply: validN_preserving.
+  - intros n r (?&?&?); split_and!; simpl; by try apply: validN_preserving.
   - by intros r1 r2; rewrite !res_included;
       intros (?&?&?); split_and!; simpl; try apply: included_preserving.
 Qed.
-Definition resC_map {Λ Σ A B} (f : A -n> B) : resC Λ Σ A -n> resC Λ Σ B :=
-  CofeMor (res_map f : resC Λ Σ A → resC Λ Σ B).
-Instance resC_map_ne {Λ Σ A B} n :
-  Proper (dist n ==> dist n) (@resC_map Λ Σ A B).
+Definition resC_map {Λ} {A A' : cofeT} {M M' : cmraT}
+    (f : A -n> A') (g : M -n> M') : resC Λ A M -n> resC Λ A' M' :=
+  CofeMor (res_map f g : resC Λ A M → resC Λ A' M').
+Instance resC_map_ne {Λ A A' M M'} n :
+  Proper (dist n ==> dist n ==> dist n) (@resC_map Λ A A' M M').
 Proof.
   intros f g Hfg r; split; simpl; auto.
   - by apply (mapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
-  - by apply optionC_map_ne, ifunctor_map_ne.
+  - by apply optionC_map_ne.
 Qed.
 
-Program Definition resF {Λ Σ} : iFunctor := {|
-  ifunctor_car := resR Λ Σ;
-  ifunctor_map A B := resC_map
+Program Definition resRF (Λ : language)
+    (F : cFunctor) (Σ : rFunctor) : rFunctor := {|
+  rFunctor_car A B := resR Λ (cFunctor_car F A B) (rFunctor_car Σ A B);
+  rFunctor_map A1 A2 B1 B2 fg :=resC_map (cFunctor_map F fg) (rFunctor_map Σ fg)
 |}.
-Next Obligation. intros Λ Σ A x. by rewrite /= res_map_id. Qed.
-Next Obligation. intros Λ Σ A B C f g x. by rewrite /= res_map_compose. Qed.
+Next Obligation.
+  intros Λ F Σ A1 A2 B1 B2 n f g Hfg.
+  apply resC_map_ne. by apply cFunctor_ne. by apply rFunctor_ne.
+Qed.
+Next Obligation.
+  intros Λ F Σ A B x. rewrite /= -{2}(res_map_id x).
+  apply res_map_ext=>y. apply cFunctor_id. apply rFunctor_id.
+Qed.
+Next Obligation.
+  intros Λ F Σ A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -res_map_compose.
+  apply res_map_ext=>y. apply cFunctor_compose. apply rFunctor_compose.
+Qed.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 01ad6e3f0..30e3f53c0 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -5,7 +5,7 @@ Import uPred.
 Notation savedPropG Λ Σ :=
   (inG Λ Σ (agreeR (laterC (iPreProp Λ (globalF Σ))))).
 
-Instance inGF_savedPropG `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
+Instance inGF_savedPropG `{inGF Λ Σ (agreeRF idCF)} : savedPropG Λ Σ.
 Proof. apply: inGF_inG. Qed.
 
 Definition saved_prop_own `{savedPropG Λ Σ}
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 0731ee12f..814c5ae98 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -8,7 +8,7 @@ Class stsG Λ Σ (sts : stsT) := StsG {
 }.
 Coercion sts_inG : stsG >-> inG.
 
-Definition stsGF (sts : stsT) : iFunctor := constF (stsR sts).
+Definition stsGF (sts : stsT) : rFunctor := constRF (stsR sts).
 Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
   `{Inhabited (sts.state sts)} : stsG Λ Σ sts.
 Proof. split; try apply _. apply: inGF_inG. Qed.
diff --git a/program_logic/tests.v b/program_logic/tests.v
index c5ef324a8..9d81b5333 100644
--- a/program_logic/tests.v
+++ b/program_logic/tests.v
@@ -2,6 +2,6 @@
 From program_logic Require Import model.
 
 Module ModelTest. (* Make sure we got the notations right. *)
-  Definition iResTest {Λ : language} {Σ : iFunctor}
+  Definition iResTest {Λ : language} {Σ : rFunctor}
     (w : iWld Λ Σ) (p : iPst Λ) (g : iGst Λ Σ) : iRes Λ Σ := Res w p (Some g).
 End ModelTest.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index a01eab178..28a3cb3d0 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -18,7 +18,7 @@ Notation "P ={ E }=> Q" := (True ⊑ vs E E P%I Q%I)
   (at level 199, E at level 50, format "P  ={ E }=>  Q") : C_scope.
 
 Section vs.
-Context {Λ : language} {Σ : iFunctor}.
+Context {Λ : language} {Σ : rFunctor}.
 Implicit Types P Q R : iProp Λ Σ.
 Implicit Types N : namespace.
 
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 9a0d67233..ea1d7996b 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -65,7 +65,7 @@ Notation "|| e {{ Φ } }" := (wp ⊤ e Φ)
    format "||  e   {{  Φ  } }") : uPred_scope.
 
 Section wp.
-Context {Λ : language} {Σ : iFunctor}.
+Context {Λ : language} {Σ : rFunctor}.
 Implicit Types P : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
 Implicit Types v : val Λ.
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index adf343e2a..89f0160fd 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -28,7 +28,7 @@ Instance: Params (@wsat) 5.
 Arguments wsat : simpl never.
 
 Section wsat.
-Context {Λ : language} {Σ : iFunctor}.
+Context {Λ : language} {Σ : rFunctor}.
 Implicit Types σ : state Λ.
 Implicit Types r : iRes Λ Σ.
 Implicit Types rs : gmap positive (iRes Λ Σ).
-- 
GitLab