Introduce cofeT -> cofeT functors, switch to bifunctors.

This cleans up some ad-hoc stuff and prepares for a generalization
of saved propositions.

_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

algebra/agree.v

 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.

algebra/auth.v

 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.

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.

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.

algebra/cofe_solver.v

 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].

algebra/excl.v

 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.

algebra/fin_maps.v

 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.

algebra/frac.v

 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.

algebra/functor.v

-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.

algebra/iprod.v

 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.

algebra/option.v

 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.

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 }.

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 }}.

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 Σ).
 

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 Σ).
 

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 Σ.
 

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 Σ.

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.

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 }}.