diff --git a/iris/agree.v b/iris/agree.v
index d60df048ff73a0aa17c59751c404923b74b41487..32853052a4aba4e2f6d1ac0102efeb79d566ce28 100644
--- a/iris/agree.v
+++ b/iris/agree.v
@@ -124,7 +124,7 @@ Proof.
 Qed.
 End agree.
 
-Canonical Structure agreeC (A : cmraT) : cmraT := CMRAT (agree A).
+Canonical Structure agreeRA (A : cofeT) : cmraT := CMRAT (agree A).
 
 Section agree_map.
   Context `{Cofe A, Cofe B} (f: A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
@@ -147,3 +147,6 @@ Section agree_map.
         try apply Hxy; eauto using agree_valid_le.
   Qed.
 End agree_map.
+
+Definition agreeRA_map {A B} (f : A -n> B) : agreeRA A -n> agreeRA B :=
+  CofeMor (agree_map f : agreeRA A → agreeRA B).