Make various functors more consistent with each other.

algebra/auth.v

@@ -169,22 +169,24 @@ End cmra.
 Arguments authRA : clear implicits.
 
 (* Functor *)
-Instance auth_fmap : FMap auth := λ A B f x,
-  Auth (f <$> authoritative x) (f (own x)).
-Arguments auth_fmap _ _ _ !_ /.
-Lemma auth_fmap_id {A} (x : auth A) : id <$> x = x.
-Proof. by destruct x; rewrite /= excl_fmap_id. Qed.
-Lemma excl_fmap_compose {A B C} (f : A → B) (g : B → C) (x : auth A) :
-  g ∘ f <$> x = g <$> f <$> x.
-Proof. by destruct x; rewrite /= excl_fmap_compose. Qed.
-Instance auth_fmap_cmra_ne {A B : cofeT} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap auth _ A B).
+Definition auth_map {A B} (f : A → B) (x : auth A) : auth B :=
+  Auth (excl_map f (authoritative x)) (f (own x)).
+Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
+Proof. by destruct x; rewrite /auth_map excl_map_id. Qed.
+Lemma auth_map_compose {A B C} (f : A → B) (g : B → C) (x : auth A) :
+  auth_map (g ∘ f) x = auth_map g (auth_map f x).
+Proof. by destruct x; rewrite /auth_map excl_map_compose. Qed.
+Lemma auth_map_ext {A B : cofeT} (f g : A → B) x :
+  (∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x.
+Proof. constructor; simpl; auto using excl_map_ext. Qed.
+Instance auth_map_cmra_ne {A B : cofeT} n :
+  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
 Proof.
-  intros f g Hf [??] [??] [??]; split; [by apply excl_fmap_cmra_ne|by apply Hf].
+  intros f g Hf [??] [??] [??]; split; [by apply excl_map_cmra_ne|by apply Hf].
 Qed.
-Instance auth_fmap_cmra_monotone {A B : cmraT} (f : A → B) :
-  (∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone f →
-  CMRAMonotone (fmap f : auth A → auth B).
+Instance auth_map_cmra_monotone {A B : cmraT} (f : A → B) :
+  (∀ n, Proper (dist n ==> dist n) f) →
+  CMRAMonotone f → CMRAMonotone (auth_map f).
 Proof.
   split.
   * by intros n [x a] [y b]; rewrite !auth_includedN /=;
@@ -193,6 +195,6 @@ Proof.
       naive_solver eauto using @includedN_preserving, @validN_preserving.
 Qed.
 Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
-  CofeMor (fmap f : authC A → authC B).
+  CofeMor (auth_map f).
 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.

algebra/cofe.v

@@ -441,12 +441,21 @@ Arguments iprodC {_} _.
 
 Definition iprod_map {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x)
   (g : iprod B1) : iprod B2 := λ x, f _ (g x).
+Lemma iprod_map_ext {A} {B1 B2 : A → cofeT} (f1 f2 : ∀ x, B1 x → B2 x) g :
+  (∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g.
+Proof. done. Qed.
+Lemma iprod_map_id {A} {B: A → cofeT} (g : iprod B) : iprod_map (λ _, id) g = g.
+Proof. done. Qed.
+Lemma iprod_map_compose {A} {B1 B2 B3 : A → cofeT}
+    (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : iprod B1) :
+  iprod_map (λ x, f2 x ∘ f1 x) g = iprod_map f2 (iprod_map f1 g).
+Proof. done. Qed.
 Instance iprod_map_ne {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x) n :
   (∀ x, Proper (dist n ==> dist n) (f x)) →
   Proper (dist n ==> dist n) (iprod_map f).
 Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
 Definition iprodC_map {A} {B1 B2 : A → cofeT} (f : iprod (λ x, B1 x -n> B2 x)) :
   iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
-Instance laterC_map_ne {A} {B1 B2 : A → cofeT} n :
+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.

algebra/excl.v

@@ -154,27 +154,30 @@ Arguments exclC : clear implicits.
 Arguments exclRA : clear implicits.
 
 (* Functor *)
-Instance excl_fmap : FMap excl := λ A B f x,
+Definition excl_map {A B} (f : A → B) (x : excl A) : excl B :=
   match x with
   | Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
   end.
-Lemma excl_fmap_id {A} (x : excl A) : id <$> x = x.
+Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
 Proof. by destruct x. Qed.
-Lemma excl_fmap_compose {A B C} (f : A → B) (g : B → C) (x : excl A) :
-  g ∘ f <$> x = g <$> f <$> x.
+Lemma excl_map_compose {A B C} (f : A → B) (g : B → C) (x : excl A) :
+  excl_map (g ∘ f) x = excl_map g (excl_map f x).
 Proof. by destruct x. Qed.
-Instance excl_fmap_cmra_ne {A B : cofeT} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap excl _ A B).
+Lemma excl_map_ext {A B : cofeT} (f g : A → B) x :
+  (∀ x, f x ≡ g x) → excl_map f x ≡ excl_map g x.
+Proof. by destruct x; constructor. Qed.
+Instance excl_map_cmra_ne {A B : cofeT} n :
+  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
 Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
-Instance excl_fmap_cmra_monotone {A B : cofeT} :
-  (∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone (fmap f : excl A → excl B).
+Instance excl_map_cmra_monotone {A B : cofeT} (f : A → B) :
+  (∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone (excl_map f).
 Proof.
   split.
-  * intros n x y [z Hy]; exists (f <$> z); rewrite Hy.
+  * intros n x y [z Hy]; exists (excl_map f z); rewrite Hy.
     by destruct x, z; constructor.
   * by intros n [a| |].
 Qed.
 Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
-  CofeMor (fmap f : exclRA A → exclRA B).
+  CofeMor (excl_map f).
 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.